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.

翻译：我们提出了一种用于推理含全局读出层的量化聚合-组合图神经网络（ACR-GNN）的逻辑语言。我们给出了该语言的逻辑刻画，并据此证明了含读出层的量化GNN验证任务属于（共）NEXPTIME完全问题。该结果表明，量化GNN的验证在计算上具有高度难解性，这将促使大量研究工作致力于保障基于GNN系统的安全性。我们还通过实验证明，与非量化模型相比，量化ACR-GNN模型在保持轻量化的同时，仍具有优秀的准确率和泛化能力。