# Exact Verification of Graph Neural Networks with Incremental Constraint Solving

arXiv: https://arxiv.org/abs/2508.09320 · HTML: https://mlsanity.com/paper/2508.09320/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 64 of its 91 references that are in the map.
- First posted on arXiv 12 Aug 2025.

## Builds on (most cited first, 30 of 64)

- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [How Powerful are Graph Neural Networks?](https://mlsanity.com/paper/1810.00826/) (2018)
- [Neural Message Passing for Quantum Chemistry](https://mlsanity.com/paper/1704.01212/) (2017)
- [Fast Graph Representation Learning with PyTorch Geometric](https://mlsanity.com/paper/1903.02428/) (2019)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges](https://mlsanity.com/paper/2104.13478/) (2021)
- [Graph Convolutional Neural Networks for Web-Scale Recommender Systems](https://mlsanity.com/paper/1806.01973/) (2018)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [TUDataset: A collection of benchmark datasets for learning with graphs](https://mlsanity.com/paper/2007.08663/) (2020)
- [Principal Neighbourhood Aggregation for Graph Nets](https://mlsanity.com/paper/2004.05718/) (2020)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Adversarial Attacks on Neural Networks for Graph Data](https://mlsanity.com/paper/1805.07984/) (2018)
- [Adversarial Attack on Graph Structured Data](https://mlsanity.com/paper/1806.02371/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Adversarial Attacks on Graph Neural Networks via Meta Learning](https://mlsanity.com/paper/1902.08412/) (2019)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Topology Attack and Defense for Graph Neural Networks: An Optimization Perspective](https://mlsanity.com/paper/1906.04214/) (2019)
- [GNNGuard: Defending Graph Neural Networks against Adversarial Attacks](https://mlsanity.com/paper/2006.08149/) (2020)
- [Graph neural networks for materials science and chemistry](https://mlsanity.com/paper/2208.09481/) (2022)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [A Semi-supervised Graph Attentive Network for Financial Fraud Detection](https://mlsanity.com/paper/2003.01171/) (2020)
- [Backdoor Attacks to Graph Neural Networks](https://mlsanity.com/paper/2006.11165/) (2020)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [From Amateurs to Connoisseurs: Modeling the Evolution of User Expertise through Online Reviews](https://mlsanity.com/paper/1303.4402/) (2013)
- [Spatially-Aware Graph Neural Networks for Relational Behavior Forecasting from Sensor Data](https://mlsanity.com/paper/1910.08233/) (2019)
- [Robustness of Graph Neural Networks at Scale](https://mlsanity.com/paper/2110.14038/) (2021)
- [Graph Adversarial Training: Dynamically Regularizing Based on Graph Structure](https://mlsanity.com/paper/1902.08226/) (2019)
- [Graph Representation Learning in Biomedicine](https://mlsanity.com/paper/2104.04883/) (2021)
- [Robustness Verification for Transformers](https://mlsanity.com/paper/2002.06622/) (2020)

## Built on by (most cited first, 4 of 4)

- [Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing](https://mlsanity.com/paper/2510.18591/) (2025)
- [Exploring Solver-Level Warmstarting for Neural Network Verification](https://mlsanity.com/paper/2609.25962/) (2026)
- [NNV3: Expanding Neural Network Verification to New Architectures and Domains](https://mlsanity.com/paper/2609.30050/) (2026)
- [Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features](https://mlsanity.com/paper/2609.30079/) (2026)

## Abstract (arXiv)

Graph neural networks (GNNs) are increasingly often employed in high-stakes applications, such as fraud detection or healthcare, but are susceptible to adversarial attacks. A number of techniques have been proposed to provide adversarial robustness guarantees, but support for commonly used aggregation functions in message-passing GNNs is lacking. In this paper, we develop an exact (sound and complete) verification method for GNNs to compute guarantees against attribute and structural perturbations that involve edge addition or deletion, subject to budget constraints. Our method employs constraint solving with bound tightening, and iteratively solves a sequence of relaxed constraint satisfaction problems while relying on incremental solving capabilities of solvers to improve efficiency. We implement GNNev, a versatile exact verifier for message-passing neural networks, which supports three aggregation functions -- sum, max and mean -- with the latter two considered here for the first time. Extensive experimental evaluation of GNNev on real-world fraud datasets (Amazon and Yelp) and biochemical datasets (MUTAG and ENZYMES) demonstrates its usability and effectiveness, as well as superior performance on node classification and competitiveness on graph classification compared to existing exact verification tools on sum-aggregated GNNs.