# Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 28 of its 67 references that are in the map.
- First posted on arXiv 23 Apr 2024.

## Builds on (most cited first, 28 of 28)

- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [A Comprehensive Survey on Graph Neural Networks](https://mlsanity.com/paper/1901.00596/) (2019)
- [Graph Convolutional Neural Networks for Web-Scale Recommender Systems](https://mlsanity.com/paper/1806.01973/) (2018)
- [Geometric deep learning: going beyond Euclidean data](https://mlsanity.com/paper/1611.08097/) (2016)
- [Revisiting Semi-Supervised Learning with Graph Embeddings](https://mlsanity.com/paper/1603.08861/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Measuring and Relieving the Over-smoothing Problem for Graph Neural Networks from the Topological View](https://mlsanity.com/paper/1909.03211/) (2019)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Graph Structure Learning for Robust Graph Neural Networks](https://mlsanity.com/paper/2005.10203/) (2020)
- [Adversarial Attack on Graph Structured Data](https://mlsanity.com/paper/1806.02371/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [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)
- [Efficient Robustness Certificates for Discrete Data: Sparsity-Aware Randomized Smoothing for Graphs, Images and More](https://mlsanity.com/paper/2008.12952/) (2020)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results](https://mlsanity.com/paper/2312.16760/) (2023)
- [Certified Robustness of Community Detection against Adversarial Structural Perturbation via Randomized Smoothing](https://mlsanity.com/paper/2002.03421/) (2020)
- [JuliaReach: a Toolbox for Set-Based Reachability](https://mlsanity.com/paper/1901.10736/) (2019)
- [Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes](https://mlsanity.com/paper/2207.02715/) (2022)
- [Scalable Verification of GNN-based Job Schedulers](https://mlsanity.com/paper/2203.03153/) (2022)
- [Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis](https://mlsanity.com/paper/1901.01780/) (2019)
- [Fundamental Limits in Formal Verification of Message-Passing Neural Networks](https://mlsanity.com/paper/2206.05070/) (2022)
- [Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs](https://mlsanity.com/paper/2006.09040/) (2020)

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

- [Exact Verification of Graph Neural Networks with Incremental Constraint Solving](https://mlsanity.com/paper/2508.09320/) (2025)
- [Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits](https://mlsanity.com/paper/2512.20755/) (2025)
- [Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing](https://mlsanity.com/paper/2510.18591/) (2025)
- [Perception with Guarantees: Certified Pose Estimation via Reachability Analysis](https://mlsanity.com/paper/2602.10032/) (2026)
- [Talking with Verifiers: Automatic Specification Generation for Neural Network Verification](https://mlsanity.com/paper/2603.02235/) (2026)
- [Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes](https://mlsanity.com/paper/2605.10474/) (2026)
- [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)

Graph neural networks are becoming increasingly popular in the field of machine learning due to their unique ability to process data structured in graphs. They have also been applied in safety-critical environments where perturbations inherently occur. However, these perturbations require us to formally verify neural networks before their deployment in safety-critical environments as neural networks are prone to adversarial attacks. While there exists research on the formal verification of neural networks, there is no work verifying the robustness of generic graph convolutional network architectures with uncertainty in the node features and in the graph structure over multiple message-passing steps. This work addresses this research gap by explicitly preserving the non-convex dependencies of all elements in the underlying computations through reachability analysis with (matrix) polynomial zonotopes. We demonstrate our approach on three popular benchmark datasets.