# Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable

arXiv: https://arxiv.org/abs/2510.08045 · HTML: https://mlsanity.com/paper/2510.08045/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- First posted on arXiv 9 Oct 2025.

## Abstract (arXiv)

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.