Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable
Not on the map. Why?
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.
Key facts. No citing papers in the map yet (data through 14 Oct 2026). First posted on arXiv 9 Oct 2025.
Builds on
0 of 0 references.
No references here yet.
Built on by
Not cited yet.
Similar, not cited
Close in wording, no citation either way
- 2025Verifying Quantized Graph Neural Networks is PSPACE-complete
- 2023rm A2Q: Aggregation-Aware Quantization for Graph Neural Networks
- 2025Efficient Mixed Precision Quantization in Graph Neural Networks
- 2023Towards Efficient Verification of Quantized Neural Networks
- 2023Low-bit Quantization for Deep Graph Neural Networks with Smoothness-aware Message Propagation
- 2026TopGQ: Fast GNN Post-Training Quantization Leveraging Topology Information
- 2023Tango: rethinking quantization for graph neural network training on GPUs
- 2023MEGA: A Memory-Efficient GNN Accelerator Exploiting Degree-Aware Mixed-Precision Quantization