pith. sign in

arxiv: 2508.09320 · v3 · pith:6ADZ2FTXnew · submitted 2025-08-12 · 💻 cs.LG · cs.AI· cs.CR

Exact Verification of Graph Neural Networks with Incremental Constraint Solving

Minghao Liu , Chia-Hsuan Lu , Marta Kwiatkowska This is my paper

Pith reviewed 2026-05-18 22:54 UTC · model grok-4.3

classification 💻 cs.LG cs.AIcs.CR
keywords graph neural networksexact verificationadversarial robustnessconstraint solvingstructural perturbationsincremental solvingmessage passingnode classification
0
0 comments X

The pith

Exact verification computes sound guarantees for GNNs against both node attribute changes and budgeted edge additions or deletions.

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

The paper develops an exact verification technique for graph neural networks that provides guarantees against both changes to node attributes and structural changes like adding or removing edges, all within a given budget. It achieves this by turning the verification problem into a series of constraint satisfaction problems that are solved incrementally with bound tightening to keep the process efficient. This matters because GNNs are used in critical areas like fraud detection, where attackers might try to fool the model by altering data or connections, and exact methods give stronger assurances than approximate ones. The approach supports common aggregation functions including sum, max, and mean.

Core claim

We develop an exact (sound and complete) verification method for GNNs to compute guarantees against attribute and structural perturbations that involve edge addition or deletion, subject to budget constraints. Our method employs constraint solving with bound tightening, and iteratively solves a sequence of relaxed constraint satisfaction problems while relying on incremental solving capabilities of solvers to improve efficiency. We implement GNNev, a versatile exact verifier for message-passing neural networks, which supports three aggregation functions -- sum, max and mean -- with the latter two considered here for the first time.

What carries the argument

Incremental constraint solving on a sequence of relaxed problems with bound tightening, which enables sound and complete verification for message-passing GNNs under attribute and structural perturbations.

If this is right

  • The method certifies robustness for node classification on real fraud datasets such as Amazon and Yelp.
  • It extends to graph classification tasks on biochemical datasets including MUTAG and ENZYMES.
  • First-time exact verification support is provided for max and mean aggregation functions.
  • Performance is superior to prior exact tools on sum-aggregated GNNs and competitive overall.

Where Pith is reading between the lines

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

  • The incremental solving strategy could extend to verification of GNNs with additional perturbation types such as node insertions.
  • Efficiency improvements may allow scaling the verifier to graphs larger than those tested if solver overhead stays low.
  • The formulation might combine with training-time regularization to produce GNNs that are easier to verify.

Load-bearing premise

Modern constraint solvers can efficiently process the sequence of relaxed problems while preserving soundness and completeness for sum, max, and mean aggregations.

What would settle it

A concrete graph and GNN where the verifier certifies no change in output under any perturbation within the budget, yet an explicit edge or attribute change within the budget is shown to flip the prediction.

Figures

Figures reproduced from arXiv: 2508.09320 by Chia-Hsuan Lu, Marta Kwiatkowska, Minghao Liu.

Figure 1
Figure 1. Figure 1: An illustration of tightened bound propagation. [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Comparison of runtime (in seconds) for sum [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The number of tasks solved by GNNEV plotted against runtime under different aggregations and budgets. Only edge deletions are allowed, and all edges are set as fragile. The verification objective is as defined in Section 4.1, Eq. (14). evaluation of the number of nodes verified plotted against an increasing global budget, shown in [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The number of tasks solved by GNNEV plotted against runtime under different aggregations and budgets. Only edge additions are allowed, and one non-edge to each node is selected as fragile. Dataset aggr GNNEV GNNEV w/o IS #Win Time(s) #Win Time(s) All instances Cora sum 1,743 7.84 965 9.21 max 1,313 19.81 1,383 20.57 mean 1,532 32.06 1,176 34.88 CiteSeer sum 2,491 10.09 821 13.35 max 1,989 28.47 1,222 29.82… view at source ↗
Figure 5
Figure 5. Figure 5: The evolution of the number of robust and nonrobust nodes verified by GNN [PITH_FULL_IMAGE:figures/full_fig_p016_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: The evolution of the number of robust and nonrobust nodes verified by GNN [PITH_FULL_IMAGE:figures/full_fig_p017_6.png] view at source ↗
read the original abstract

Graph neural networks (GNNs) are increasingly often employed in high-stakes applications, such as fraud detection or healthcare, but are susceptible to adversarial attacks. A number of techniques have been proposed to provide adversarial robustness guarantees, but support for commonly used aggregation functions in message-passing GNNs is lacking. In this paper, we develop an exact (sound and complete) verification method for GNNs to compute guarantees against attribute and structural perturbations that involve edge addition or deletion, subject to budget constraints. Our method employs constraint solving with bound tightening, and iteratively solves a sequence of relaxed constraint satisfaction problems while relying on incremental solving capabilities of solvers to improve efficiency. We implement GNNev, a versatile exact verifier for message-passing neural networks, which supports three aggregation functions -- sum, max and mean -- with the latter two considered here for the first time. Extensive experimental evaluation of GNNev on real-world fraud datasets (Amazon and Yelp) and biochemical datasets (MUTAG and ENZYMES) demonstrates its usability and effectiveness, as well as superior performance on node classification and competitiveness on graph classification compared to existing exact verification tools on sum-aggregated GNNs.

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.

Referee Report

2 major / 3 minor

Summary. The paper claims to develop an exact (sound and complete) verification method called GNNev for message-passing GNNs against combined attribute and structural perturbations (edge additions/deletions subject to a budget). It employs incremental constraint solving with bound tightening to iteratively solve relaxed CSPs, supporting sum, max, and mean aggregations (the latter two for the first time in this context). Experiments on fraud datasets (Amazon, Yelp) and biochemical datasets (MUTAG, ENZYMES) demonstrate usability, effectiveness, and superior performance on node classification compared to prior exact tools for sum-aggregated GNNs.

Significance. If the soundness and completeness claims hold, the work is significant as it extends exact verification to mean and max aggregations under structural attacks, addressing a practical gap for GNNs in high-stakes applications like fraud detection. The incremental solving technique provides a pragmatic efficiency improvement while aiming to retain exactness, and the real-world dataset experiments offer concrete evidence of applicability beyond synthetic cases.

major comments (2)
  1. [§3.3] §3.3 (Incremental Verification Procedure): The central claim of completeness for structural perturbations with mean aggregation relies on the refinement loop eventually covering all feasible neighbor-set configurations within the budget. The description of initial relaxations (e.g., ignoring some cardinality constraints) and subsequent tightening does not include a formal argument or termination proof showing that no valid edge-add/delete solution is missed, which is load-bearing for the exactness guarantee.
  2. [§3.2] §3.2 (Constraint Encoding for Aggregations): For max and mean aggregations under edge deletions, the encoding of variable degrees and adjacency must preserve the global perturbation budget. The paper sketches the relaxed problems but does not demonstrate (via proof sketch or exhaustive case analysis) that incremental solver calls yield the exact robustness result rather than a spurious unsat due to incomplete tightening.
minor comments (3)
  1. [Abstract] Abstract: The statement that max and mean are 'considered here for the first time' would benefit from a brief comparison to the closest prior exact verifiers to clarify the novelty.
  2. [§5] §5 (Experiments): Runtime tables would be clearer with error bars or statistics over multiple runs, especially given solver variability on structural perturbation instances.
  3. [Figure 2] Figure 2: The flowchart of the relaxation sequence could include explicit labels for which constraints are relaxed in each iteration to aid reader understanding.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and constructive comments on our manuscript. The concerns regarding the formal justification of completeness and exactness are well-taken, and we will strengthen the presentation in the revised version by adding explicit arguments and proof sketches. We address each major comment below.

read point-by-point responses

  1. Referee: [§3.3] §3.3 (Incremental Verification Procedure): The central claim of completeness for structural perturbations with mean aggregation relies on the refinement loop eventually covering all feasible neighbor-set configurations within the budget. The description of initial relaxations (e.g., ignoring some cardinality constraints) and subsequent tightening does not include a formal argument or termination proof showing that no valid edge-add/delete solution is missed, which is load-bearing for the exactness guarantee.

    Authors: We agree that an explicit formal argument for termination and completeness would improve the rigor of Section 3.3. The refinement procedure begins with a relaxation that ignores certain cardinality constraints on neighbor sets and iteratively tightens bounds using the incremental solver's ability to reuse learned clauses. Because each tightening step adds constraints that exclude only provably infeasible configurations (while preserving all solutions within the perturbation budget), and the space of possible neighbor-set modifications is finite, the loop is guaranteed to terminate. When it reports unsat, no feasible configuration remains; when it finds a satisfying assignment, a concrete perturbation is exhibited. In the revision we will add a dedicated paragraph (and an appendix proof sketch) establishing monotonicity of the relaxations and finiteness of the configuration space to make this argument self-contained. revision: yes

  2. Referee: [§3.2] §3.2 (Constraint Encoding for Aggregations): For max and mean aggregations under edge deletions, the encoding of variable degrees and adjacency must preserve the global perturbation budget. The paper sketches the relaxed problems but does not demonstrate (via proof sketch or exhaustive case analysis) that incremental solver calls yield the exact robustness result rather than a spurious unsat due to incomplete tightening.

    Authors: We acknowledge that the current text provides only a high-level sketch of the encodings for max and mean aggregations under deletions. The global budget is maintained by introducing an auxiliary integer variable that accumulates the total number of edge deletions (and additions) across all nodes; each local degree variable is linked to this global counter via linear inequalities. Because the incremental solver calls operate on successively tighter but still sound relaxations of the same overall constraint system, any unsat result is inherited from the original problem and cannot be spurious. We will augment Section 3.2 with a short proof sketch and a small exhaustive case analysis for the deletion-only setting to demonstrate that the budget constraint is never violated and that completeness is retained. revision: yes

Circularity Check

0 steps flagged

No circularity: verification derives from standard CSP encoding and solver primitives

full rationale

The paper's central contribution is an exact verifier that encodes GNN message-passing (including mean and max aggregations) as constraint satisfaction problems over attribute and structural perturbations, then solves a sequence of relaxations using incremental solver capabilities. No equation or claim reduces by construction to a fitted parameter, self-defined quantity, or load-bearing self-citation; soundness and completeness follow from the standard properties of the underlying constraint solver once the encoding is shown to be faithful. The approach is self-contained against external benchmarks of CSP theory and does not rename known results or smuggle ansatzes via prior work by the same authors.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on standard properties of constraint solvers and bound propagation; no free parameters or new entities are introduced in the abstract.

axioms (1)
  • domain assumption Modern constraint solvers support efficient incremental solving of successive relaxed problems
    Efficiency claim depends on solver reuse behavior that is assumed rather than proven in the abstract.

pith-pipeline@v0.9.0 · 5742 in / 1164 out tokens · 40786 ms · 2026-05-18T22:54:10.511716+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

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

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

15 extracted references · 15 canonical work pages · 1 internal anchor

  1. [1]

    InPLDI 2021, 466–481

    Fast and precise certification of transformers. InPLDI 2021, 466–481. Boopathy, A.; Weng, T.; Chen, P.; Liu, S.; and Daniel, L

    work page 2021

  2. [2]

    In AAAI 2019, 3240–3247

    CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks. In AAAI 2019, 3240–3247. Botoeva, E.; Kouvaros, P.; Kronqvist, J.; Lomuscio, A.; and Misener, R. 2020. Efficient Verification of ReLU-Based Neural Networks via Dependency Analysis. In AAAI 2020, 3291–3299. Bronstein, M. M.; Bruna, J.; Cohen, T.; and Velickovic, P

    work page 2019

  3. [3]

    Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges

    Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges. CoRR, abs/2104.13478. Bunel, R.; Turkaslan, I.; Torr, P. H. S.; Kohli, P.; and Mudigonda, P. K. 2018. A Unified View of Piecewise Linear Neural Network Verification. In NeurIPS 2018, 4795–4804. Cai, P.; Wang, H.; Sun, Y .; and Liu, M. 2021. DiGNet: Learning Scalable Self-Driving Polici...

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  4. [4]

    Neural Networks Learn

    Medical-Knowledge-Based Graph Neural Network for Medication Combination Prediction.IEEE Trans. Neural Networks Learn. Syst., 35(10): 13246–13257. Geisler, S.; Schmidt, T.; S ¸irin, H.; Z¨ugner, D.; Bojchevski, A.; and G ¨unnemann, S. 2021. Robustness of Graph Neural Networks at Scale. In NeurIPS 2021. Gilmer, J.; Schoenholz, S. S.; Riley, P. F.; Vinyals, ...

    work page 2021

  5. [5]

    In IJCAI 2024, 3532–3540

    A Logic for Reasoning about Aggregate-Combine Graph Neural Networks. In IJCAI 2024, 3532–3540. Osselin, P.; Kenlay, H.; and Dong, X. 2023. Structure-aware robustness certificates for graph classification. In UAI 2023, 1596–1605. Rayana, S.; and Akoglu, L. 2015. Collective Opinion Spam Detection: Bridging Review Networks and Metadata. In KDD 2015, 985–994....

    work page 2024

  6. [6]

    In NeurIPS 2019, 9832–9842

    A Convex Relaxation Barrier to Tight Robustness Ver- ification of Neural Networks. In NeurIPS 2019, 9832–9842. S¨alzer, M.; and Lange, M. 2023. Fundamental Limits in Formal Verification of Message-Passing Neural Networks. In ICLR 2023. Scholten, Y .; Schuchardt, J.; Geisler, S.; Bojchevski, A.; and G¨unnemann, S. 2022. Randomized Message-Interception Smoo...

    work page arXiv 2019

  7. [7]

    In ICLR 2020

    Robustness Verification for Transformers. In ICLR 2020. Tao, S.; Cao, Q.; Shen, H.; Huang, J.; Wu, Y .; and Cheng, X

    work page 2020

  8. [8]

    In CIKM 2021, 1794–1803

    Single Node Injection Attack against Graph Neural Networks. In CIKM 2021, 1794–1803. Tjeng, V .; Xiao, K. Y .; and Tedrake, R. 2019. Evaluating Ro- bustness of Neural Networks with Mixed Integer Program- ming. In ICLR 2019. Tran, H.; Bak, S.; Xiang, W.; and Johnson, T. T. 2020. Veri- fication of Deep Convolutional Neural Networks Using Im- ageStars. In CA...

    work page 2021

  9. [9]

    In NeurIPS 2018, 6369–6379

    Efficient Formal Safety Analysis of Neural Networks. In NeurIPS 2018, 6369–6379. Weng, T.; Zhang, H.; Chen, H.; Song, Z.; Hsieh, C.; Daniel, L.; Boning, D. S.; and Dhillon, I. S. 2018. Towards Fast Computation of Certified Robustness for ReLU Networks. In ICML 2018, 5273–5282. Wu, H.; Wang, C.; Tyshetskiy, Y .; Docherty, A.; Lu, K.; and Zhu, L. 2019. Adve...

    work page 2018

  10. [10]

    InNeurIPS 2018, 4944– 4953

    Efficient Neural Network Robustness Certification with General Activation Functions. InNeurIPS 2018, 4944– 4953. Zhang, S.; Campos, J. S.; Feldmann, C.; Walz, D.; Sandfort, F.; Mathea, M.; Tsay, C.; and Misener, R. 2023. Optimiz- ing over trained GNNs via symmetry breaking. In NeurIPS 2023. Zhang, X.; and Zitnik, M. 2020. GNNGuard: Defending Graph Neural ...

    work page 2018

  11. [11]

    Mean aggregation In this case, recall that we reduce the original problem to a combination of subproblems

    Therefore, we must take 0 into consideration. Mean aggregation In this case, recall that we reduce the original problem to a combination of subproblems. For non- negative integers s2 and s3, define the variable zs2,s3 := mean(X1 ∪ X ′ 2 ∪ X ′ 3), where X ′ 2 ⊆ X2, X ′ 3 ⊆ X3, |X2\X ′ 2| = s2, and |X ′ 3| = s3. The upper and lower bounds of the original pr...

    work page

  12. [12]

    + sum(X ′ 3)) , Because the values of s2 and s3 are fixed, the selections of X ′ 2 ⊆ X2 and X ′ 3 ⊆ X3 are independent. Thus, the up- per bound of zs2,s3 is given by the sum of upper bounds of sum(X1), sum(X ′ 2), and sum(X ′ 3), divided by ns2,s3 where X ′ 2 ⊆ X2, X ′ 3 ⊆ X3, |X2\X ′ 2| = s2, and |X ′ 3| = s3. Observe that, for a set of variables Y , bec...

    work page

  13. [13]

    Since |X ′ 2| = |X2| −s2, the upper bound of sum(X ′

    where X ′ 2 ⊆ X2 and |X2\X ′ 2| = s2. Since |X ′ 2| = |X2| −s2, the upper bound of sum(X ′

    work page

  14. [14]

    • Similarly, since X ′ 3 ⊆ X3 and |X ′ 3| = s3, the upper bound of sum(X ′

    is given by the sum of the(|X2| −s2)-largest upper bounds in X2, that is,P 1≤i≤|X2|−s2 hi(X2, i). • Similarly, since X ′ 3 ⊆ X3 and |X ′ 3| = s3, the upper bound of sum(X ′

    work page

  15. [15]

    Thus zs2,s3 is upper bounded by 1 ns2,s3  X x∈X1 x + X 1≤i≤|X2|−s2 hi(X2, i) + X 1≤i≤s3 hi(X3, i)  

    isP 1≤i≤s3 hi(X3, i). Thus zs2,s3 is upper bounded by 1 ns2,s3  X x∈X1 x + X 1≤i≤|X2|−s2 hi(X2, i) + X 1≤i≤s3 hi(X3, i)   . Note that the bound is tight. That is, there exist setsX ′ 2 ⊆ X2 and X ′ 3 ⊆ X3 with |X2\X ′ 2| = s2 and |X ′ 3| = s3 that achieve this bound exactly. C Proof of Theorem 1 Recall the theorem: Given a GNN f, an attributed directe...

    work page 2019