mlsanityData to 7 Oct 2026

Fundamental Limits in Formal Verification of Message-Passing Neural Networks

arXiv 2206.05070 ↗First posted 10 Jun 2022cs.LG cs.LOcited by 9

Not on the map. Why?

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.

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

Builds on

20 of 32 references.

References · 20

  1. 2018How Powerful are Graph Neural Networks?cited by 4,355
  2. 2017Neural Message Passing for Quantum Chemistrycited by 3,460
  3. 2019A Comprehensive Survey on Graph Neural Networkscited by 2,906
  4. 2018Graph Neural Networks: A Review of Methods and Applicationscited by 1,571
  5. 2018Weisfeiler and Leman Go Neural: Higher-order Graph Neural Networkscited by 878
  6. 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 739
  7. 2019Graph Neural Networks for Social Recommendationcited by 711
  8. 2018Adversarial Attacks on Neural Networks for Graph Datacited by 395
  9. 2018Neural Relational Inference for Interacting Systemscited by 339
  10. 2018Adversarial Attack on Graph Structured Datacited by 300
  11. 2019Adversarial Attacks on Graph Neural Networks via Meta Learningcited by 261
  12. 2019What graph neural networks cannot learn: depth vs widthcited by 195
8 more
  1. 2021DropGNN: Random Dropouts Increase the Expressiveness of Graph Neural Networkscited by 117
  2. 2021Robustness of Graph Neural Networks at Scalecited by 100
  3. 2021The Logic of Graph Neural Networkscited by 84
  4. 2020Towards More Practical Adversarial Attacks on Graph Neural Networkscited by 76
  5. 2020Efficient Robustness Certificates for Discrete Data: Sparsity-Aware Randomized Smoothing for Graphs, Images and Morecited by 56
  6. 2020Scalable Attack on Graph Data by Injecting Vicious Nodescited by 50
  7. 2021Reachability Is NP-Complete Even for the Simplest Neural Networkscited by 27
  8. 2020Indirect Adversarial Attacks via Poisoning Neighbors for Graph Convolutional Networkscited by 16

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 4; 2025: 4; 2026: 1.

9 papers.

  1. 2024Verifying message-passing neural networks via topology-based bounds tighteningcited by 10
  2. 2024Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structurecited by 8
  3. 2024Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoningcited by 5
  4. 2025Exact Verification of Graph Neural Networks with Incremental Constraint Solvingcited by 4
  5. 2025Verifying Quantized Graph Neural Networks is PSPACE-completecited by 2
  6. 2025Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exitscited by 1
  7. 2024The μG Language for Programming Graph Neural Networkscited by 0
  8. 2025Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testingcited by 0
  9. 2026Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Featurescited by 0