# Uncovering the Limits of Proof Sharing for Neural Networks

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 24 of its 48 references that are in the map.
- First posted on arXiv 19 Aug 2026.

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

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [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)
- [Towards Evaluating the Robustness of Neural Networks](https://mlsanity.com/paper/1608.04644/) (2016)
- [One pixel attack for fooling deep neural networks](https://mlsanity.com/paper/1710.08864/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [SoK: Certified Robustness for Deep Neural Networks](https://mlsanity.com/paper/2009.04131/) (2020)
- [Certified Defenses for Adversarial Patches](https://mlsanity.com/paper/2003.06693/) (2020)
- [SparseFool: a few pixels make a big difference](https://mlsanity.com/paper/1811.02248/) (2018)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Sparse-RS: a versatile framework for query-efficient sparse black-box adversarial attacks](https://mlsanity.com/paper/2006.12834/) (2020)
- [Introduction to Neural Network Verification](https://mlsanity.com/paper/2109.10317/) (2021)
- [Certified Training: Small Boxes are All You Need](https://mlsanity.com/paper/2210.04871/) (2022)
- [Scaling Up Exact Neural Network Compression by ReLU Stability](https://mlsanity.com/paper/2102.07804/) (2021)
- [Provable Defense Against Geometric Transformations](https://mlsanity.com/paper/2207.11177/) (2022)
- [Incremental Verification of Neural Networks](https://mlsanity.com/paper/2304.01874/) (2023)
- [Incremental Randomized Smoothing Certification](https://mlsanity.com/paper/2305.19521/) (2023)
- [Shared Certificates for Neural Network Verification](https://mlsanity.com/paper/2109.00542/) (2021)
- [Demanded Abstract Interpretation (Extended Version)](https://mlsanity.com/paper/2104.01270/) (2021)
- [Boosting Few-Pixel Robustness Verification via Covering Verification Designs](https://mlsanity.com/paper/2405.10924/) (2024)
- [Towards Generalized Certified Robustness with Multi-Norm Training](https://mlsanity.com/paper/2410.03000/) (2024)
- [Tight Robustness Certification Through the Convex Hull of ℓ0 Attacks](https://mlsanity.com/paper/2511.10576/) (2025)

## Abstract (arXiv)

Robustness verification of neural networks is increasingly important, due to their use in many critical domains. In certain scenarios, proof sharing has been shown to accelerate incomplete verification techniques by reusing intermediate-layer abstract states, or templates, across queries. However, questions remain as to the robustness of template-based acceleration across varying network architectures, properties, datasets, and training methods. In this work, we perform a systematic study of the effectiveness of template-based acceleration and its limits. Our study shows that template subsumption rates can vary widely across scenarios. We present a novel metric of jointly stable neurons to explain this variation, showing that in some cases template-based techniques are very unlikely to provide any speedup. Then, we present FastCert, a novel technique for automatically distributing templates across neural network layers to increase performance impact, eschewing templates entirely if they are unlikely to produce a speedup. Across a large set of covering-design based L0-verification tasks, FastCert achieved an average speedup of 1.13x over an extant template-based reuse technique.