Source-linked AI summary
Strong mixed-integer programming formulations for trained neural networks
Ross Anderson, Joey Huchette, Christian Tjandraatmadja, Juan Pablo Vielma
TL;DR
Optimization problems containing trained neural networks require formulations that support provably optimal solutions, especially for verification, where rigorous dual bounds matter. This paper develops an ideal, non-extended ReLU formulation and shows that separating its inequalities can strengthen bounds efficiently compared with alternative formulations.
Problem
Optimization over trained neural networks arises in applications including deep reinforcement learning and neural-network verification, where provably optimal solutions and rigorous dual bounds are important.
Method
The paper formulates a ReLU using only its original input and output variables plus one binary variable, with exponentially many inequalities, linear-time separation, and facet-defining guarantees under mild conditions.
Results
The separated inequalities improve LP bounds by more than 15% on average while taking roughly 2.5 times as long as the baseline, whereas the extended formulation cannot solve its LP relaxation within 30 minutes.
Takeaways & Limitations
Restricting cutting planes to the proposed inequality family produces substantially stronger bounds than generic short-time cut generation and does so far faster than the extended formulation.
Takeaways & Limitations
The commonly used big-M formulation is not necessarily ideal and can admit LP-relaxation points outside the convex hull of the ReLU graph.
Abstract
from arXiv · showhide
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.
1 Introduction
The paper develops ideal MIP formulations for embedding trained ReLU neural networks in optimization, motivated especially by verification tasks requiring provably optimal solutions and rigorous dual bounds.
- 1 Introduction: Trained feedforward ReLU networks support predictive tasks including image classification, speech recognition, machine translation, and robotics and control.Each neuron applies a ReLU to an affine function with learned weights and bias; specialized linear transformations can be reduced to this model after training.
- 1 Introduction: Optimization over trained neural networks arises in reinforcement learning, robustness verification, and image-generation problems.These applications may use learned cost, transition, or perception functions inside optimization models.
- 1 Introduction: MIP provides provably optimal solutions and rigorous dual bounds, unlike heuristic or local-search approaches that primarily produce feasible solutions.The paper identifies verification as a setting where such bounds can guarantee robustness.
- 1.1 MIP formulation preliminaries: The paper focuses on formulating each ReLU neuron over a bounded affine-input domain, using a binary variable to indicate its active or inactive branch.Whole-network formulations can be assembled from formulations for individual neurons.
- 1.1 MIP formulation preliminaries: Its main contribution is an ideal non-extended ReLU formulation with one binary variable, no auxiliary continuous variables, exponentially many inequalities, and a linear-time separation routine.The inequalities are facet-defining under mild conditions, and the formulation is obtained by projecting an ideal extended formulation.
- 1 Introduction: The formulation targets weaknesses of prevalent big-M approaches, which are not necessarily ideal or exact convex relaxations for individual ReLU neurons.The paper also situates the work among convex-relaxation, satisfiability, constraint-programming, global-optimization, and predict-then-optimize approaches.
2 The ReLU neuron
The section compares big-M and extended formulations for a ReLU neuron before introducing an ideal non-extended formulation that preserves tightness without auxiliary continuous variables.
- 2.1 A big-M formulation: The standard big-M formulation uses one binary variable but may fail to provide an exact convex relaxation.A feasible LP-relaxation point can project outside the convex hull of the ReLU graph, so the formulation is not ideal.
- 2.1 A big-M formulation: The big-M formulation can have an arbitrarily bad integrality gap, even when the input dimension η is fixed.The example constructs a point where the convex-hull relaxation requires y=0, while the big-M relaxation deviates by at least 1/2.
- 2.2 An ideal extended formulation: The multiple-choice formulation is ideal but introduces auxiliary continuous variables, producing quadratic growth in network size.Applied across layers, it requires m0 + Σ_i=1^r (m_i−1+1)m_i continuous variables and may suffer from degeneracy in simplex-based branch-and-bound.
- 2.3 An ideal non-extended formulation: The proposed non-extended formulation is ideal, uses only the original input/output variables and one binary variable, and matches the multiple-choice formulation’s strength.It is obtained by projecting an ideal extended formulation and adds an exponential family of inequalities to the big-M model.
- 2.3 An ideal non-extended formulation: Each inequality in the exponential family is facet-defining and necessary under the strict-activity assumption.Strict activity excludes neurons that are always inactive or always affine, and the resulting formulation is minimal modulo variable bounds.
- 2.3 An ideal non-extended formulation: The exponential inequalities can be separated in linear time by selecting the subset that minimizes the right-hand side.For any violated inequality, Proposition 3 identifies the most violated member through independent componentwise choices.
3 Computational experiments
The experiments evaluate ReLU formulations on MNIST verification problems using smaller and larger convolutional networks, comparing solve performance and root-node dual bounds.
- Verification setup: The study verifies robustness by maximizing the logit difference between a target adversarial class and the true class within an infinity-norm perturbation ball.A negative optimum or valid dual bound verifies robustness against that target class.
- Networks and instances: The experiments use smaller and larger convolutional ReLU networks, with TensorFlow pseudocode documenting their architectures.The smaller model has a dense ReLU layer with 16 neurons before the final 10-output linear layer.
- Small ReLU network: 7 times faster on average, big-M + (6b) solves the smaller-network instances faster than the big-M formulation.Big-M fails to prove optimality within 30 minutes on 79 of 100 instances and is never fastest; using some cuts is important because big-M + no cuts times out on every instance.
- Small ReLU network: The extended method is roughly 5 times slower than big-M + (6b) but times out on only 19 instances, making it more reliable than big-M for the smaller network.The authors attribute the computational improvement to the stronger ideal formulations.
- Larger ReLU network: The extended formulation’s LP relaxation cannot be solved within 30 minutes on any larger-network instance because its size grows quadratically.Big-M + (6b) strengthens the baseline dual bound by more than 15% on average while taking roughly 2.5 times as long.
- Larger ReLU network: The big-M method achieves roughly 18% improvement but requires almost two orders of magnitude more time than big-M + (6b).With a 15-second limit, big-M achieves less than 4% improvement, suggesting the targeted inequalities are not trivial for generic cutting planes to infer.
A.1 Proof of Proposition 1
The proof derives the projected formulation by Fourier–Motzkin elimination, handling zero and negative weights before removing redundant inequalities.
- Projection: Fourier–Motzkin elimination projects out auxiliary and intermediate variables from formulation (5), leaving a system involving the original input variables.The elimination proceeds component by component after eliminating x1, y0, and y1.
- Special cases: Zero-weight input components yield their original bounds Li <= xi <= Ui after elimination.Such components appear only in the corresponding bound constraints.
- Special cases: Negative weights are handled by introducing an auxiliary variable ˜xi = -xi, reversing its bounds, and proceeding with nonnegative weights.The transformed coefficients use wi <- |wi|, Li <- -Ui, and Ui <- -Li.
- Redundancy: The inequalities indexed by subsets of supp(w) are shown redundant when their associated coefficient expression has either nonnegative or negative sign.Each case represents the targeted inequality as a conic combination of remaining constraints.
A.2 Proof of Proposition 2
The proof establishes facet-defining status by constructing enough feasible points satisfying one inequality at equality and proving their affine independence.
- Assumptions: The proof assumes nonnegative weights and selects a subset I of indices without loss of generality by permuting rows and interchanging signs.Under this assumption, the transformed bounds coincide with the original bounds.
- Feasible points: It constructs two endpoint points and perturbed points that remain feasible and satisfy the selected inequality at equality under strict activity.The perturbations move lower-bound coordinates outside I and upper-bound coordinates inside I.
- Affine independence: η + 2 feasible points are shown to be affinely independent using a matrix with full row rank.Permuting the z column produces an upper-triangular matrix with a nonzero diagonal.