# Strong mixed-integer programming formulations for trained neural networks

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

## Key facts

- Cited by 115 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Nov 2018.

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

- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [Towards Lower Bounds on the Depth of ReLU Neural Networks](https://mlsanity.com/paper/2105.14835/) (2021)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [Partition-based formulations for mixed-integer optimization of trained ReLU neural networks](https://mlsanity.com/paper/2102.04373/) (2021)
- [When Deep Learning Meets Polyhedral Theory: A Survey](https://mlsanity.com/paper/2305.00241/) (2023)
- [OMLT: Optimization & Machine Learning Toolkit](https://mlsanity.com/paper/2202.02414/) (2022)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [Unsupervised Learning for Combinatorial Optimization with Principled Objective Relaxation](https://mlsanity.com/paper/2207.05984/) (2022)
- [Mixed-Integer Optimization with Constraint Learning](https://mlsanity.com/paper/2111.04469/) (2021)
- [Physics-Informed Neural Networks with Hard Linear Equality Constraints](https://mlsanity.com/paper/2402.07251/) (2024)
- [Strong Optimal Classification Trees](https://mlsanity.com/paper/2103.15965/) (2021)
- [Optimization with Constraint Learning: A Framework and Survey](https://mlsanity.com/paper/2110.02121/) (2021)
- [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)
- [Expressive Losses for Verified Robustness via Convex Combinations](https://mlsanity.com/paper/2305.13991/) (2023)
- [IBP Regularization for Verified Adversarial Robustness via Branch-and-Bound](https://mlsanity.com/paper/2206.14772/) (2022)
- [Scaling Up Exact Neural Network Compression by ReLU Stability](https://mlsanity.com/paper/2102.07804/) (2021)
- [Finding Regions of Counterfactual Explanations via Robust Optimization](https://mlsanity.com/paper/2301.11113/) (2023)
- [Maximizing information from chemical engineering data sets: Applications to machine learning](https://mlsanity.com/paper/2201.10035/) (2022)
- [CertiFair: A Framework for Certified Global Fairness of Neural Networks](https://mlsanity.com/paper/2205.09927/) (2022)
- [Neur2SP: Neural Two-Stage Stochastic Programming](https://mlsanity.com/paper/2205.12006/) (2022)
- [Learning to Solve Vehicle Routing Problems: A Survey](https://mlsanity.com/paper/2205.02453/) (2022)
- [Model-Based Control with Sparse Neural Dynamics](https://mlsanity.com/paper/2312.12791/) (2023)
- [Incremental Verification of Neural Networks](https://mlsanity.com/paper/2304.01874/) (2023)
- [Traversing the Local Polytopes of ReLU Neural Networks: A Unified Approach for Network Verification](https://mlsanity.com/paper/2111.08922/) (2021)
- [Between steps: Intermediate relaxations between big-M and convex hull formulations](https://mlsanity.com/paper/2101.12708/) (2021)
- [Optimizing Objective Functions from Trained ReLU Neural Networks via Sampling](https://mlsanity.com/paper/2205.14189/) (2022)
- [Stability Verification of Neural Network Controllers using Mixed-Integer Programming](https://mlsanity.com/paper/2206.13374/) (2022)
- [Scaling the Convex Barrier with Sparse Dual Algorithms](https://mlsanity.com/paper/2101.05844/) (2021)

## Abstract (arXiv)

We present an ideal mixed-integer programming (MIP) formulation for a rectified linear unit (ReLU) appearing in a trained neural network. Our formulation requires a single binary variable and no additional continuous variables beyond the input and output variables of the ReLU. We contrast it with an ideal "extended" formulation with a linear number of additional continuous variables, derived through standard techniques. An apparent drawback of our formulation is that it requires an exponential number of inequality constraints, but we provide a routine to separate the inequalities in linear time. We also prove that these exponentially-many constraints are facet-defining under mild conditions. Finally, we study network verification problems and observe that dynamically separating from the exponential inequalities 1) is much more computationally efficient and scalable than the extended formulation, 2) decreases the solve time of a state-of-the-art MIP solver by a factor of 7 on smaller instances, and 3) nearly matches the dual bounds of a state-of-the-art MIP solver on harder instances, after just a few rounds of separation and in orders of magnitude less time.