# Fundamental Limits in Formal Verification of Message-Passing Neural Networks

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 32 references that are in the map.
- First posted on arXiv 10 Jun 2022.

## Builds on (most cited first, 20 of 20)

- [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)
- [A Comprehensive Survey on Graph Neural Networks](https://mlsanity.com/paper/1901.00596/) (2019)
- [Graph Neural Networks: A Review of Methods and Applications](https://mlsanity.com/paper/1812.08434/) (2018)
- [Weisfeiler and Leman Go Neural: Higher-order Graph Neural Networks](https://mlsanity.com/paper/1810.02244/) (2018)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Graph Neural Networks for Social Recommendation](https://mlsanity.com/paper/1902.07243/) (2019)
- [Adversarial Attacks on Neural Networks for Graph Data](https://mlsanity.com/paper/1805.07984/) (2018)
- [Neural Relational Inference for Interacting Systems](https://mlsanity.com/paper/1802.04687/) (2018)
- [Adversarial Attack on Graph Structured Data](https://mlsanity.com/paper/1806.02371/) (2018)
- [Adversarial Attacks on Graph Neural Networks via Meta Learning](https://mlsanity.com/paper/1902.08412/) (2019)
- [What graph neural networks cannot learn: depth vs width](https://mlsanity.com/paper/1907.03199/) (2019)
- [DropGNN: Random Dropouts Increase the Expressiveness of Graph Neural Networks](https://mlsanity.com/paper/2111.06283/) (2021)
- [Robustness of Graph Neural Networks at Scale](https://mlsanity.com/paper/2110.14038/) (2021)
- [The Logic of Graph Neural Networks](https://mlsanity.com/paper/2104.14624/) (2021)
- [Towards More Practical Adversarial Attacks on Graph Neural Networks](https://mlsanity.com/paper/2006.05057/) (2020)
- [Efficient Robustness Certificates for Discrete Data: Sparsity-Aware Randomized Smoothing for Graphs, Images and More](https://mlsanity.com/paper/2008.12952/) (2020)
- [Scalable Attack on Graph Data by Injecting Vicious Nodes](https://mlsanity.com/paper/2004.13825/) (2020)
- [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021)
- [Indirect Adversarial Attacks via Poisoning Neighbors for Graph Convolutional Networks](https://mlsanity.com/paper/2002.08012/) (2020)

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

- [Verifying message-passing neural networks via topology-based bounds tightening](https://mlsanity.com/paper/2402.13937/) (2024)
- [Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure](https://mlsanity.com/paper/2404.15065/) (2024)
- [Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning](https://mlsanity.com/paper/2405.18548/) (2024)
- [Exact Verification of Graph Neural Networks with Incremental Constraint Solving](https://mlsanity.com/paper/2508.09320/) (2025)
- [Verifying Quantized Graph Neural Networks is PSPACE-complete](https://mlsanity.com/paper/2502.16244/) (2025)
- [Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits](https://mlsanity.com/paper/2512.20755/) (2025)
- [The μG Language for Programming Graph Neural Networks](https://mlsanity.com/paper/2407.09441/) (2024)
- [Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing](https://mlsanity.com/paper/2510.18591/) (2025)
- [Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features](https://mlsanity.com/paper/2609.30079/) (2026)

## Abstract (arXiv)

Output reachability and adversarial robustness are among the most relevant safety properties of neural networks. We show that in the context of Message Passing Neural Networks (MPNN), a common Graph Neural Network (GNN) model, formal verification is impossible. In particular, we show that output reachability of graph-classifier MPNN, working over graphs of unbounded size, non-trivial degree and sufficiently expressive node labels, cannot be verified formally: there is no algorithm that answers correctly (with yes or no), given an MPNN, whether there exists some valid input to the MPNN such that the corresponding output satisfies a given specification. However, we also show that output reachability and adversarial robustness of node-classifier MPNN can be verified formally when a limit on the degree of input graphs is given a priori. We discuss the implications of these results, for the purpose of obtaining a complete picture of the principle possibility to formally verify GNN, depending on the expressiveness of the involved GNN models and input-output specifications.