Strong mixed-integer programming formulations for trained neural networks
This work addresses a computational bottleneck in neural network verification for researchers and practitioners in optimization and AI, offering a more scalable method, though it is incremental as it builds on existing MIP techniques.
The paper tackles the problem of formulating trained neural networks as mixed-integer programs (MIPs) by introducing an ideal formulation for ReLU units that uses a single binary variable and no extra continuous variables, but requires exponentially many constraints, with a linear-time separation routine. The result shows that dynamically separating these constraints improves computational efficiency, reducing solve times by a factor of 7 on smaller instances and nearly matching dual bounds on harder instances in much less time.
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.