Exact Verification of Graph Neural Networks with Incremental Constraint Solving

TL;DR

This paper introduces GNNev, an exact verification tool for message-passing GNNs supporting sum, max, and mean aggregations, enabling robustness guarantees against structural perturbations.

Contribution

The paper presents a sound, complete verification method for GNNs that supports multiple aggregation functions, including the first support for mean and max aggregations.

Findings

GNNev effectively verifies GNN robustness on real-world datasets.

Supports sum, max, and mean aggregation functions in verification.

Outperforms existing tools on sum-aggregated GNNs in experiments.

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.