# Neural Network Verification as Piecewise Linear Optimization: Formulations for the Composition of Staircase Functions

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 38 references that are in the map.
- First posted on arXiv 27 Nov 2022.

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

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Towards Evaluating the Robustness of Neural Networks](https://mlsanity.com/paper/1608.04644/) (2016)
- [XNOR-Net: ImageNet Classification Using Binary Convolutional Neural Networks](https://mlsanity.com/paper/1603.05279/) (2016)
- [The Limitations of Deep Learning in Adversarial Settings](https://mlsanity.com/paper/1511.07528/) (2015)
- [Deep Learning in Neural Networks: An Overview](https://mlsanity.com/paper/1404.7828/) (2014)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Adversarial Examples for Evaluating Reading Comprehension Systems](https://mlsanity.com/paper/1707.07328/) (2017)
- [DoReFa-Net: Training Low Bitwidth Convolutional Neural Networks with Low Bitwidth Gradients](https://mlsanity.com/paper/1606.06160/) (2016)
- [Quantized Neural Networks: Training Neural Networks with Low Precision Weights and Activations](https://mlsanity.com/paper/1609.07061/) (2016)
- [Adversarial Attacks and Defenses in Images, Graphs and Text: A Review](https://mlsanity.com/paper/1909.08072/) (2019)
- [Towards Accurate Binary Convolutional Neural Network](https://mlsanity.com/paper/1711.11294/) (2017)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (2018)
- [Learning Activation Functions to Improve Deep Neural Networks](https://mlsanity.com/paper/1412.6830/) (2014)
- [The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification](https://mlsanity.com/paper/2006.14076/) (2020)
- [Adversarial Perturbations Against Deep Neural Networks for Malware Classification](https://mlsanity.com/paper/1606.04435/) (2016)
- [Tightened Convex Relaxations for Neural Network Robustness Certification](https://mlsanity.com/paper/2004.00570/) (2020)
- [Small and Strong Formulations for Unions of Convex Sets from the Cayley Embedding](https://mlsanity.com/paper/1704.03954/) (2017)
- [Embedding Formulations and Complexity for Unions of Polyhedra](https://mlsanity.com/paper/1506.01417/) (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)
- [Formal Verification of Markov Processes with Learned Parameters](https://mlsanity.com/paper/2501.15767/) (2025)

## Abstract (arXiv)

We present a technique for neural network verification using mixed-integer programming (MIP) formulations. We derive a strong formulation for each neuron in a network using piecewise linear activation functions. Additionally, as in general, these formulations may require an exponential number of inequalities, we also derive a separation procedure that runs in super-linear time in the input dimension. We first introduce and develop our technique on the class of staircase functions, which generalizes the ReLU, binarized, and quantized activation functions. We then use results for staircase activation functions to obtain a separation method for general piecewise linear activation functions. Empirically, using our strong formulation and separation technique, we can reduce the computational time in exact verification settings based on MIP and improve the false negative rate for inexact verifiers relying on the relaxation of the MIP formulation.