# Neural Network Verification with Proof Production

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

## Key facts

- Cited by 22 papers in the map (data through 14 Oct 2026).
- Builds on 29 of its 79 references that are in the map.
- First posted on arXiv 1 Jun 2022.

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

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [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)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [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)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Measuring Neural Net Robustness with Constraints](https://mlsanity.com/paper/1605.07262/) (2016)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [Fastened CROWN: Tightened Neural Network Robustness Certificates](https://mlsanity.com/paper/1912.00574/) (2019)
- [Parallelization Techniques for Verifying Neural Networks](https://mlsanity.com/paper/2004.08440/) (2020)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [Towards Scalable Verification of Deep Reinforcement Learning](https://mlsanity.com/paper/2105.11931/) (2021)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Learning to Give Checkable Answers with Prover-Verifier Games](https://mlsanity.com/paper/2108.12099/) (2021)
- [Verifying Recurrent Neural Networks using Invariant Inference](https://mlsanity.com/paper/2004.02462/) (2020)
- [Global Optimization of Objective Functions Represented by ReLU Networks](https://mlsanity.com/paper/2010.03258/) (2020)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [Efficient Neural Network Analysis with Sum-of-Infeasibilities](https://mlsanity.com/paper/2203.11201/) (2022)
- [Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI](https://mlsanity.com/paper/2005.07173/) (2020)
- [Pruning and Slicing Neural Networks using Formal Verification](https://mlsanity.com/paper/2105.13649/) (2021)
- [Verification-Aided Deep Ensemble Selection](https://mlsanity.com/paper/2202.03898/) (2022)
- [Minimal Multi-Layer Modifications of Deep Neural Networks](https://mlsanity.com/paper/2110.09929/) (2021)

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

- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks](https://mlsanity.com/paper/2210.13915/) (2022)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [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)
- [Verifying Generalization in Deep Learning](https://mlsanity.com/paper/2302.05745/) (2023)
- [Tighter Abstract Queries in Neural Network Verification](https://mlsanity.com/paper/2210.12871/) (2022)
- [Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing](https://mlsanity.com/paper/2402.00035/) (2024)
- [A Certified Proof Checker for Deep Neural Network Verification in Imandra](https://mlsanity.com/paper/2405.10611/) (2024)
- [Towards a Certified Proof Checker for Deep Neural Network Verification](https://mlsanity.com/paper/2307.06299/) (2023)
- [SoundnessBench: A Soundness Benchmark for Neural Network Verifiers](https://mlsanity.com/paper/2412.03154/) (2024)
- [Abstraction-Based Proof Production in Formal Verification of Neural Networks](https://mlsanity.com/paper/2506.09455/) (2025)
- [Towards Formal Verification of Deep Neural Networks for Object Detection](https://mlsanity.com/paper/2407.01295/) (2024)
- [Proof Minimization in Neural Network Verification](https://mlsanity.com/paper/2511.08198/) (2025)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [Incremental Neural Network Verification via Learned Conflicts](https://mlsanity.com/paper/2603.12232/) (2026)
- [Formally Verified Approximate Policy Iteration](https://mlsanity.com/paper/2406.07340/) (2024)
- [Proof-Carrying Neuro-Symbolic Code](https://mlsanity.com/paper/2504.12031/) (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)
- [veriFIRE: an Industrial Case Study in Verifying Consistency Properties for a DNN-Based Wildfire Detection System](https://mlsanity.com/paper/2606.04121/) (2026)

## Abstract (arXiv)

Deep neural networks (DNNs) are increasingly being employed in safety-critical systems, and there is an urgent need to guarantee their correctness. Consequently, the verification community has devised multiple techniques and tools for verifying DNNs. When DNN verifiers discover an input that triggers an error, that is easy to confirm; but when they report that no error exists, there is no way to ensure that the verification tool itself is not flawed. As multiple errors have already been observed in DNN verification tools, this calls the applicability of DNN verification into question. In this work, we present a novel mechanism for enhancing Simplex-based DNN verifiers with proof production capabilities: the generation of an easy-to-check witness of unsatisfiability, which attests to the absence of errors. Our proof production is based on an efficient adaptation of the well-known Farkas' lemma, combined with mechanisms for handling piecewise-linear functions and numerical precision errors. As a proof of concept, we implemented our technique on top of the Marabou DNN verifier. Our evaluation on a safety-critical system for airborne collision avoidance shows that proof production succeeds in almost all cases and requires only minimal overhead.