Verifying message-passing neural networks via topology-based bounds tightening

TL;DR

This work tackles certifiable robustness for message-passing neural networks (MPNNs) under graph perturbations by developing topology-based bounds tightening within a mixed-integer framework. It extends the Big-M encoding to handle edge additions/removals and budgets, and introduces static and aggressive bounds-tightening routines that exploit graph structure to tighten variable bounds. The authors demonstrate that these techniques, implemented as an open-source SCIP extension, substantially accelerate verification on node and graph classification tasks while yielding stronger robustness certificates, with OBBT-like insights and ReLU-bound tightening integrated into the process. The practical impact is improved reliability of GNN predictions in safety-critical settings, enabling faster, scalable certification against topology-based adversarial attacks.

Abstract

Since graph neural networks (GNNs) are often vulnerable to attack, we need to know when we can trust them. We develop a computationally effective approach towards providing robust certificates for message-passing neural networks (MPNNs) using a Rectified Linear Unit (ReLU) activation function. Because our work builds on mixed-integer optimization, it encodes a wide variety of subproblems, for example it admits (i) both adding and removing edges, (ii) both global and local budgets, and (iii) both topological perturbations and feature modifications. Our key technology, topology-based bounds tightening, uses graph structure to tighten bounds. We also experiment with aggressive bounds tightening to dynamically change the optimization constraints by tightening variable bounds. To demonstrate the effectiveness of these strategies, we implement an extension to the open-source branch-and-cut solver SCIP. We test on both node and graph classification problems and consider topological attacks that both add and remove edges.

Figures (7)

• Figure 1: (left) Consider a graph with $6$ nodes $u = 0, \ldots, 5$ and one feature. The neighbor set of node $0$ is $\mathcal{N}(0)=\{0,1,2\}$. The input bounds are given above each node. Assume the budget, i.e., maximal number of modifications, for node $0$ is $3$. The modifications could be removing neighbors from $\mathcal{N}(0)$ or adding new neighbors from $\{3,4,5\}$. Four decisions have been made in the branch-and-bound tree, i.e., binary variables representing edges are set as $A_{1,0}=0,A_{2,0}=1,A_{3,0}=0,A_{4,0}=1$. Since node $2$ is a neighbor of node $0$ while node $3$ is not, fixing $A_{2,0}=1$ and $A_{3,0}=0$ spends no budget. For each method, we compute the bounds for node $0$ in the next layer. To compute a lower bound, the plain strategy (basic) chooses all negative lower bounds without considering either budgets or previous decisions in the branch-and-bound tree. Static bounds tightening (sbt), the first topology-based bounds tightening routine, removes node $2$ and adds node $3, 4$ as neighbors within $3$ budgets, but ignores decisions in the branch-and-bound tree. Aggressive bounds tightening (abt) yields tighter bounds by saving node $0$ and adding node $5$ as neighbors. (right) The branch-and-bound tree corresponding to the left. We provide the bounds yielded from abt and budget left after each decision.
• Figure 2: ENZYMES benchmark. (left) Number of instances solved by each method below different time costs. (middle) Number of robust instances solved by each method below different time costs. (right) Consider $\rho$, the ratio of time cost between SCIPabt and SCIPsbt on each robust instance. SCIPabt is at least $10\%$ faster than SCIPsbt on $412$ robust instances.
• Figure 3: For each SCIP-based method with local attack strength $s=2$ on ENZYMES (the first row) and MUTAG (the second row), we count the number of robust graphs (green), nonrobust graphs (red), and time out (white). The percentage $\delta$ of the number of edges is the global budget.
• Figure 4: For each SCIP-based method on ENZYMES with local attack strength $s\in \{2,3,4\}$, we count the number of robust graphs (green), nonrobust graphs (red), and time out (white). The percentage $\delta$ of the number of edges is the global budget.
• Figure 5: For each SCIP-based method on MUTAG with local attack strength $s\in \{2,3,4\}$, we count the number of robust graphs (green), nonrobust graphs (red), and time out (white). The percentage $\delta$ of the number of edges is the global budget.

Theorems & Definitions (6)

• Remark 2.1
• Remark 3.1
• Remark 3.3
• Remark 3.5
• proof : Proof of Property \ref{['prop:sbt']}
• proof : Proof of Property \ref{['prop:abt']}