{"ID":2858070,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2510.08045","arxiv_id":"2510.08045","title":"Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable","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.","short_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...","url_abs":"https://arxiv.org/abs/2510.08045","url_pdf":"https://arxiv.org/pdf/2510.08045v2","authors":"[\"Artem Chernobrovkin\",\"Marco Sälzer\",\"François Schwarzentruber\",\"Nicolas Troquard\"]","published":"2025-10-09T10:29:09Z","proceeding":"cs.LO","tasks":"[\"cs.LO\",\"cs.AI\",\"cs.CC\",\"cs.LG\"]","methods":"[\"Graph Neural Network\"]","has_code":false}