Verifying Quantized Graph Neural Networks is PSPACE-complete
Authors: Marco Sälzer, Francois Schwarzentruber, Nicolas Troquard
IJCAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | 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. |
| Researcher Affiliation | Academia | 1 Technical University of Kaiserslautern, Kaiserslautern, Germany 2ENS de Lyon, CNRS, Universit e Claude Bernard Lyon 1, Inria, LIP, UMR 5668, 69342, Lyon, France 3Gran Sasso Science Institute (GSSI), Viale F. Crispi, 7 67100 L Aquila, Italy |
| Pseudocode | Yes | Figure 4: Tableau rules for the satisfiability problem in Lquant GNN when δ is written in unary. |
| Open Source Code | Yes | A prototype implementation1 of the proof system is presented in [S alzer et al., 2025]. 1https://github.com/francoisschwarzentruber/ijcai2025-verifquantgnn |
| Open Datasets | No | The paper focuses on theoretical verification of GNNs and introduces a logical framework. It does not perform experiments on specific datasets and therefore does not provide access information for any. |
| Dataset Splits | No | The paper is theoretical and does not involve experimental evaluation on datasets. Therefore, it does not describe dataset splits. |
| Hardware Specification | No | The paper is purely theoretical, focusing on logical frameworks and complexity proofs for GNN verification. It does not describe any experiments that would require specific hardware specifications. |
| Software Dependencies | No | The paper mentions a prototype implementation of the proof system in Python via a GitHub link, but it does not specify version numbers for Python or any specific libraries/solvers used in that implementation. It mentions PyTorch Geometric as a third-party library for general GNNs but not as a specific dependency for its own methodology with version. |
| Experiment Setup | No | The paper presents theoretical work on verifying quantized GNNs and does not include experimental results or a detailed experimental setup with hyperparameters or training configurations. |