# Abstraction-Based Proof Production in Formal Verification of Neural Networks

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 50 references that are in the map.
- First posted on arXiv 11 Jun 2025.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Learning Transferable Visual Models From Natural Language Supervision](https://mlsanity.com/paper/2103.00020/) (2021)
- [Robust Speech Recognition via Large-Scale Weak Supervision](https://mlsanity.com/paper/2212.04356/) (2022)
- [WaveNet: A Generative Model for Raw Audio](https://mlsanity.com/paper/1609.03499/) (2016)
- [ViViT: A Video Vision Transformer](https://mlsanity.com/paper/2103.15691/) (2021)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [DeepAbstract: Neural Network Abstraction for Accelerating Verification](https://mlsanity.com/paper/2006.13735/) (2020)
- [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes](https://mlsanity.com/paper/2207.02715/) (2022)
- [Neural Network Verification with Proof Production](https://mlsanity.com/paper/2206.00512/) (2022)
- [Neural Network Verification using Residual Reasoning](https://mlsanity.com/paper/2208.03083/) (2022)
- [Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks](https://mlsanity.com/paper/2207.00759/) (2022)
- [Tighter Abstract Queries in Neural Network Verification](https://mlsanity.com/paper/2210.12871/) (2022)
- [Fully Automatic Neural Network Reduction for Formal Verification](https://mlsanity.com/paper/2305.01932/) (2023)
- [DeepCDCL: An CDCL-based Neural Network Verification Framework](https://mlsanity.com/paper/2403.07956/) (2024)
- [DelBugV: Delta-Debugging Neural Network Verifiers](https://mlsanity.com/paper/2305.18558/) (2023)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [Automated Verification of Soundness of DNN Certifiers](https://mlsanity.com/paper/2504.04542/) (2025)
- [Towards Bit-Width-Independent Proofs in SMT Solvers](https://mlsanity.com/paper/1905.10434/) (2019)

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

- [VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification](https://mlsanity.com/paper/2605.07451/) (2026)
- [On Improving Deep Active Learning with Formal Verification](https://mlsanity.com/paper/2512.14170/) (2025)
- [Talking with Verifiers: Automatic Specification Generation for Neural Network Verification](https://mlsanity.com/paper/2603.02235/) (2026)
- [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)

Modern verification tools for deep neural networks (DNNs) increasingly rely on abstraction to scale to realistic architectures. In parallel, proof production is becoming a critical requirement for increasing the reliability of DNN verification results. However, current proofproducing verifiers do not support abstraction-based reasoning, creating a gap between scalability and provable guarantees. We address this gap by introducing a novel framework for proof-producing abstraction-based DNN verification. Our approach modularly separates the verification task into two components: (i) proving the correctness of an abstract network, and (ii) proving the soundness of the abstraction with respect to the original DNN. The former can be handled by existing proof-producing verifiers, whereas we propose the first method for generating formal proofs for the latter. This preliminary work aims to enable scalable and trustworthy verification by supporting common abstraction techniques within a formal proof framework.