# Shared Certificates for Neural Network Verification

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

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Builds on 29 of its 63 references that are in the map.
- First posted on arXiv 1 Sep 2021.

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

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Evasion Attacks against Machine Learning at Test Time](https://mlsanity.com/paper/1708.06131/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Adversarial Patch](https://mlsanity.com/paper/1712.09665/) (2017)
- [Transferability in Machine Learning: from Phenomena to Black-Box Attacks using Adversarial Samples](https://mlsanity.com/paper/1605.07277/) (2016)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (2018)
- [Certified Defenses for Adversarial Patches](https://mlsanity.com/paper/2003.06693/) (2020)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [Trustworthy AI](https://mlsanity.com/paper/2011.02272/) (2020)
- [Certified Defense to Image Transformations via Randomized Smoothing](https://mlsanity.com/paper/2002.12463/) (2020)
- [Neural Network Branching for Neural Network Verification](https://mlsanity.com/paper/1912.01329/) (2019)
- [DeepAbstract: Neural Network Abstraction for Accelerating Verification](https://mlsanity.com/paper/2006.13735/) (2020)
- [ReluDiff: Differential Verification of Deep Neural Networks](https://mlsanity.com/paper/2001.03662/) (2020)
- [NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation](https://mlsanity.com/paper/2009.09943/) (2020)
- [Towards Practical Verification of Machine Learning: The Case of Computer Vision Systems](https://mlsanity.com/paper/1712.01785/) (2017)
- [Linear Encodings for Polytope Containment Problems](https://mlsanity.com/paper/1903.05214/) (2019)
- [Continuous Safety Verification of Neural Networks](https://mlsanity.com/paper/2010.05689/) (2020)
- [Scalable and Modular Robustness Analysis of Deep Neural Networks](https://mlsanity.com/paper/2108.11651/) (2021)

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

- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Incremental Verification of Neural Networks](https://mlsanity.com/paper/2304.01874/) (2023)
- [Incremental Randomized Smoothing Certification](https://mlsanity.com/paper/2305.19521/) (2023)
- [PECAN: A Deterministic Certified Defense Against Backdoor Attacks](https://mlsanity.com/paper/2301.11824/) (2023)
- [Mini-Batch Robustness Verification of Deep Neural Networks](https://mlsanity.com/paper/2508.15454/) (2025)
- [MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression](https://mlsanity.com/paper/2506.04268/) (2025)
- [Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees](https://mlsanity.com/paper/2507.17453/) (2025)
- [Branch and Bound for Relational Verification of Neural Networks](https://mlsanity.com/paper/2608.13118/) (2026)
- [Uncovering the Limits of Proof Sharing for Neural Networks](https://mlsanity.com/paper/2608.19351/) (2026)
- [Exploring Solver-Level Warmstarting for Neural Network Verification](https://mlsanity.com/paper/2609.25962/) (2026)

## Abstract (arXiv)

Existing neural network verifiers compute a proof that each input is handled correctly under a given perturbation by propagating a symbolic abstraction of reachable values at each layer. This process is repeated from scratch independently for each input (e.g., image) and perturbation (e.g., rotation), leading to an expensive overall proof effort when handling an entire dataset. In this work, we introduce a new method for reducing this verification cost without losing precision based on a key insight that abstractions obtained at intermediate layers for different inputs and perturbations can overlap or contain each other. Leveraging our insight, we introduce the general concept of shared certificates, enabling proof effort reuse across multiple inputs to reduce overall verification costs. We perform an extensive experimental evaluation to demonstrate the effectiveness of shared certificates in reducing the verification cost on a range of datasets and attack specifications on image classifiers including the popular patch and geometric perturbations. We release our implementation at https://github.com/eth-sri/proof-sharing.