Verifying Graph Neural Networks with Readout is Intractable

TL;DR

The paper investigates the formal verification of quantized GNNs with global readout by introducing the modal quantized logic $q\mathcal{L}$ and proving that ACR-GNN verification tasks are (co)NEXPTIME-complete, establishing inherent intractability in general. To address practicality, it proves NP-bounded variants by bounding the number of vertices and develops a prototype verifier, showing feasibility at small scales. The work also demonstrates that quantized ACR-GNNs can achieve substantial size reductions (through dynamic PTQ) with minimal accuracy loss on synthetic and biological graphs, suggesting practicality for resource-constrained deployments. Collectively, these results delineate the theoretical limits of GNN verification while providing a concrete, quantifiable pathway to usable, quantized GNNs in constrained environments and guiding future research toward scalable verification techniques.

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.

Figures (9)

• Figure 1: DAG data structure for the formula $agg(x_1 + x_2) + (x_1 + x_2) \geq 3$.
• Figure 2: Encoding a torus of exponential size with (modal) $q\mathcal{L}$ formulas. Vertices $u_{x, y}$ correspond to locations $(x, y)$ in the torus while $u_N$ and $u_E$ denote intermediate vertices indicating the direction (resp., north and east).
• Figure 3: Encoding a torus of exponential size with an $\mathcal{ALCQ}$-$T_C$Box with one role.
• Figure 4: Non-linear activation functions that influence were analyzed.
• Figure 5: Heatmaps of ACR-GNN accuracy across activation functions and network depth. Each row corresponds to a metric (Train, Test1, Test2), while each column corresponds to a dataset classifier ($p_1$, $p_2$, $p_3$). Color intensity indicates classification accuracy.

Theorems & Definitions (49)

• example 1
• example 2: continues Example \ref{['ex:animals-humans']}
• lemma 2
• theorem 3
• definition 4
• example 5
• proposition 5
• proposition 5
• proposition 5
• proposition 5