Verifying Quantized Graph Neural Networks is PSPACE-complete
Logic in Computer Science
2025-08-14 v2 Computational Complexity
Machine Learning
Abstract
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.
Cite
@article{arxiv.2502.16244,
title = {Verifying Quantized Graph Neural Networks is PSPACE-complete},
author = {Marco Sälzer and François Schwarzentruber and Nicolas Troquard},
journal= {arXiv preprint arXiv:2502.16244},
year = {2025}
}
Comments
In 34th International Joint Conference on Artificial Intelligence (IJCAI 2025)