# Output Range Analysis for Deep Neural Networks

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

## Key facts

- Cited by 30 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Sep 2017.

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

- [How to Certify Machine Learning Based Safety-critical Systems? A Systematic Literature Review](https://mlsanity.com/paper/2107.12045/) (2021)
- [How to Robustify Black-Box ML Models? A Zeroth-Order Optimization Perspective](https://mlsanity.com/paper/2203.14195/) (2022)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [Minimal Multi-Layer Modifications of Deep Neural Networks](https://mlsanity.com/paper/2110.09929/) (2021)
- [Incremental Verification of Neural Networks](https://mlsanity.com/paper/2304.01874/) (2023)
- [QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks](https://mlsanity.com/paper/2212.11138/) (2022)
- [Learning Density Distribution of Reachable States for Autonomous Systems](https://mlsanity.com/paper/2109.06728/) (2021)
- [Certified Zeroth-order Black-Box Defense with Robust UNet Denoiser](https://mlsanity.com/paper/2304.06430/) (2023)
- [Linearity Grafting: Relaxed Neuron Pruning Helps Certifiable Robustness](https://mlsanity.com/paper/2206.07839/) (2022)
- [A Survey on Verification and Validation, Testing and Evaluations of Neurosymbolic Artificial Intelligence](https://mlsanity.com/paper/2401.03188/) (2024)
- [CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness](https://mlsanity.com/paper/2206.03044/) (2022)
- [Neural Network Verification with PyRAT](https://mlsanity.com/paper/2410.23903/) (2024)
- [Tighter Abstract Queries in Neural Network Verification](https://mlsanity.com/paper/2210.12871/) (2022)
- [Reachable Polyhedral Marching (RPM): An Exact Analysis Tool for Deep-Learned Control Systems](https://mlsanity.com/paper/2210.08339/) (2022)
- [Insta-RS: Instance-wise Randomized Smoothing for Improved Robustness and Accuracy](https://mlsanity.com/paper/2103.04436/) (2021)
- [Safety Verification for Neural Networks Based on Set-boundary Analysis](https://mlsanity.com/paper/2210.04175/) (2022)
- [Certified Adversarial Robustness Within Multiple Perturbation Bounds](https://mlsanity.com/paper/2304.10446/) (2023)
- [Feed-Forward Neural Networks as a Mixed-Integer Program](https://mlsanity.com/paper/2402.06697/) (2024)
- [Towards Formal Verification of Deep Neural Networks for Object Detection](https://mlsanity.com/paper/2407.01295/) (2024)
- [A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning enabled Control Systems](https://mlsanity.com/paper/2303.05394/) (2023)
- [Verification of Neural Network Control Systems using Symbolic Zonotopes and Polynotopes](https://mlsanity.com/paper/2306.14619/) (2023)
- [A Novel Framework for Threat Analysis of Machine Learning-based Smart Healthcare Systems](https://mlsanity.com/paper/2103.03472/) (2021)
- [Model-Agnostic Reachability Analysis on Deep Neural Networks](https://mlsanity.com/paper/2304.00813/) (2023)
- [Verifying Safety of Neural Networks from Topological Perspectives](https://mlsanity.com/paper/2306.15403/) (2023)
- [Performance Bounds for Neural Network Estimators: Applications in Fault Detection](https://mlsanity.com/paper/2103.12141/) (2021)
- [Failing with Grace: Learning Neural Network Controllers that are Boundedly Unsafe](https://mlsanity.com/paper/2106.11881/) (2021)
- [Safe AI -- How is this Possible?](https://mlsanity.com/paper/2201.10436/) (2022)
- [PCV: A Point Cloud-Based Network Verifier](https://mlsanity.com/paper/2301.11806/) (2023)
- [A simple algorithm for output range analysis for deep neural networks](https://mlsanity.com/paper/2407.02700/) (2024)
- [Exact and Asymptotically Complete Robust Verifications of Neural Networks via Ising Solvers](https://mlsanity.com/paper/2603.00408/) (2026)

## Abstract (arXiv)

Deep neural networks (NN) are extensively used for machine learning tasks such as image classification, perception and control of autonomous systems. Increasingly, these deep NNs are also been deployed in high-assurance applications. Thus, there is a pressing need for developing techniques to verify neural networks to check whether certain user-expected properties are satisfied. In this paper, we study a specific verification problem of computing a guaranteed range for the output of a deep neural network given a set of inputs represented as a convex polyhedron. Range estimation is a key primitive for verifying deep NNs. We present an efficient range estimation algorithm that uses a combination of local search and linear programming problems to efficiently find the maximum and minimum values taken by the outputs of the NN over the given input set. In contrast to recently proposed "monolithic" optimization approaches, we use local gradient descent to repeatedly find and eliminate local minima of the function. The final global optimum is certified using a mixed integer programming instance. We implement our approach and compare it with Reluplex, a recently proposed solver for deep neural networks. We demonstrate the effectiveness of the proposed approach for verification of NNs used in automated control as well as those used in classification.