# Fully Automatic Neural Network Reduction for Formal Verification

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 32 of its 68 references that are in the map.
- First posted on arXiv 3 May 2023.

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

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Theoretically Principled Trade-off between Robustness and Accuracy](https://mlsanity.com/paper/1901.08573/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [A Survey of Convolutional Neural Networks: Analysis, Applications, and Prospects](https://mlsanity.com/paper/2004.02806/) (2020)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Towards Understanding the Role of Over-Parametrization in Generalization of Neural Networks](https://mlsanity.com/paper/1805.12076/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Reducing the Hausdorff Distance in Medical Image Segmentation with Convolutional Neural Networks](https://mlsanity.com/paper/1904.10030/) (2019)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [Explainability of deep vision-based autonomous driving systems: Review and challenges](https://mlsanity.com/paper/2101.05307/) (2021)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [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)
- [Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks](https://mlsanity.com/paper/2210.13915/) (2022)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [Abstraction based Output Range Analysis for Neural Networks](https://mlsanity.com/paper/2007.09527/) (2020)
- [DeepAbstract: Neural Network Abstraction for Accelerating Verification](https://mlsanity.com/paper/2006.13735/) (2020)
- [JuliaReach: a Toolbox for Set-Based Reachability](https://mlsanity.com/paper/1901.10736/) (2019)
- [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 using Residual Reasoning](https://mlsanity.com/paper/2208.03083/) (2022)
- [Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis](https://mlsanity.com/paper/1901.01780/) (2019)
- [Can pruning improve certified robustness of neural networks?](https://mlsanity.com/paper/2206.07311/) (2022)
- [Abstract Neural Networks](https://mlsanity.com/paper/2009.05660/) (2020)
- [Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs](https://mlsanity.com/paper/2006.09040/) (2020)
- [Neural Activation Patterns (NAPs): Visual Explainability of Learned Concepts](https://mlsanity.com/paper/2206.10611/) (2022)
- [Bisimulations for Neural Network Reduction](https://mlsanity.com/paper/2110.03726/) (2021)
- [Dynamic Probabilistic Pruning: A general framework for hardware-constrained pruning at different granularities](https://mlsanity.com/paper/2105.12686/) (2021)

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

- [AgentGuard: Runtime Verification of AI Agents](https://mlsanity.com/paper/2509.23864/) (2025)
- [Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations](https://mlsanity.com/paper/2506.08505/) (2025)
- [Abstraction-Based Proof Production in Formal Verification of Neural Networks](https://mlsanity.com/paper/2506.09455/) (2025)
- [Expediting Neural Network Verification via Network Reduction](https://mlsanity.com/paper/2308.03330/) (2023)
- [Efficient Reachability Analysis for Convolutional Neural Networks Using Hybrid Zonotopes](https://mlsanity.com/paper/2503.10840/) (2025)
- [The Misery of Mechanistic Interpretability: A Formal Perspective](https://mlsanity.com/paper/2609.15533/) (2026)

## Abstract (arXiv)

Formal verification of neural networks is essential before their deployment in safety-critical applications. However, existing methods for formally verifying neural networks are not yet scalable enough to handle practical problems under strict time constraints. We address this challenge by introducing a fully automatic and sound reduction of neural networks using reachability analysis. The soundness ensures that the verification of the reduced network entails the verification of the original network. Our sound reduction approach is applicable to neural networks with any type of element-wise activation function, such as ReLU, sigmoid, and tanh. The network reduction is computed on the fly while simultaneously verifying the original network and its specification. All parameters are automatically tuned to minimize the network size without compromising verifiability. We further show the applicability of our approach to convolutional neural networks by explicitly exploiting similar neighboring pixels. Our evaluation shows that our approach reduces large neural networks to a fraction of the original number of neurons and thus shortens the verification time to a similar degree.