Deep Neural Networks as 0-1 Mixed Integer Linear Programs: A Feasibility Study

By Matteo Fischetti, Jason Jo. 2017

84 citations recorded by the source corpus.

Deep Neural Networks (DNNs) are very popular these days, and are the subject of a very intense investigation. A DNN is made by layers of internal units (or neurons), each of which computes an affine combination of the output of the units in the previous layer, applies a nonlinear operator, and outputs the corresponding value (also known as activation). A commonly-used nonlinear operator is the so-called rectified linear unit (ReLU), whose output is just the maximum between its input value and zero. In this (and other similar cases like max pooling, where the max operation involves more than one input value), one can model the DNN as a 0-1 Mixed Integer Linear Program (0-1 MILP) where the continuous variables correspond to the output values of each unit, and a binary variable is associated with each ReLU to model its yes/no nature. In this paper we discuss the peculiarity of this kind of 0-1 MILP models, and describe an effective bound-tightening technique intended to ease its solution. We also present possible applications of the 0-1 MILP model arising in feature visualization and in the construction of adversarial examples. Preliminary computational results are reported, aimed at investigating (on small DNNs) the computational performance of a state-of-the-art MILP solver when applied to a known test case, namely, hand-written digit recognition.

How researchers see this paper

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

1. Huan Zhang
2. Hadi Salman
3. Shiqi Wang
4. Cho-Jui Hsieh
5. Greg Yang
6. Hongge Chen
7. Tsui-Wei Weng
8. Eric Wong

Citations in the corpus

• Provably Robust Deep Learning via Adversarially Trained Smoothed Classifiers (2019, methodology): “Exact methods, usually based on Satisfiability Modulo Theories solvers [18, 11] or mixed integer linear programming [33, 24, 12], are guaranteed to find an adversarial example around a datapoint if it exists.”
• Towards Fast Computation of Certified Robustness for ReLU Networks (2018, methodology): “For ReLU networks, the verification problem can be transformed into a Mixed Integer Linear Programming (MILP) problem (Lomuscio & Maganti, 2017; Cheng et al., 2017; Fischetti & Jo, 2017) by using binary variables to encode the states of ReLU activation in each neuron.”
• A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks (2019, methodology): “…solve the robustness verification problem (1) by typically employing MILP solvers (Cheng et al., 2017; Lomuscio & Maganti, 2017; Dutta et al., 2018; Fischetti & Jo, 2017; Tjeng et al., 2019; Xiao et al., 2019) or Satisfiability Modulo Theories (SMT) solvers (Scheibler et al., 2015; Katz et al.,…”
• MixTrain: Scalable Training of Formally Robust Neural Networks (2018, background): “MILP solver achieves better performance [60], [61], [62], but they still suffer from high nonlinearity of resulting formulas.”
• Evaluating Robustness of Neural Networks with Mixed Integer Programming (2017, methodology): “Complete verifiers typically employ either MILP solvers [10, 12, 15, 29] or SMT [6, 14, 27, 35].”
• Efficient Neural Network Robustness Certification with General Activation Functions (2018, methodology): “3, we can compute analytic output bounds efficiently without resorting to any optimization solvers for general `p distortion, and the time complexity for an m-layer ReLU network is polynomial time in contrast to Reluplex or Mixed-Integer Optimization-based approach [22, 23] where SMT and MIO solvers”