# Towards a Certified Proof Checker for Deep Neural Network Verification

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 35 references that are in the map.
- First posted on arXiv 12 Jul 2023.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [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)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Measuring Neural Net Robustness with Constraints](https://mlsanity.com/paper/1605.07262/) (2016)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [Abstraction based Output Range Analysis for Neural Networks](https://mlsanity.com/paper/2007.09527/) (2020)
- [Neural Network Verification with Proof Production](https://mlsanity.com/paper/2206.00512/) (2022)
- [Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs](https://mlsanity.com/paper/2006.09040/) (2020)
- [Fast BATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks](https://mlsanity.com/paper/2111.09293/) (2021)
- [Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers](https://mlsanity.com/paper/2202.05207/) (2022)
- [The Imandra Automated Reasoning System (system description)](https://mlsanity.com/paper/2004.10263/) (2020)
- [Neural Networks in Imandra: Matrix Representation as a Verification Choice](https://mlsanity.com/paper/2205.09556/) (2022)
- [Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code](https://mlsanity.com/paper/1803.06960/) (2018)

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

- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Proof Minimization in Neural Network Verification](https://mlsanity.com/paper/2511.08198/) (2025)
- [Compiling High-Level Neural Network Specifications into VNN-LIB Queries](https://mlsanity.com/paper/2402.01353/) (2024)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [Efficient Certified Reasoning for Binarized Neural Networks](https://mlsanity.com/paper/2507.02916/) (2025)

## Abstract (arXiv)

Recent developments in deep neural networks (DNNs) have led to their adoption in safety-critical systems, which in turn has heightened the need for guaranteeing their safety. These safety properties of DNNs can be proven using tools developed by the verification community. However, these tools are themselves prone to implementation bugs and numerical stability problems, which make their reliability questionable. To overcome this, some verifiers produce proofs of their results which can be checked by a trusted checker. In this work, we present a novel implementation of a proof checker for DNN verification. It improves on existing implementations by offering numerical stability and greater verifiability. To achieve this, we leverage two key capabilities of Imandra, an industrial theorem prover: its support of infinite precision real arithmetic and its formal verification infrastructure. So far, we have implemented a proof checker in Imandra, specified its correctness properties and started to verify the checker's compliance with them. Our ongoing work focuses on completing the formal verification of the checker and further optimizing its performance.