Verifying Quantized Graph Neural Networks is PSPACE-complete
This addresses the problem of ensuring reliability in quantized GNNs for AI safety and formal methods, but it is incremental as it builds on existing verification work.
The paper tackles the verification of quantized Graph Neural Networks (GNNs) using fixed-width arithmetic, showing that the linear-constrained validity (LVP) problem for verifying GNN properties is PSPACE-complete, indicating feasibility but computational challenge.
In this paper, we investigate the verification of quantized Graph Neural Networks (GNNs), where some fixed-width arithmetic is used to represent numbers. We introduce the linear-constrained validity (LVP) problem for verifying GNNs properties, and provide an efficient translation from LVP instances into a logical language. We show that LVP is in PSPACE, for any reasonable activation functions. We provide a proof system. We also prove PSPACE-hardness, indicating that while reasoning about quantized GNNs is feasible, it remains generally computationally challenging.