# Neural Network Verification using Residual Reasoning

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

## Key facts

- Cited by 18 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Aug 2022.

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

- [Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks](https://mlsanity.com/paper/2210.13915/) (2022)
- [Verification-Guided Shielding for Deep Reinforcement Learning](https://mlsanity.com/paper/2406.06507/) (2024)
- [Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations](https://mlsanity.com/paper/2506.08505/) (2025)
- [veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System](https://mlsanity.com/paper/2212.03287/) (2022)
- [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)
- [On Optimizing Back-Substitution Methods for Neural Network Verification](https://mlsanity.com/paper/2208.07669/) (2022)
- [Fully Automatic Neural Network Reduction for Formal Verification](https://mlsanity.com/paper/2305.01932/) (2023)
- [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)
- [Safe and Reliable Training of Learning-Based Aerospace Controllers](https://mlsanity.com/paper/2407.07088/) (2024)
- [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)
- [Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits](https://mlsanity.com/paper/2512.20755/) (2025)
- [Talking with Verifiers: Automatic Specification Generation for Neural Network Verification](https://mlsanity.com/paper/2603.02235/) (2026)
- [Towards Verified and Targeted Explanations through Formal Methods](https://mlsanity.com/paper/2604.14209/) (2026)
- [veriFIRE: an Industrial Case Study in Verifying Consistency Properties for a DNN-Based Wildfire Detection System](https://mlsanity.com/paper/2606.04121/) (2026)
- [Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features](https://mlsanity.com/paper/2609.30079/) (2026)

## Abstract (arXiv)

With the increasing integration of neural networks as components in mission-critical systems, there is an increasing need to ensure that they satisfy various safety and liveness requirements. In recent years, numerous sound and complete verification methods have been proposed towards that end, but these typically suffer from severe scalability limitations. Recent work has proposed enhancing such verification techniques with abstraction-refinement capabilities, which have been shown to boost scalability: instead of verifying a large and complex network, the verifier constructs and then verifies a much smaller network, whose correctness implies the correctness of the original network. A shortcoming of such a scheme is that if verifying the smaller network fails, the verifier needs to perform a refinement step that increases the size of the network being verified, and then start verifying the new network from scratch - effectively "wasting" its earlier work on verifying the smaller network. In this paper, we present an enhancement to abstraction-based verification of neural networks, by using residual reasoning: the process of utilizing information acquired when verifying an abstract network, in order to expedite the verification of a refined network. In essence, the method allows the verifier to store information about parts of the search space in which the refined network is guaranteed to behave correctly, and allows it to focus on areas where bugs might be discovered. We implemented our approach as an extension to the Marabou verifier, and obtained promising results.