Verifying Graph Neural Networks with Readout is Intractable
This addresses the safety verification problem for GNN-based systems, which is crucial for ensuring reliability in applications like network analysis or autonomous systems, but the result is incremental as it builds on existing verification frameworks.
The paper tackles the verification problem for quantized graph neural networks with readout, proving that verification tasks are (co)NEXPTIME-complete, which implies computational intractability, and experimentally shows that quantized models are lightweight while maintaining good accuracy and generalization.
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.