# ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 42 references that are in the map.
- First posted on arXiv 9 Jun 2021.

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

- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [Improved Precision and Recall Metric for Assessing Generative Models](https://mlsanity.com/paper/1904.06991/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Adversarial Examples: Attacks and Defenses for Deep Learning](https://mlsanity.com/paper/1712.07107/) (2017)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [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)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [Parallelization Techniques for Verifying Neural Networks](https://mlsanity.com/paper/2004.08440/) (2020)
- [Neural Bridge Sampling for Evaluating Safety-Critical Autonomous Systems](https://mlsanity.com/paper/2008.10581/) (2020)
- [ReluDiff: Differential Verification of Deep Neural Networks](https://mlsanity.com/paper/2001.03662/) (2020)
- [Verification of Image-based Neural Network Controllers Using Generative Models](https://mlsanity.com/paper/2105.07091/) (2021)
- [Global Optimization of Objective Functions Represented by ReLU Networks](https://mlsanity.com/paper/2010.03258/) (2020)
- [Validation of Image-Based Neural Network Controllers through Adaptive Stress Testing](https://mlsanity.com/paper/2003.02381/) (2020)
- [Robustness Certification of Generative Models](https://mlsanity.com/paper/2004.14756/) (2020)
- [Fast Neural Network Verification via Shadow Prices](https://mlsanity.com/paper/1902.07247/) (2019)
- [Correctness Verification of Neural Networks](https://mlsanity.com/paper/1906.01030/) (2019)
- [Generating Probabilistic Safety Guarantees for Neural Network Controllers](https://mlsanity.com/paper/2103.01203/) (2021)
- [On Computing the Minkowski Difference of Zonotopes](https://mlsanity.com/paper/1512.02794/) (2015)

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

- [When Deep Learning Meets Polyhedral Theory: A Survey](https://mlsanity.com/paper/2305.00241/) (2023)
- [Optimized Symbolic Interval Propagation for Neural Network Verification](https://mlsanity.com/paper/2212.08567/) (2022)

## Abstract (arXiv)

Deep neural networks often lack the safety and robustness guarantees needed to be deployed in safety critical systems. Formal verification techniques can be used to prove input-output safety properties of networks, but when properties are difficult to specify, we rely on the solution to various optimization problems. In this work, we present an algorithm called ZoPE that solves optimization problems over the output of feedforward ReLU networks with low-dimensional inputs. The algorithm eagerly splits the input space, bounding the objective using zonotope propagation at each step, and improves computational efficiency compared to existing mixed-integer programming approaches. We demonstrate how to formulate and solve three types of optimization problems: (i) minimization of any convex function over the output space, (ii) minimization of a convex function over the output of two networks in series with an adversarial perturbation in the layer between them, and (iii) maximization of the difference in output between two networks. Using ZoPE, we observe a 25× speedup on property 1 of the ACAS Xu neural network verification benchmark compared to several state-of-the-art verifiers, and an 85× speedup on a set of linear optimization problems compared to a mixed-integer programming baseline. We demonstrate the versatility of the optimizer in analyzing networks by projecting onto the range of a generative adversarial network and visualizing the differences between a compressed and uncompressed network.