# Proof Minimization in Neural Network Verification

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 33 of its 71 references that are in the map.
- First posted on arXiv 11 Nov 2025.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Activation Functions in Deep Learning: A Comprehensive Survey and Benchmark](https://mlsanity.com/paper/2109.14545/) (2021)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [Fastened CROWN: Tightened Neural Network Robustness Certificates](https://mlsanity.com/paper/1912.00574/) (2019)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [Neural Network Verification with Proof Production](https://mlsanity.com/paper/2206.00512/) (2022)
- [NLP Verification: Towards a General Methodology for Certifying Robustness](https://mlsanity.com/paper/2403.10144/) (2024)
- [veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System](https://mlsanity.com/paper/2212.03287/) (2022)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [DNN Verification, Reachability, and the Exponential Function Problem](https://mlsanity.com/paper/2305.06064/) (2023)
- [Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing](https://mlsanity.com/paper/2402.00035/) (2024)
- [Neural Networks for Safety-Critical Applications - Challenges, Experiments and Perspectives](https://mlsanity.com/paper/1709.00911/) (2017)
- [A Certified Proof Checker for Deep Neural Network Verification in Imandra](https://mlsanity.com/paper/2405.10611/) (2024)
- [Scalable Synthesis of Formally Verified Neural Value Function for Hamilton-Jacobi Reachability Analysis](https://mlsanity.com/paper/2407.20532/) (2024)
- [ANTONIO: Towards a Systematic Method of Generating NLP Benchmarks for Verification](https://mlsanity.com/paper/2305.04003/) (2023)
- [Towards a Certified Proof Checker for Deep Neural Network Verification](https://mlsanity.com/paper/2307.06299/) (2023)

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

- [Incremental Neural Network Verification via Learned Conflicts](https://mlsanity.com/paper/2603.12232/) (2026)
- [On Improving Deep Active Learning with Formal Verification](https://mlsanity.com/paper/2512.14170/) (2025)
- [The Luna Bound Propagator for Formal Analysis of Neural Networks](https://mlsanity.com/paper/2603.23878/) (2026)
- [Neural Network Verification using Partial Multi-Neuron Relaxation](https://mlsanity.com/paper/2605.30155/) (2026)

## Abstract (arXiv)

The widespread adoption of deep neural networks (DNNs) requires efficient techniques for verifying their safety. DNN verifiers are complex tools, which might contain bugs that could compromise their soundness and undermine the reliability of the verification process. This concern can be mitigated using proofs: artifacts that are checkable by an external and reliable proof checker, and which attest to the correctness of the verification process. However, such proofs tend to be extremely large, limiting their use in many scenarios. In this work, we address this problem by minimizing proofs of unsatisfiability produced by DNN verifiers. We present algorithms that remove facts which were learned during the verification process, but which are unnecessary for the proof itself. Conceptually, our method analyzes the dependencies among facts used to deduce UNSAT, and removes facts that did not contribute. We then further minimize the proof by eliminating remaining unnecessary dependencies, using two alternative procedures. We implemented our algorithms on top of a proof producing DNN verifier, and evaluated them across several benchmarks. Our results show that our best-performing algorithm reduces proof size by 37%-82% and proof checking time by 30%-88%, while introducing a runtime overhead of 7%-20% to the verification process itself.