publications

2026

1. Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features

   Anne M Tumlin, Ben Wooding, Zhenxuan Shao, and 3 more authors

   In Proceedings of the Symposium on AI Verification (SAIV), 2026

   To appear

   Abs Code

   Graph neural networks (GNNs) have become a prominent approach for developing fast, topology-aware surrogates in electric power systems, supporting tasks such as power flow (PF) analysis, optimal power flow (OPF) estimation, and cascading failure analysis (CFA). Despite this growing use, formally verifying GNN-based models remains challenging, with existing methods limited in scope. We extend the neural network verification (NNV) framework to graph-structured inputs through GraphStar sets, a generalization of Star sets that captures uncertainty over both node and edge features. This extension enables the propagation of linear message-passing operations and the sound approximation of ReLU nonlinearities for GNN architectures, including graph convolutional network (GCN) and graph isomorphism network with edge features (GINE) layers. We evaluate GNNV across three power system tasks, PF, OPF, and CFA, on the IEEE-24, IEEE-39, and IEEE-118 test cases, as well as two standard graph classification benchmarks, ENZYMES and PROTEINS. Our results show that GNNV provides tighter robustness guarantees than CORA on graph classification models with ReLU-based activations and, for the first time, delivers edge-aware robustness guarantees for GINE-based PF and OPF models under joint node and edge perturbations.

2024

1. FairNNV: The Neural Network Verification Tool For Certifying Fairness

   Anne M Tumlin, Diego Manzanas Lopez, Preston Robinette, and 3 more authors

   In Proceedings of the 5th ACM International Conference on AI in Finance, 2024

   Abs

   Ensuring fairness in machine learning (ML) is vital, especially as these models are increasingly used in socially critical financial decision-making processes such as credit scoring, loan approvals, and fraud detection. Fairness verification aims to provide formal guarantees of fairness in ML models. In this work, we introduce FairNNV, a tool that leverages the Neural Network Verification (NNV) framework to verify individual and counterfactual fairness using reachability analysis techniques. FairNNV introduces the Verified Fairness (VF) score to quantify fairness. Additionally, we compare the verification process of models before and after applying adversarial debiasing techniques to assess the impact of bias mitigation. We demonstrate FairNNV’s effectiveness on several fairness benchmark datasets, including Adult Census, German Credit, and Bank Marketing, with a focused analysis on the impact of adversarial debiasing on Adult Census classifiers. Experimental results show differences between empirical fairness improvements using adversarial debiasing and fairness verification scores with FairNNV, indicating a need for integrating formal verification into the evaluation process to guide model selections when assessing fairness.

2. Verification of Behavior Trees with Contingency Monitors

   Serena S. Serbinowska, Nicholas Potteiger, Anne M. Tumlin, and 1 more author

   Electronic Proceedings in Theoretical Computer Science, Nov 2024

2021

1. Toxic Comment Detection: Analyzing the Combination of Text and Emojis

   Michael Aquino, Yasiris Ortiz, Arif Rashid, and 4 more authors

   In 2021 IEEE 18th International Conference on Mobile Ad Hoc and Smart Systems (MASS), Oct 2021

   ISSN: 2155-6814

   Abs

   Detection of toxicity in online commentary is a growing branch of Natural Language Processing (NLP). Most research in the area rely only on text-based toxic comment detection. We propose a machine learning approach for detecting the toxicity of a comment by analyzing both the text and the emojis within the comment. Our approach utilizes word embeddings derived from GloVe and emoji2vec to train a bidirectional Long Short Term Memory (biLSTM) model. We also create a new labeled dataset with comments with text and emojis. The accuracy score of our model on preliminary data is 0.911.

2. A Visibility Roadmap Sampling Approach for a Multi-Robot Visibility-Based Pursuit-Evasion Problem

   Trevor Olsen, Anne M. Tumlin, Nicholas M. Stiffler, and 1 more author

   In 2021 IEEE International Conference on Robotics and Automation (ICRA), May 2021

   ISSN: 2577-087X

   Abs

   Given a two-dimensional polygonal space, the multi-robot visibility-based pursuit-evasion problem tasks several pursuer robots with the goal of establishing visibility with an arbitrarily fast evader. The best known complete algorithm for this problem takes time doubly exponential in the number of robots. However, sampling-based techniques have shown promise in generating feasible solutions in these scenarios. One of the primary drawbacks to employing existing sampling-based methods is that existing algorithms have long execution times and high failure rates for complex environments. This paper addresses that limitation by proposing a new algorithm that takes an environment as its input and returns a joint motion strategy which ensures that the evader is captured by one of the pursuers. Starting with a single pursuer, we sequentially construct Sample-Generated Pursuit-Evasion Graphs to create such a joint motion strategy. This sequential graph structure ensures that our algorithm will always terminate with a solution, regardless of the complexity of the environment. We describe an implementation of this algorithm and present quantitative results that show significant improvement in comparison to the existing algorithm.