Verifying Quantized Graph Neural Networks Is PSPACE-Complete
Abstract
In this paper, we investigate 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
Text
Sälzer et al. "Verifying Quantized Graph Neural Networks Is PSPACE-Complete." International Joint Conference on Artificial Intelligence, 2025. doi:10.24963/IJCAI.2025/519Markdown
[Sälzer et al. "Verifying Quantized Graph Neural Networks Is PSPACE-Complete." International Joint Conference on Artificial Intelligence, 2025.](https://mlanthology.org/ijcai/2025/salzer2025ijcai-verifying/) doi:10.24963/IJCAI.2025/519BibTeX
@inproceedings{salzer2025ijcai-verifying,
title = {{Verifying Quantized Graph Neural Networks Is PSPACE-Complete}},
author = {Sälzer, Marco and Schwarzentruber, François and Troquard, Nicolas},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2025},
pages = {4660-4668},
doi = {10.24963/IJCAI.2025/519},
url = {https://mlanthology.org/ijcai/2025/salzer2025ijcai-verifying/}
}