Strong mixed-integer programming formulations for trained neural networks

By Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, Juan Pablo Vielma. Mathematical programming, 2018

321 citations recorded by the source corpus.

We present strong mixed-integer programming (MIP) formulations for high-dimensional piecewise linear functions that correspond to trained neural networks. These formulations can be used for a number of important tasks, such as verifying that an image classification network is robust to adversarial inputs, or solving decision problems where the objective function is a machine learning model. We present a generic framework, which may be of independent interest, that provides a way to construct sharp or ideal formulations for the maximum of d affine functions over arbitrary polyhedral input domains. We apply this result to derive MIP formulations for a number of the most popular nonlinear operations (e.g. ReLU and max pooling) that are strictly stronger than other approaches from the literature. We corroborate this computationally, showing that our formulations are able to offer substantial improvements in solve time on verification tasks for image classification networks.

Subfields: Artificial Intelligence, Computer Vision and Pattern Recognition

View Paper: https://www.semanticscholar.org/paper/ba73fe5e00212289dea15c642a2bd0e1db3b9b6c

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Vision and Pattern Recognition

Citations in the corpus

CAQL: Continuous Action Q-Learning (2019, methodology): “…MIP model have been used in neural network veriﬁcation (Cheng et al., 2017; Lomuscio & Maganti, 2017; Bunel et al., 2018; Dutta et al., 2018; Fischetti & Jo, 2018; Anderson et al., 2019; Tjeng et al., 2019) and analysis (Serra et al., 2018; Kumar et al., 2019), but its application to RL is novel .”
A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks (2019, background): “It is possible to obtain other (maybe tighter) convex relaxations (Anderson et al., 2018), but it comes with more assumptions on the nonlinear layers and more complex convex constraints.”