# Verifying Quantized Graph Neural Networks is PSPACE-complete

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 37 references that are in the map.
- First posted on arXiv 22 Feb 2025.

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

- [Graph Attention Networks](https://mlsanity.com/paper/1710.10903/) (2017)
- [Fast Graph Representation Learning with PyTorch Geometric](https://mlsanity.com/paper/1903.02428/) (2019)
- [Graph Neural Networks: A Review of Methods and Applications](https://mlsanity.com/paper/1812.08434/) (2018)
- [A Survey of Quantization Methods for Efficient Neural Network Inference](https://mlsanity.com/paper/2103.13630/) (2021)
- [Scalable Verification of Quantized Neural Networks (Technical Report)](https://mlsanity.com/paper/2012.08185/) (2020)
- [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021)
- [The Descriptive Complexity of Graph Neural Networks](https://mlsanity.com/paper/2303.04613/) (2023)
- [Some Might Say All You Need Is Sum](https://mlsanity.com/paper/2302.11603/) (2023)
- [Decidability of Graph Neural Networks via Logical Characterizations](https://mlsanity.com/paper/2404.18151/) (2024)
- [Logical Characterizations of Recurrent Graph Neural Networks with Reals and Floats](https://mlsanity.com/paper/2405.14606/) (2024)
- [QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks](https://mlsanity.com/paper/2212.11138/) (2022)
- [Towards Efficient Verification of Quantized Neural Networks](https://mlsanity.com/paper/2312.12679/) (2023)
- [A Logic for Reasoning About Aggregate-Combine Graph Neural Networks](https://mlsanity.com/paper/2405.00205/) (2024)
- [Fundamental Limits in Formal Verification of Message-Passing Neural Networks](https://mlsanity.com/paper/2206.05070/) (2022)
- [On Classical Decidable Logics extended with Percentage Quantifiers and Arithmetics](https://mlsanity.com/paper/2106.15250/) (2021)

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

- [The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics](https://mlsanity.com/paper/2505.11930/) (2025)
- [Clausal Deletion Backdoors for QBF: a Parameterized Complexity Approach](https://mlsanity.com/paper/2605.12073/) (2026)

## Abstract (arXiv)

In this paper, we investigate the verification of quantized Graph Neural Networks (GNNs), where some fixed-width arithmetic is used to represent numbers. We introduce the linear-constrained validity (LVP) problem for verifying GNNs properties, and provide an efficient translation from LVP instances into a logical language. We show that LVP is in PSPACE, for any reasonable activation functions. We provide a proof system. We also prove PSPACE-hardness, indicating that while reasoning about quantized GNNs is feasible, it remains generally computationally challenging.