Verifying Quantized Graph Neural Networks is PSPACE-complete
Not on the map. Why?
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.
Key facts. Cited by 2 papers in the map (data through 7 Oct 2026). Builds on 15 of its 37 references that are in the map. First posted on arXiv 22 Feb 2025.
Builds on
15 of 37 references.
References · 15
- 2017Graph Attention Networkscited by 8,854
- 2019Fast Graph Representation Learning with PyTorch Geometriccited by 2,414
- 2018Graph Neural Networks: A Review of Methods and Applicationscited by 1,571
- 2021A Survey of Quantization Methods for Efficient Neural Network Inferencecited by 798
- 2020Scalable Verification of Quantized Neural Networks (Technical Report)cited by 28
- 2021Reachability Is NP-Complete Even for the Simplest Neural Networkscited by 27
- 2023The Descriptive Complexity of Graph Neural Networkscited by 26
- 2023Some Might Say All You Need Is Sumcited by 21
- 2024Decidability of Graph Neural Networks via Logical Characterizationscited by 13
- 2024Logical Characterizations of Recurrent Graph Neural Networks with Reals and Floatscited by 13
- 2022QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networkscited by 12
- 2023Towards Efficient Verification of Quantized Neural Networkscited by 10
Built on by
Citing papers per year: 2025: 1; 2026: 1.
2 papers.