Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable

Artem Chernobrovkin; Fran\c{c}ois Schwarzentruber; Marco S\"alzer; Nicolas Troquard

arxiv: 2510.08045 · v2 · submitted 2025-10-09 · 💻 cs.LO · cs.AI· cs.CC· cs.LG

Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable

Artem Chernobrovkin , Marco S\"alzer , Fran\c{c}ois Schwarzentruber , Nicolas Troquard This is my paper

Pith reviewed 2026-05-18 08:48 UTC · model grok-4.3

classification 💻 cs.LO cs.AIcs.CCcs.LG

keywords graph neural networksquantizationverificationcomputational complexitylogical characterizationreadoutNEXPTIME

0 comments

The pith

Verification tasks for quantized graph neural networks with global readout are decidable but (co)NEXPTIME-complete.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a logical language that exactly describes the behavior of quantized aggregate-combine graph neural networks equipped with global readout. It uses this language to deliver a precise characterization of what these networks can compute. From the characterization the authors derive that standard verification questions about the networks belong to the complexity classes NEXPTIME and coNEXPTIME. This places verification in the decidable realm while showing it lies at the upper end of practical tractability. Readers care because GNNs appear in safety-critical settings; the result quantifies how expensive it is to certify that a deployed quantized model will behave as intended.

Core claim

The authors provide a logical language for reasoning about quantized ACR-GNNs with global readout, prove that the language gives a faithful characterization of the networks' semantics, and use the characterization to establish that verification tasks for these networks are (co)NEXPTIME-complete.

What carries the argument

A logical language that supplies a complete characterization of the semantics of quantized ACR-GNNs with global readout.

If this is right

Safety properties of quantized GNNs with readout can be checked algorithmically, yet the check may require exponential resources on worst-case inputs.
Practical verification of large GNN-based systems will need approximation techniques or restrictions on network size or property language.
Quantized ACR-GNN models remain attractive for deployment because experiments show they stay accurate and generalize well while using fewer resources.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The exponential complexity suggests that statistical or sampling-based verification methods may become necessary for real-world graph sizes.
Similar logical characterizations could be attempted for other GNN architectures to classify which variants admit feasible verification.
The result motivates the design of quantization schemes that simultaneously preserve accuracy and reduce the worst-case verification cost.

Load-bearing premise

The introduced logical language correctly and completely captures the semantics of quantized ACR-GNNs with global readout.

What would settle it

A concrete verification problem for a quantized ACR-GNN with readout whose solution lies outside NEXPTIME or coNEXPTIME, or an explicit counter-example showing that the logical language fails to capture some network behavior.

Figures

Figures reproduced from arXiv: 2510.08045 by Artem Chernobrovkin, Fran\c{c}ois Schwarzentruber, Marco S\"alzer, Nicolas Troquard.

**Figure 1.** Figure 1: DAG data structure for the formula agg(x1 + x2) + (x1 + x2) ≥ 3. 3 LOGIC qL We set up a logical framework called qL extending the logic introduced in Sälzer et al. (2025) with global aggregation: it is a lingua franca to represent GNN computations and properties on graphs. Syntax. Let F be a finite set of features and 𝕂 be some finite-width arithmetic. We consider a set of expressions defined by the follow… view at source ↗

**Figure 2.** Figure 2: Encoding a torus of exponential size with (modal) [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗

**Figure 3.** Figure 3: Encoding a torus of exponential size with an [PITH_FULL_IMAGE:figures/full_fig_p024_3.png] view at source ↗

**Figure 4.** Figure 4: Non-linear activation functions that influence were analyzed. [PITH_FULL_IMAGE:figures/full_fig_p030_4.png] view at source ↗

**Figure 5.** Figure 5: Heatmaps of ACR-GNN accuracy across activation functions and network depth. Each row [PITH_FULL_IMAGE:figures/full_fig_p032_5.png] view at source ↗

**Figure 6.** Figure 6: Mean dPTQ speedup (non-dPTQ time / dPTQ time) by activation function and classifier. [PITH_FULL_IMAGE:figures/full_fig_p034_6.png] view at source ↗

**Figure 7.** Figure 7: Heatmaps of ACR-GNN accuracy after applying the dynamic PTQ across activation [PITH_FULL_IMAGE:figures/full_fig_p035_7.png] view at source ↗

**Figure 8.** Figure 8: Training time by depth of the ACR-GNN. The results show substantial variability depending on the activation function. Piecewise activations such as trReLU (187.6 min) and ReLU (204.7 min) yield the fastest training times, while smooth activations such as Softplus (250.1 min), ReLU6 (244.2 min), and SiLU (232.5 min) incur significant overhead. Sigmoid also ranks among the slower functions (229.2 min) [PITH… view at source ↗

**Figure 9.** Figure 9: PPI. Dynamic PTQ Speedup by Activation (mean across layers). [PITH_FULL_IMAGE:figures/full_fig_p040_9.png] view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper proves (co)NEXPTIME-completeness for verifying quantized ACR-GNNs with readout using a new logical characterization.

read the letter

The main point is that verification of safety properties for quantized aggregate-combine GNNs with global readout is (co)NEXPTIME-complete. They reach this by defining a logical language that characterizes the networks and then proving the complexity bound from it. This is new relative to earlier GNN verification results, which did not address the quantized case with readout in this form. The experiments add a practical note by showing that quantization keeps accuracy and generalization close to the full-precision versions while cutting model size. That part is straightforward and useful for anyone thinking about deploying these models. The central assumption is that the logical language fully encodes the quantized aggregate-combine steps and the readout operation, including any discretization effects. If the encoding misses cases such as overflow or certain readout interactions, the complexity result would apply only to the logic rather than the concrete networks. The abstract gives no proof details, so the strength of that link is hard to judge from what is here, but the approach itself is direct and avoids circularity. The paper targets researchers working on formal verification of graph neural networks and on safety for quantized models. A reader focused on complexity bounds for neural architectures would pick up the new (co)NEXPTIME result and the supporting experiments. It has enough formal content and reproducible experimental claims to merit sending out for peer review rather than a desk rejection.

Referee Report

2 major / 3 minor

Summary. The paper introduces a logical language for reasoning about quantized aggregate-combine graph neural networks with global readout (ACR-GNNs). It provides a logical characterization of these models and uses the characterization to prove that verification tasks for quantized GNNs with readout are (co)NEXPTIME-complete. The manuscript also reports experiments showing that quantized ACR-GNN models remain lightweight while preserving accuracy and generalization relative to non-quantized baselines.

Significance. If the logical characterization is faithful to the quantized ACR-GNN semantics, the (co)NEXPTIME-completeness result supplies a tight complexity bound that explains why verification remains intractable even after quantization, motivating further work on approximate or compositional verification techniques for GNN safety. The experimental section supplies supporting evidence that quantization can be applied without catastrophic loss of predictive performance.

major comments (2)

[§4, Theorem 1] §4 (Logical Characterization), Theorem 1: the equivalence between the logic and quantized ACR-GNNs with readout is stated without an explicit argument that the finite quantization levels and global readout aggregation are encoded without omitting saturation or overflow cases; if any such case is missing, the complexity bounds apply only to the logic rather than the concrete model.
[§5] §5 (Complexity Proof), reduction for NEXPTIME-hardness: the construction encodes the GNN computation into the logic, but the proof sketch does not bound the number of distinct quantized values that can arise from repeated aggregate-combine steps before readout; without this bound the reduction may produce an exponential blow-up not present in the original GNN.

minor comments (3)

[§3 and §5] Notation for the readout function is introduced in §3 but reused without redefinition in the complexity section; a single consolidated definition would improve readability.
[Experimental section] The experimental section reports accuracy on standard benchmarks but does not state the precise quantization bit-widths or the number of quantization levels used; these parameters should be listed in a table.
[Introduction] A reference to prior decidability results for non-quantized GNNs is missing from the introduction; adding it would clarify the incremental contribution.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review of our manuscript. We address each major comment below, providing clarifications on the logical characterization and complexity reduction while indicating the revisions we will incorporate to make the arguments fully explicit.

read point-by-point responses

Referee: [§4, Theorem 1] §4 (Logical Characterization), Theorem 1: the equivalence between the logic and quantized ACR-GNNs with readout is stated without an explicit argument that the finite quantization levels and global readout aggregation are encoded without omitting saturation or overflow cases; if any such case is missing, the complexity bounds apply only to the logic rather than the concrete model.

Authors: We agree that an explicit discussion of saturation and overflow handling strengthens the presentation. In the semantics of quantized ACR-GNNs, both aggregate and combine functions operate over a fixed finite set of quantization levels; any operation exceeding the representable range saturates to the extremal value (e.g., max or min of the level set). The logical language mirrors this by restricting all terms and predicates to the same finite domain and by defining the readout aggregation as a direct sum (or other fixed aggregator) over node embeddings that already incorporate saturation. The proof of Theorem 1 proceeds by structural induction that preserves these bounded operations at every step. To address the concern directly, we will add a short subsection in §4 that spells out the encoding of saturation/overflow cases and confirms that the equivalence therefore holds for the concrete quantized model rather than an idealized version. revision: yes
Referee: [§5] §5 (Complexity Proof), reduction for NEXPTIME-hardness: the construction encodes the GNN computation into the logic, but the proof sketch does not bound the number of distinct quantized values that can arise from repeated aggregate-combine steps before readout; without this bound the reduction may produce an exponential blow-up not present in the original GNN.

Authors: The set of admissible values is fixed once and for all by the chosen quantization scheme (a constant, independent of graph size or depth). Consequently, every aggregate-combine step maps the finite domain into itself; no new distinct values are generated beyond the initial quantization levels. The reduction therefore constructs a formula whose size is polynomial in the size of the GNN parameters, the graph, and the fixed quantization bit-width. We acknowledge that the current sketch leaves this invariance implicit. In the revised version we will insert an explicit lemma stating that the value domain remains constant across layers and that the reduction incurs no exponential blow-up in the number of distinct constants. revision: yes

Circularity Check

0 steps flagged

No circularity; logical characterization is independent bridge to complexity result

full rationale

The paper introduces a logical language for quantized ACR-GNNs with readout, provides a logical characterization, and reduces verification to a decision problem in that logic to obtain the (co)NEXPTIME-completeness result. This follows the standard pattern of encoding a computational model into a logic and analyzing the logic's complexity; the characterization is presented as a proven equivalence rather than a definitional tautology. No self-definitional steps, fitted inputs renamed as predictions, or load-bearing self-citations appear in the provided abstract or description. The derivation remains self-contained against external benchmarks of complexity theory, with the fidelity of the encoding serving as a correctness assumption rather than a circular reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the assumption that the newly introduced logical language faithfully models the quantized ACR-GNN semantics; the proof then applies standard results from logic and complexity theory.

axioms (1)

standard math Standard axioms and inference rules of first-order logic and the theory of computational complexity classes
Invoked to establish decidability and to classify the verification problem into coNEXPTIME.

pith-pipeline@v0.9.0 · 5639 in / 1195 out tokens · 35362 ms · 2026-05-18T08:48:08.870152+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

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.
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We introduce a quantized variant of Quantifier-Free Boolean algebra Presburger Arithmetic (QFBAPA) logic, denoted by QFBAPA𝕂, and prove that it is in NP as the original QFBAPA on integers. We then reduce the satisfiability problem of qL to the one of QFBAPA𝕂.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

13 extracted references · 13 canonical work pages

[1]

doi: https://doi.org/10.1016/j.drudis.2021.02.011

ISSN 1359-6446. doi: https://doi.org/10.1016/j.drudis.2021.02.011. URL https://www. sciencedirect.com/science/article/pii/S1359644621000787. Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How powerful are graph neural networks? In7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenRevie...

work page doi:10.1016/j.drudis.2021.02.011 2021
[2]

Letχbe a QFBAPA 𝕂 formula

work page
[3]

For each set expression B appearing in some |B|, guess a non-negative integer number kB in𝕂

work page
[4]

Letχ ′ be a (grounded) formula in which we replaced|B|byk B

work page
[5]

Check that χ′ is true (can be done in poly-time since χ′ is a grounded formula, it is a Boolean formula on variable-free equations and inequations in𝕂)

work page
[6]

We now build a standard QFBAPA formulaδ= V B constraint(B)where: constraint(B) = |B|=k B ifk B <∞ 𝕂 |B| ≥limitifk B = +∞𝕂 wherelimitis the maximum number that is considered as infinity in𝕂

work page
[7]

Accepts if it accepts

Run a non-deterministic poly-time algorithm for the QFBAPA satisfiability on δ. Accepts if it accepts. Otherwise reject. The algorithm runs in poly-time. Guessing a number nB is in poly-time since it consists in guessing n bits (n in unary). Step 4 is just doing the computations in 𝕂. In Step 6, δ can be computed in poly-time. If χ is QFBAPA𝕂 satisfiable,...

work page 2000
[8]

Let φ be a qL

We reduce the satisfiability problem in (modal)qL (restricted to graded modal logic + graded universal modality, because it is sufficient to encode the tiling problem) toVT3 in poly-time as follows. Let φ be a qL. We build in poly-time an ACR-GNN A that recognizes all pointed graphs. We haveφis satisfiable iff[[φ]]∩[[A]]̸=∅SoVT3 is NEXPTIME-hard

work page
[9]

We reduce the validity problem of qL toVT2

The validity problem of qL (dual problem of the satisfiability problem, i.e., given a formula φ, is φ true in all pointed graphs G, u?) is coNEXPTIME-hard. We reduce the validity problem of qL toVT2. Let φ be a qL formula. We construct an ACR-GNN A that accepts all pointed graphs. We haveφis valid iff[[A]]⊆[[φ]]. SoVT2 is coNEXPTIME-hard

work page
[10]

Let ψ be a qL formula

We reduce the validity problem of qL toVT1. Let ψ be a qL formula. (again restricted to graded modal logic + graded global modalities as for point 1). So following Barceló et al. (2020), we can construct in poly-time an ACR-GNN A that is equivalent to ψ (by Barceló et al. (2020)). We haveψis valid iff[[⊤]]⊆[[A]]. SoVT1 is coNEXPTIME-hard. 18 Theorem 14.Th...

work page 2020
[11]

For the lower bound, we reduce (propositional) SAT toVT’3 in poly-time as follows

NP upper bound is also obtained by guessing a graph with at most N vertices and then check. For the lower bound, we reduce (propositional) SAT toVT’3 in poly-time as follows. Let φ be a propositional formula. We build in poly-time an ACR-GNN A that recognizes all pointed graphs. We haveφis satisfiable iff[[φ]]∩[[A]]̸=∅SoVT’3 is NP-hard

work page
[12]

The validity problem of propositional logic (dual problem of the satisfiability problem, i.e., given a formula φ, is φ true for all valuations) is coNP-hard

coNP upper bound corresponds to a NP upper bound for the dual problem: guessing a graph with at most N vertices which is recognizes by A but in which φ does not hold. The validity problem of propositional logic (dual problem of the satisfiability problem, i.e., given a formula φ, is φ true for all valuations) is coNP-hard. We reduce the validity problem o...

work page
[13]

there exist betweenNandMnodes

coNP upper bound is obtained similarly. For the lower bound, we reduce the validity problem of propositional logic toVT’1. Let ψ be a propositional formula. So following Barceló et al. (2020), we can construct in poly-time an ACR-GNN A that is equivalent to ψ (by Barceló et al. (2020)). We haveψis valid iff[[⊤]]⊆[[A]]. SoVT’1 is coNP-hard. B PROTOTYPE VER...

work page 2020

[1] [1]

doi: https://doi.org/10.1016/j.drudis.2021.02.011

ISSN 1359-6446. doi: https://doi.org/10.1016/j.drudis.2021.02.011. URL https://www. sciencedirect.com/science/article/pii/S1359644621000787. Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How powerful are graph neural networks? In7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenRevie...

work page doi:10.1016/j.drudis.2021.02.011 2021

[2] [2]

Letχbe a QFBAPA 𝕂 formula

work page

[3] [3]

For each set expression B appearing in some |B|, guess a non-negative integer number kB in𝕂

work page

[4] [4]

Letχ ′ be a (grounded) formula in which we replaced|B|byk B

work page

[5] [5]

Check that χ′ is true (can be done in poly-time since χ′ is a grounded formula, it is a Boolean formula on variable-free equations and inequations in𝕂)

work page

[6] [6]

We now build a standard QFBAPA formulaδ= V B constraint(B)where: constraint(B) = |B|=k B ifk B <∞ 𝕂 |B| ≥limitifk B = +∞𝕂 wherelimitis the maximum number that is considered as infinity in𝕂

work page

[7] [7]

Accepts if it accepts

Run a non-deterministic poly-time algorithm for the QFBAPA satisfiability on δ. Accepts if it accepts. Otherwise reject. The algorithm runs in poly-time. Guessing a number nB is in poly-time since it consists in guessing n bits (n in unary). Step 4 is just doing the computations in 𝕂. In Step 6, δ can be computed in poly-time. If χ is QFBAPA𝕂 satisfiable,...

work page 2000

[8] [8]

Let φ be a qL

We reduce the satisfiability problem in (modal)qL (restricted to graded modal logic + graded universal modality, because it is sufficient to encode the tiling problem) toVT3 in poly-time as follows. Let φ be a qL. We build in poly-time an ACR-GNN A that recognizes all pointed graphs. We haveφis satisfiable iff[[φ]]∩[[A]]̸=∅SoVT3 is NEXPTIME-hard

work page

[9] [9]

We reduce the validity problem of qL toVT2

The validity problem of qL (dual problem of the satisfiability problem, i.e., given a formula φ, is φ true in all pointed graphs G, u?) is coNEXPTIME-hard. We reduce the validity problem of qL toVT2. Let φ be a qL formula. We construct an ACR-GNN A that accepts all pointed graphs. We haveφis valid iff[[A]]⊆[[φ]]. SoVT2 is coNEXPTIME-hard

work page

[10] [10]

Let ψ be a qL formula

We reduce the validity problem of qL toVT1. Let ψ be a qL formula. (again restricted to graded modal logic + graded global modalities as for point 1). So following Barceló et al. (2020), we can construct in poly-time an ACR-GNN A that is equivalent to ψ (by Barceló et al. (2020)). We haveψis valid iff[[⊤]]⊆[[A]]. SoVT1 is coNEXPTIME-hard. 18 Theorem 14.Th...

work page 2020

[11] [11]

For the lower bound, we reduce (propositional) SAT toVT’3 in poly-time as follows

NP upper bound is also obtained by guessing a graph with at most N vertices and then check. For the lower bound, we reduce (propositional) SAT toVT’3 in poly-time as follows. Let φ be a propositional formula. We build in poly-time an ACR-GNN A that recognizes all pointed graphs. We haveφis satisfiable iff[[φ]]∩[[A]]̸=∅SoVT’3 is NP-hard

work page

[12] [12]

The validity problem of propositional logic (dual problem of the satisfiability problem, i.e., given a formula φ, is φ true for all valuations) is coNP-hard

coNP upper bound corresponds to a NP upper bound for the dual problem: guessing a graph with at most N vertices which is recognizes by A but in which φ does not hold. The validity problem of propositional logic (dual problem of the satisfiability problem, i.e., given a formula φ, is φ true for all valuations) is coNP-hard. We reduce the validity problem o...

work page

[13] [13]

there exist betweenNandMnodes

coNP upper bound is obtained similarly. For the lower bound, we reduce the validity problem of propositional logic toVT’1. Let ψ be a propositional formula. So following Barceló et al. (2020), we can construct in poly-time an ACR-GNN A that is equivalent to ψ (by Barceló et al. (2020)). We haveψis valid iff[[⊤]]⊆[[A]]. SoVT’1 is coNP-hard. B PROTOTYPE VER...

work page 2020