# Optimized Symbolic Interval Propagation for Neural Network Verification

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 31 references that are in the map.
- First posted on arXiv 15 Dec 2022.

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

- [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)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [Scaling Polyhedral Neural Network Verification on GPUs](https://mlsanity.com/paper/2007.10868/) (2020)
- [NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation](https://mlsanity.com/paper/2009.09943/) (2020)
- [Geometric Path Enumeration for Equivalence Verification of Neural Networks](https://mlsanity.com/paper/2112.06582/) (2021)
- [ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs](https://mlsanity.com/paper/2106.05325/) (2021)

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

- [IoUCert: Robustness Verification for Anchor-based Object Detectors](https://mlsanity.com/paper/2603.03043/) (2026)
- [Extending Neural Network Verification to a Larger Family of Piece-wise Linear Activation Functions](https://mlsanity.com/paper/2311.10780/) (2023)
- [Scaling Neural Network Verification with Tensor Parallelism and Fully Sharded Data Parallelism](https://mlsanity.com/paper/2606.09377/) (2026)
- [Certified Training for Convolutional Perturbations](https://mlsanity.com/paper/2607.18195/) (2026)

## Abstract (arXiv)

Neural networks are increasingly applied in safety critical domains, their verification thus is gaining importance. A large class of recent algorithms for proving input-output relations of feed-forward neural networks are based on linear relaxations and symbolic interval propagation. However, due to variable dependencies, the approximations deteriorate with increasing depth of the network. In this paper we present DPNeurifyFV, a novel branch-and-bound solver for ReLU networks with low dimensional input-space that is based on symbolic interval propagation with fresh variables and input-splitting. A new heuristic for choosing the fresh variables allows to ameliorate the dependency problem, while our novel splitting heuristic, in combination with several other improvements, speeds up the branch-and-bound procedure. We evaluate our approach on the airborne collision avoidance networks ACAS Xu and demonstrate runtime improvements compared to state-of-the-art tools.