# On Optimizing Back-Substitution Methods for Neural Network Verification

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 28 of its 62 references that are in the map.
- First posted on arXiv 16 Aug 2022.

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

- [Very Deep Convolutional Networks for Large-Scale Image Recognition](https://mlsanity.com/paper/1409.1556/) (2014)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Concrete Problems in AI Safety](https://mlsanity.com/paper/1606.06565/) (2016)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (2018)
- [Measuring Neural Net Robustness with Constraints](https://mlsanity.com/paper/1605.07262/) (2016)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [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)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)
- [Towards Scalable Verification of Deep Reinforcement Learning](https://mlsanity.com/paper/2105.11931/) (2021)
- [DeepAbstract: Neural Network Abstraction for Accelerating Verification](https://mlsanity.com/paper/2006.13735/) (2020)
- [Verifying Recurrent Neural Networks using Invariant Inference](https://mlsanity.com/paper/2004.02462/) (2020)
- [Global Optimization of Objective Functions Represented by ReLU Networks](https://mlsanity.com/paper/2010.03258/) (2020)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [Efficient Neural Network Analysis with Sum-of-Infeasibilities](https://mlsanity.com/paper/2203.11201/) (2022)
- [Scalable Polyhedral Verification of Recurrent Neural Networks](https://mlsanity.com/paper/2005.13300/) (2020)
- [Pruning and Slicing Neural Networks using Formal Verification](https://mlsanity.com/paper/2105.13649/) (2021)
- [Verification-Aided Deep Ensemble Selection](https://mlsanity.com/paper/2202.03898/) (2022)
- [Neural Network Verification using Residual Reasoning](https://mlsanity.com/paper/2208.03083/) (2022)

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

- [VeriX: Towards Verified Explainability of Deep Neural Networks](https://mlsanity.com/paper/2212.01051/) (2022)
- [Convex Bounds on the Softmax Function with Applications to Robustness Verification](https://mlsanity.com/paper/2303.01713/) (2023)
- [Towards Verified and Targeted Explanations through Formal Methods](https://mlsanity.com/paper/2604.14209/) (2026)
- [Neural Network Verification using Partial Multi-Neuron Relaxation](https://mlsanity.com/paper/2605.30155/) (2026)
- [Shifting-based Optimizable Linear Relaxations for General Activation Functions](https://mlsanity.com/paper/2606.20292/) (2026)
- [Mining Verdict Boundaries for Neural Network Verification](https://mlsanity.com/paper/2607.28954/) (2026)

## Abstract (arXiv)

With the increasing application of deep learning in mission-critical systems, there is a growing need to obtain formal guarantees about the behaviors of neural networks. Indeed, many approaches for verifying neural networks have been recently proposed, but these generally struggle with limited scalability or insufficient accuracy. A key component in many state-of-the-art verification schemes is computing lower and upper bounds on the values that neurons in the network can obtain for a specific input domain -- and the tighter these bounds, the more likely the verification is to succeed. Many common algorithms for computing these bounds are variations of the symbolic-bound propagation method; and among these, approaches that utilize a process called back-substitution are particularly successful. In this paper, we present an approach for making back-substitution produce tighter bounds. To achieve this, we formulate and then minimize the imprecision errors incurred during back-substitution. Our technique is general, in the sense that it can be integrated into numerous existing symbolic-bound propagation techniques, with only minor modifications. We implement our approach as a proof-of-concept tool, and present favorable results compared to state-of-the-art verifiers that perform back-substitution.