aiqbench analysis
This research extends formal verification frameworks to graph neural networks (GNNs), providing sound robustness guarantees for architectures like GCN and GINE used in critical infrastructure such as electric power systems. By introducing GraphStar sets, the authors enable rigorous analysis of uncertainty across both node and edge features, addressing a key limitation in existing methods that often ignore edge perturbations. The study demonstrates tighter bounds on model reliability compared to prior approaches, offering essential safety assurances for deploying GNNs in high-stakes applications where topology-aware surrogates are vital.
Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features
arXiv:2609.30079v1 Announce Type: new Abstract: 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.
Abstract: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.
Machine Learning (cs.LG); Artificial Intelligence (cs.AI)
arXiv:2609.30079 [cs.LG]
(or arXiv:2609.30079v1 [cs.LG] for this version)
https://doi.org/10.48550/arXiv.2609.30079 Focus to learn more arXiv-issued DOI via DataCite (pending registration)
https://doi.org/10.1007/978-3-032-32357-6_13 Focus to learn more DOI(s) linking to related resources
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Full text under the publisher's open licence · 290 words
Related coverage
NNV3: Expanding Neural Network Verification to New Architectures and Domains
arXiv · Sep 25, 2026
TNODEV: Toolbox for Neural ODE Verification
arXiv · Jun 16, 2026
Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes
arXiv · Aug 5, 2026
Safety-Constrained Reinforcement Learning with Post-Training Reachability Verification for Robot Navigation
arXiv · Sep 28, 2026