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

arXiv: https://arxiv.org/abs/2402.13937 · HTML: https://mlsanity.com/paper/2402.13937/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Builds on 36 of its 54 references that are in the map.
- First posted on arXiv 21 Feb 2024.

## Builds on (most cited first, 30 of 36)

- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [Fast Graph Representation Learning with PyTorch Geometric](https://mlsanity.com/paper/1903.02428/) (2019)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [Predict then Propagate: Graph Neural Networks meet Personalized PageRank](https://mlsanity.com/paper/1810.05997/) (2018)
- [TUDataset: A collection of benchmark datasets for learning with graphs](https://mlsanity.com/paper/2007.08663/) (2020)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Adversarial Attacks on Neural Networks for Graph Data](https://mlsanity.com/paper/1805.07984/) (2018)
- [Adversarial Attack on Graph Structured Data](https://mlsanity.com/paper/1806.02371/) (2018)
- [Adversarial Attacks on Graph Neural Networks via Meta Learning](https://mlsanity.com/paper/1902.08412/) (2019)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Topology Attack and Defense for Graph Neural Networks: An Optimization Perspective](https://mlsanity.com/paper/1906.04214/) (2019)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (2018)
- [Robustness of Graph Neural Networks at Scale](https://mlsanity.com/paper/2110.14038/) (2021)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Towards More Practical Adversarial Attacks on Graph Neural Networks](https://mlsanity.com/paper/2006.05057/) (2020)
- [Certifiable Robustness to Graph Perturbations](https://mlsanity.com/paper/1910.14356/) (2019)
- [Certifiable Robustness and Robust Training for Graph Convolutional Networks](https://mlsanity.com/paper/1906.12269/) (2019)
- [Certified Robustness of Graph Neural Networks against Adversarial Structural Perturbation](https://mlsanity.com/paper/2008.10715/) (2020)
- [Efficient Robustness Certificates for Discrete Data: Sparsity-Aware Randomized Smoothing for Graphs, Images and More](https://mlsanity.com/paper/2008.12952/) (2020)
- [Scalable Attack on Graph Data by Injecting Vicious Nodes](https://mlsanity.com/paper/2004.13825/) (2020)
- [The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification](https://mlsanity.com/paper/2006.14076/) (2020)
- [Partition-based formulations for mixed-integer optimization of trained ReLU neural networks](https://mlsanity.com/paper/2102.04373/) (2021)
- [OMLT: Optimization & Machine Learning Toolkit](https://mlsanity.com/paper/2202.02414/) (2022)
- [PANE: scalable and effective attributed network embedding](https://mlsanity.com/paper/2009.00826/) (2020)
- [Scalable Verification of GNN-based Job Schedulers](https://mlsanity.com/paper/2203.03153/) (2022)
- [Indirect Adversarial Attacks via Poisoning Neighbors for Graph Convolutional Networks](https://mlsanity.com/paper/2002.08012/) (2020)
- [Enabling Research through the SCIP Optimization Suite 8.0](https://mlsanity.com/paper/2303.07101/) (2023)
- [Fundamental Limits in Formal Verification of Message-Passing Neural Networks](https://mlsanity.com/paper/2206.05070/) (2022)

## Built on by (most cited first, 10 of 10)

- [Exact Certification of (Graph) Neural Networks Against Label Poisoning](https://mlsanity.com/paper/2412.00537/) (2024)
- [Provable Robustness of (Graph) Neural Networks Against Data Poisoning and Backdoor Attacks](https://mlsanity.com/paper/2407.10867/) (2024)
- [Exact Verification of Graph Neural Networks with Incremental Constraint Solving](https://mlsanity.com/paper/2508.09320/) (2025)
- [Global optimization of graph acquisition functions for neural architecture search](https://mlsanity.com/paper/2505.23640/) (2025)
- [Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits](https://mlsanity.com/paper/2512.20755/) (2025)
- [Certifying Robustness of Graph Convolutional Networks for Node Perturbation with Polyhedra Abstract Interpretation](https://mlsanity.com/paper/2405.08645/) (2024)
- [Optimization over Trained (and Sparse) Neural Networks: A Surrogate within a Surrogate](https://mlsanity.com/paper/2505.01985/) (2025)
- [Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing](https://mlsanity.com/paper/2510.18591/) (2025)
- [NNV3: Expanding Neural Network Verification to New Architectures and Domains](https://mlsanity.com/paper/2609.30050/) (2026)
- [Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features](https://mlsanity.com/paper/2609.30079/) (2026)

## Abstract (arXiv)

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.