Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable
Logic in Computer Science
2026-04-28 v2 Artificial Intelligence
Computational Complexity
Machine Learning
Abstract
We introduce a logical language for reasoning about quantized aggregate-combine graph neural networks with global readout (ACR-GNNs). We provide a logical characterization and use it to prove that verification tasks for quantized GNNs with readout are (co)NEXPTIME-complete. This result implies that the verification of quantized GNNs is computationally intractable, prompting substantial research efforts toward ensuring the safety of GNN-based systems. We also experimentally demonstrate that quantized ACR-GNN models are lightweight while maintaining good accuracy and generalization capabilities with respect to non-quantized models.
Cite
@article{arxiv.2510.08045,
title = {Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable},
author = {Artem Chernobrovkin and Marco Sälzer and François Schwarzentruber and Nicolas Troquard},
journal= {arXiv preprint arXiv:2510.08045},
year = {2026}
}