Neural networks trained only to optimize for training accuracy can often be fooled by adversarial examples --- slightly perturbed inputs misclassified with high confidence. Verification of networks enables us to gauge their vulnerability to such adversarial examples. We formulate verification of piecewise-linear neural networks as a mixed integer program. On a representative task of finding minimum adversarial distortions, our verifier is two to three orders of magnitude quicker than the state-of-the-art. We achieve this computational speedup via tight formulations for non-linearities, as well as a novel presolve algorithm that makes full use of all information available. The computational speedup allows us to verify properties on convolutional and residual networks with over 100,000 ReLUs --- several orders of magnitude more than networks previously verified by any complete verifier. In particular, we determine for the first time the exact adversarial accuracy of an MNIST classifier to perturbations with bounded l-∞ norm ε=0.1: for this classifier, we find an adversarial example for 4.38% of samples, and a certificate of robustness to norm-bounded perturbations for the remainder. Across all robust training procedures and network architectures considered, and for both the MNIST and CIFAR-10 datasets, we are able to certify more samples than the state-of-the-art and find more adversarial examples than a strong first-order attack. Neural networks trained only to optimize for training accuracy have been shown to be vulnerable to adversarial examples: perturbed inputs that are very similar to some regular input but for which the output is radically different BID14 . There is now a large body of work proposing defense methods to produce classifiers that are more robust to adversarial examples. However, as long as a defense is evaluated only via heuristic attacks (such as the Fast Gradient Sign Method (FGSM) (Goodfellow et al., 2015) or BID6 's attack (CW)), we have no guarantee that the defense actually increases the robustness of the classifier produced. Defense methods thought to be successful when published have often later been found to be vulnerable to a new class of attacks. For instance, multiple defense methods are defeated in BID5 by constructing defense-specific loss functions and in BID0 by overcoming obfuscated gradients.Fortunately, we can evaluate robustness to adversarial examples in a principled fashion. One option is to determine (for each test input) the minimum distance to the closest adversarial example, which we call the minimum adversarial distortion BID7 . Alternatively, we can determine the adversarial test accuracy BID1 , which is the proportion of the test set for which no perturbation in some bounded class causes a misclassification. An increase in the mean minimum adversarial distortion or in the adversarial test accuracy indicates an improvement in robustness. 1 We present an efficient implementation of a mixed-integer linear programming (MILP) verifier for properties of piecewise-linear feed-forward neural networks. Our tight formulation for nonlinearities and our novel presolve algorithm combine to minimize the number of binary variables in the MILP problem and dramatically improve its numerical conditioning. Optimizations in our MILP implementation improve performance by several orders of magnitude when compared to a naïve MILP implementation, and we are two to three orders of magnitude faster than the state-of-the-art Satisfiability Modulo Theories (SMT) based verifier, Reluplex BID7 We make the following key contributions:• We demonstrate that, despite considering the full combinatorial nature of the network, our verifier can succeed at evaluating the robustness of larger neural networks, including those with convolutional and residual layers.• We identify why we can succeed on larger neural networks with hundreds of thousands of units. First , a large fraction of the ReLUs can be shown to be either always active or always inactive over the bounded input domain. Second , since the predicted label is determined by the unit in the final layer with the maximum activation, proving that a unit never has the maximum activation over all bounded perturbations eliminates it from consideration. We exploit both phenomena, reducing the overall number of non-linearities considered.• We determine for the first time the exact adversarial accuracy for MNIST classifiers to perturbations with bounded l ∞ norm . We are also able to certify more samples than the state-of-the-art and find more adversarial examples across MNIST and CIFAR-10 classifiers with different architectures trained with a variety of robust training procedures.Our code is available at https://github.com/vtjeng/MIPVerify.jl. This paper presents an efficient complete verifier for piecewise-linear neural networks.While we have focused on evaluating networks on the class of perturbations they are designed to be robust to, defining a class of perturbations that generates images perceptually similar to the original remains an important direction of research. Our verifier is able to handle new classes of perturbations (such as convolutions applied to the original image) as long as the set of perturbed images is a union of polytopes in the input space.We close with ideas on improving verification of neural networks. First, our improvements can be combined with other optimizations in solving MILPs. For example, BID4 DISPLAYFORM0 We consider two cases.Recall that a is the indicator variable a = 1 x≥0 .When a = 0, the constraints in Equation FORMULA0 This formulation for rectified linearities is sharp BID15 if we have no further information about x. This is the case since relaxing the integrality constraint on a leads to (x, y) being restricted to an area that is the convex hull of y = max(x, 0). However , if x is an affine expression x = w T z + b, the formulation is no longer sharp, and we can add more constraints using bounds we have on z to improve the problem formulation.
We efficiently verify the robustness of deep neural models with over 100,000 ReLUs, certifying more samples than the state-of-the-art and finding more adversarial examples than a strong first-order attack. Performs a careful study of mixed integer linear programming approaches for verifying robustness of neural networks to adversarial perturbations and proposes three enhancements to MILP formulations of neural network verification.