ML Security PapersExact Verification of Graph Neural Networks with Incremental Constraint Solving
Minghao Liu , Chia-Hsuan Lu , Marta Kwiatkowska
Published on arXiv
2508.09320
Input Manipulation Attack
OWASP ML Top 10 — ML01
Key Finding
GNNev achieves superior node classification verification performance and competitive graph classification results compared to existing exact verification tools, while being the first to support max and mean aggregation in exact GNN verification.
GNNev
Novel technique introduced
Graph neural networks (GNNs) are increasingly 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 for node classification and competitiveness on graph classification compared to existing exact verification tools on sum-aggregated GNNs.
Key Contributions
- First exact (sound and complete) GNN verification method supporting max and mean aggregation functions, in addition to sum, for message-passing GNNs.
- Incremental constraint solving with bound tightening that iteratively solves relaxed constraint satisfaction problems to improve verification efficiency.
- GNNev implementation evaluated on real-world fraud (Amazon, Yelp) and biochemical (MUTAG, ENZYMES) datasets, outperforming existing exact tools on node classification.
🛡️ Threat Analysis
Proposes a defense (exact verification) that computes certified robustness guarantees against adversarial input perturbations — both attribute and structural (edge addition/deletion) — for GNNs at inference time.