Research map / Graph learning / GNN architectures
Verifying message-passing neural networks via topology-based bounds tightening
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes topology-based bounds tightening (static sbt and aggressive abt) for big-M mixed-integer verification of ReLU message-passing neural networks, implemented in SCIP, and tests robustness certification on MUTAG/ENZYMES graph classification and Cora/CiteSeer node classification.
Problem
Certifying robustness of message-passing neural networks with ReLU activations against topological perturbations (adding/removing edges under global and local budgets) is computationally hard because the big-M mixed-integer verification problems are large and loose.
Approach
Exploit graph structure and perturbation budgets to compute tighter variable bounds in the big-M MIP: static bounds tightening computes bounds from original neighbors then applies the budget, and aggressive bounds tightening re-tightens bounds at each branch-and-bound node using fixed edge decisions and remaining budget, added as local cutting planes in SCIP.
Key results
- On ENZYMES (s=2), SCIPsbt reduces average solve time from 605.97s (SCIPbasic) to 230.59s and solves 5831 vs 5579 instances out of 5915.
- On MUTAG (s=2), SCIPabt gives 238.10s average on robust instances vs 798.47s for SCIPbasic, and SCIPsbt solves all 1589 instances.
- Node classification instances on Cora and CiteSeer are solved in well under a second on average by all SCIP variants.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Add static bounds tightening to SCIP | SCIP on ENZYMES graph classification, s=2 · ENZYMES, all instances | avg-time (s): 605.97 -> 230.59 | Helped |
| Add static bounds tightening to SCIP | SCIP on MUTAG graph classification, s=2 · MUTAG, all instances | avg-time (s): 679.86 -> 196.07 | Helped |
| Add static bounds tightening to Gurobi | Gurobi on ENZYMES graph classification, s=2 · ENZYMES, all instances | avg-time (s): 86.03 -> 74.87 | Helped |
| Add static bounds tightening to Gurobi | Gurobi on MUTAG graph classification, s=2 · MUTAG, all instances | avg-time (s): 34.58 -> 59.93 | Hurt |
| Use aggressive bounds tightening instead of static bounds tightening (ablation) | SCIP on Cora node classification · Cora | avg-time (s): 0.17 -> 0.46 | Hurt |
| Use aggressive bounds tightening instead of static bounds tightening (ablation) | SCIP on CiteSeer node classification · CiteSeer | avg-time (s): 0.07 -> 0.31 | Hurt |
| Add static bounds tightening to SCIP | SCIP on CiteSeer node classification · CiteSeer | avg-time (s): 0.07 -> 0.07 | No clear effect |
| Use aggressive bounds tightening instead of static bounds tightening (ablation) | SCIP on ENZYMES graph classification, s=2 · ENZYMES, all instances | avg-time (s): 230.59 -> 246.02 | Hurt |
| Use aggressive bounds tightening instead of static bounds tightening (ablation) | SCIP on MUTAG graph classification, s=2 · MUTAG, all instances | avg-time (s): 196.07 -> 207.50 | Hurt |
| Add static bounds tightening to SCIP | SCIP on ENZYMES graph classification, s=2 · ENZYMES, all instances | instances solved: 5579 -> 5831 | Helped |
| Add static bounds tightening to SCIP | SCIP on MUTAG graph classification, s=2 · MUTAG, all instances | instances solved: 1575 -> 1589 | Helped |
Surprising findings
- Static bounds tightening slows Gurobi/SCIP on MUTAG across all instances because most MUTAG instances are non-robust and finding an attack is what matters.
- Aggressive bounds tightening was not consistently faster than static bounds tightening; tighter OBBT bounds gave only limited solving-time improvement over sbt.
Experimental setup
Datasets: MUTAG ENZYMES Cora CiteSeer
Benchmarks: MUTAG ENZYMES Cora CiteSeer
Metrics: average solving time shifted geometric mean solving time number of solved instances within time limit
Baselines: SCIPbasic Gurobi basic (GRBbasic) Gurobi static bounds tightening (GRBsbt) OBBT
Builds on: big-M ReLU formulation feasibility-based bounds tightening SCIP GraphSAGE OMLT
Closest papers by meaning
- Accurate and Scalable Graph Neural Networks via Message Invariance (ICLR 2025 · similarity 0.86)
- What do Graph Neural Networks learn? Insights from Tropical Geometry (NeurIPS 2024 · similarity 0.86)
- Deterministic Certification of Graph Neural Networks against Graph Poisoning Attacks with Arbitrary Perturbations (CVPR 2025 · similarity 0.86)
- A Simple and Yet Fairly Effective Defense for Graph Neural Networks (AAAI 2024 · similarity 0.86)
- Probabilistically Rewired Message-Passing Neural Networks (ICLR 2024 · similarity 0.86)
- Sign is Not a Remedy: Multiset-to-Multiset Message Passing for Learning on Heterophilic Graphs (ICML 2024 · similarity 0.86)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.
