---
title: "Verifying Quantized Graph Neural Networks is PSPACE-complete"
authors:
  - "Marco Sälzer"
  - "Francois Schwarzentruber"
  - "Nicolas Troquard"
doi: "10.24963/ijcai.2025/519"
url: "https://ijcai.org/proceedings/2025/519"
pdf: "https://ijcai.org/proceedings/2025/0519.pdf"
venue: "Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence"
year: 2025
pages: "4660-4668"
track: "Main Track"
keywords:
  - "Knowledge Representation and Reasoning: KRR: Computational complexity of reasoning"
  - "Machine Learning: ML: Other"
  - "Knowledge Representation and Reasoning: KRR: Automated reasoning and theorem proving"
---

# Verifying Quantized Graph Neural Networks is PSPACE-complete

Marco Sälzer, Francois Schwarzentruber, Nicolas Troquard

*Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence*, pages 4660-4668. DOI: [10.24963/ijcai.2025/519](https://doi.org/10.24963/ijcai.2025/519)

## 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.