Verifying Neural Networks with Mixed Integer Programming

By Vincent Tjeng, Russ Tedrake. 2017

120 citations recorded by the source corpus.

Neural networks have demonstrated considerable success in a wide variety of real-world problems. However, the presence of adversarial examples - slightly perturbed inputs that are misclassified with high confidence - limits our ability to guarantee performance for these networks in safety-critical applications. We demonstrate that, for networks that are piecewise affine (for example, deep networks with ReLU and maxpool units), proving no adversarial example exists - or finding the closest example if one does exist - can be naturally formulated as solving a mixed integer program. Solves for a fully-connected MNIST classifier with three hidden layers can be completed an order of magnitude faster than those of the best existing approach. To address the concern that adversarial examples are irrelevant because pixel-wise attacks are unlikely to happen in natural images, we search for adversaries over a natural class of perturbations written as convolutions with an adversarial blurring kernel. When searching over blurred images, we find that as opposed to pixelwise attacks, some misclassifications are impossible. Even more interestingly, a small fraction of input images are provably robust to blurs: every blurred version of the input is classified with the same, correct label.

Subfields: Artificial Intelligence, Program Analysis & Verification

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 Program Analysis & Verification

Citations in the corpus

Training verified learners with learned verifiers (2018, neutral): “Algorithms based on formal verification [7, 10, 14] and mixed integer programming [9, 27] have been proposed to solve this problem for networks with piecewise linear activation functions (like ReLUs and maxpooling).”
Robustness May Be at Odds with Accuracy (2018, background): “…has there been progress towards models that achieve robustness that can be demonstrated empirically and, in some cases, even formally veriﬁed (Madry et al., 2017; Kolter & Wong, 2017; Sinha et al., 2017; Tjeng & Tedrake, 2017; Raghunathan et al., 2018; Dvijotham et al., 2018a; Xiao et al., 2018b).”
Scaling provable adversarial defenses (2018, background): “…(combinatorial) solvers to verify the robustness properties of networks, either via Satisﬁability Modulo Theories (SMT) solvers [Huang et al., 2017, Ehlers, 2017, Carlini and Wagner, 2017] or integer programming approaches [Lomuscio and Maganti, 2017, Tjeng and Tedrake, 2017, Cheng et al., 2017].”
A Dual Approach to Scalable Verification of Deep Networks (2018, background): “More recently, researchers have proposed a set of approaches that make use of branch and bound algorithms either directly or via mixed-integer programming solvers [Bunel et al., 2017, Cheng et al., 2017, Tjeng and Tedrake, 2017].”
On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models (2018, methodology): “However, when running a complete solver (using a MIP formulation), we are able to ﬁnd a counter-example that successfully induces the model to misclassify the “eight” as a “two” (as shown in Figure 6c).”
Semidefinite relaxations for certifying robustness to adversarial examples (2018, methodology): “A variety of robust MNIST networks are certiﬁed by Tjeng and Tedrake [26].”
An abstract domain for certifying neural networks (2019, methodology): “Complete verifiers are based on SMT solving [Ehlers 2017; Katz et al. 2017], mixed integer linear programming [Tjeng and Tedrake 2017] or input refinement [Wang et al. 2018] whereas existing incomplete verifiers are based on duality [Dvijotham et al. 2018; Raghunathan et al. 2018], abstract…”
Provable Robustness of ReLU networks via Maximization of Linear Regions (2018, background): “While globally optimal solutions can be obtained via mixed-integer optimization for small ReLU networks [25], this approach does not For each dataset and architecture we report the percentage of points of the test set for which we can compute the guaranteed optimal solution of (1) for models…”
Abduction-Based Explanations for Machine Learning Models (2018, methodology): “Although other recently proposed MILP encodings could be considered (Tjeng and Tedrake 2017), the most significant differences are in the algorithm used.”
Globally-Robust Neural Networks (2021, background): “L G ] 11 J un 2021 small models (Fischetti & Jo, 2018; Fromherz et al., 2021; Gehr et al., 2018; Jordan et al., 2019; Tjeng & Tedrake, 2017), requiring several orders of magnitude more time than a typical forward pass of a network; on moderately-large CNNs, these techniques either time out after…”
Output Range Analysis for Deep Feedforward Neural Networks (2018, methodology): “A similar encoding is also presented by Tjeng and Tedrake [27] for verifying robustness of neural network classifiers under a class of perturbations.”
Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability (2018, methodology): “Exact verification of networks has been the subject of many recent works (Katz et al., 2017; Ehlers, 2017; Carlini et al., 2017; Tjeng et al., 2017; Lomuscio and Maganti, 2017; Cheng et al., 2017a).”
Fast and Effective Robustness Certification (2018, methodology): “Complete verifiers do not have false positives but have limited scalability as they are based on computationally expensive methods such as SMT solving [14, 8], mixed integer linear programming [27] or input refinement [28].”
A randomized gradient-free attack on ReLU networks (2018, methodology): “[16,5], and for ReLU networks a few formulations have been proposed for the exact solution [10,3,24], most notably [24] which uses mixed-integer programming to achieve this.”