PaperlayerView exact revision on arXiv

Source-linked AI summary

Evaluating Robustness of Neural Networks with Mixed Integer Programming

Vincent Tjeng, Kai Xiao, Russ Tedrake

arXiv:1711.07356v3cs.LGcs.CRcs.CV

TL;DR

Heuristic attacks alone cannot guarantee that a defense improves neural-network robustness. This paper formulates verification of piecewise-linear networks as a MILP and develops a faster verifier. It reports faster minimum-distortion verification, broader network coverage, and exact adversarial-accuracy evaluation for MNIST classifiers.

  • Problem

    Evaluating defenses only with heuristic attacks does not guarantee that they improve robustness to adversarial examples.

    Source: §1 · p. 1

  • Method

    The paper formulates verification of piecewise-linear neural networks as a MILP, using tight nonlinearity formulations and a presolve algorithm.

    Source: §1 · p. 1

  • Results

    The verifier is two to three orders of magnitude faster than Reluplex on minimum adversarial distortion and certifies more samples while finding more adversarial examples across the evaluated classifiers and procedures.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The verifier determines exact adversarial accuracy for MNIST classifiers and can verify larger networks, including convolutional and residual architectures.

    Source: §1 · p. 2

    The verifier handles new perturbation classes when the set of perturbed images is a union of polytopes, while defining perceptually similar perturbations remains an important research direction.

    Source: §6 · p. 9

Abstract

from arXiv · show

Neural networks have demonstrated considerable success on a wide variety of real-world problems. However, networks trained only to optimize for training accuracy can often be fooled by adversarial examples - slightly perturbed inputs that are 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 networks with an order of magnitude more ReLUs 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_\infty$ norm $\epsilon=0.1$: for this classifier, we find an adversarial example for 4.38% of samples, and a certificate of robustness (to perturbations with bounded norm) for the remainder. Across all robust training procedures and network architectures considered, we are able to certify more samples than the state-of-the-art and find more adversarial examples than a strong first-order attack.

1 INTRODUCTION

Heuristic attacks alone cannot guarantee that a defense improves robustness, motivating principled verification. The paper presents a faster MILP verifier and applies it to larger networks and exact adversarial-accuracy evaluation.

1 INTRODUCTION

  • Minimum adversarial distortion and adversarial test accuracy are complementary measures of robustness, and bounded-perturbation certificates can be used iteratively to find minimum distortions.An increase in either mean minimum distortion or adversarial test accuracy indicates improved robustness.Source: §1 · p. 1
  • The verifier is two to three orders of magnitude faster than the state-of-the-art SMT-based Reluplex verifier on minimum adversarial distortion.Its tight nonlinearity formulation and presolve algorithm reduce binary variables and improve numerical conditioning.Source: §1 · pp. 1–2
  • The verifier handles larger networks, including convolutional and residual architectures.The paper identifies networks with hundreds of thousands of units as within reach.Source: §1 · p. 2
  • Eliminating ReLUs known to be always active or inactive and output units that cannot win reduces the nonlinearities requiring verification.These reductions use the bounded input domain and the final-layer maximum that determines the predicted label.Source: §1 · p. 2
  • The verifier determines exact adversarial accuracy for MNIST classifiers and certifies more samples while finding more adversarial examples than competing approaches.The reported comparisons span MNIST and CIFAR-10 classifiers, architectures, and robust training procedures.Source: §1 · p. 2

2 RELATED WORK

Related work distinguishes complete from incomplete verification and places MILP verification alongside SMT approaches. The paper compares its verifier with prior approaches and describes how complete verification complements robust training.

2 RELATED WORK

  • Incomplete verifiers reason over an outer approximation of the adversarial polytope, while complete verifiers reason over the exact set and can resolve any query given sufficient time.Under a time limit, complete verifiers resolve only a fraction of queries; extending the limit can increase that fraction.Source: §2 · p. 2
  • Incomplete robustness verifiers use methods including duality, layerwise approximations, discretization, abstract interpretation, Lipschitz bounds, and linear ReLU bounds.The cited examples include Dvijotham et al. (2018), Kolter & Wong (2017), and Raghunathan et al. (2018) for duality.Source: §2 · p. 2
  • Complete verifiers typically use MILP or SMT solvers, and this MILP verifier is two to three orders of magnitude faster than Reluplex on minimum adversarial distortion.Its improvements also allow verification of a network with over 100,000 units, several orders of magnitude larger than the largest MNIST classifier previously verified by a complete verifier.Source: §2 · p. 2
  • Complete verification can augment robust training by resolving inputs left uncertain by heuristic attacks and incomplete verifiers, enabling more accurate comparisons of training procedures.Robust training procedures typically minimize an estimate of worst-case loss because calculating the exact loss can be costly.Source: §2 · pp. 2–3

3 BACKGROUND AND NOTATION

The background defines the network notation and states when verification can be expressed as an MILP. Its scope includes piecewise-linear network layers and properties over bounded input domains.

3 BACKGROUND AND NOTATION

  • A neural network is denoted f(·; θ): R^m → R^n, with fixed weights θ; a classifier has one output neuron per target class.Source: §3 · p. 3
  • Verification asks whether an output property holds for every input in a bounded domain, and MILP expression requires linear properties over polyhedra whose union forms that domain.Source: §3 · p. 3
  • The network must be composed of piecewise-linear layers, including linear transformations and piecewise-linear functions such as ReLU and maximum pooling.Convolutions, average pooling, residual shortcut connections, and evaluation-time batch normalization and dropout are included as linear transformations.Source: §3 · p. 3

4 FORMULATING ROBUSTNESS EVALUATION OF CLASSIFIERS AS AN MILP

The section formulates robustness queries for piecewise-linear classifiers as MILP feasibility or optimization problems. It then develops tight formulations for ReLU and maximum functions and progressively tightens bounds to improve tractability.

4 FORMULATING ROBUSTNESS EVALUATION OF CLASSIFIERS AS AN MILP

  • Robustness to bounded perturbations is tested by asking whether any valid perturbed input changes the predicted label; robustness holds when the corresponding adversarial-query problem is infeasible.The perturbation set must intersect the valid-input domain, and an adversarial example satisfies the query constraints.Source: §4 · p. 3
  • Minimum adversarial distortion is formulated as an optimization over perturbations that change the predicted label, with the chosen distance metric as the objective.The formulation can target labels in a specified set, and common l1, l2, and l∞ objectives require no additional integer variables.Source: §4 · pp. 3–4

4.1 FORMULATING PIECEWISE-LINEAR FUNCTIONS IN THE MILP FRAMEWORK

  • Tight ReLU and maximum-function formulations are central to solver performance, using binary indicators to represent the piecewise-linear choices.ReLUs with bounds wholly on one side of zero are stably active or inactive; maximum constraints can discard inputs whose upper bounds cannot reach the largest lower bound.Source: §4.1 · p. 4

4.2 PROGRESSIVE BOUNDS TIGHTENING

  • Tighter bounds strengthen the MILP and can avoid binary variables for stable ReLUs, while loose bounds propagate downstream and weaken later bounds.The procedure balances build time for tighter bounds against solve time for the main MILP.Source: §4.2 · p. 4
  • The implementation uses interval arithmetic and linear programming to determine bounds, with linear programming slower but tighter.The two procedures differ in computational cost and bound tightness.Source: §4.2 · p. 4
  • Progressive bounds tightening starts with fast, coarse bounds and refines them only when tighter bounds could improve the formulation.For ReLUs, bounds proving a stable phase permit early termination.Source: §4.2 · pp. 4–5
  • Progressive tightening can incorporate additional bound procedures between interval arithmetic and linear programming, potentially reducing build times.The authors note that such procedures are not part of the stated IA-and-LP combination.Source: §4.2 · pp. 4–5

5 EXPERIMENTS

Experiments evaluate the MILP verifier on MNIST and CIFAR-10 classifiers, including ablations, comparisons with other verifiers, and tests of verification-time determinants. The verifier improves adversarial-error bounds across tested networks, and its solve time tracks unresolved ReLUs and labels more closely than total ReLU count.

5 EXPERIMENTS

  • Experiments use MNIST and CIFAR-10 feed-forward classifiers with standard or robust training, and generally report a timeout when a sample takes over 1200 seconds.The evaluated architectures include MLPs, convolutional networks, and a ResNet.Source: §5 · p. 5

5.1.1 COMPARISONS TO OTHER MILP-BASED COMPLETE VERIFIERS

  • Table 1 reports verifier ablations evaluating the adversarial accuracy of MNIST classifier LPd-CNNA against perturbations with l∞ norm bound ϵ = 0.1, with one optimization removed per test.Build time is the time used to determine bounds; solve time is the time used to solve the main MILP after bounds are determined.Source: Table 1 · p. 6
  • Ablations indicate that each of the three optimizations is critical; the authors expect runtimes several orders faster without asymmetric bounds, and at least an order faster than Fischetti & Jo (2018).The three optimizations are progressive tightening, use of the restricted input domain, and asymmetric ReLU bounds.Source: §5.1.1 · pp. 5–6

5.1.2 COMPARISONS TO OTHER COMPLETE AND INCOMPLETE VERIFIERS

  • On the l∞ norm, verification is two to three orders of magnitude faster than Reluplex for minimum targeted adversarial distortion on MNIST samples.Figure 1 reports average per-sample times; Reluplex results were available only for the l∞ norm.Source: Figure 1 · p. 6, §5.1.2 · p. 6
  • For incomplete verifiers, the best certified lower bound under the l∞ norm is less than half the true minimum distortion, and the gap grows for deeper networks.Figure 2 reports means over 100 MNIST samples; the authors note that a true distortion of 0.1 would correspond to verification only to 0.05.Source: §5.1.2 · p. 7, Figure 2 · p. 7

5.2 DETERMINING ADVERSARIAL ACCURACY OF MNIST AND CIFAR-10 CLASSIFIERS

  • For every tested network, the verifier improves both the lower bound on adversarial error over PGD and the upper bound over the previous state of the art.For LPd-RES, which has 107,496 units, the solver reaches its time limit for only 0.31% of samples.Source: §5.2 · p. 7, Table 2 · p. 8

5.2.1 OBSERVATIONS ON DETERMINANTS OF VERIFICATION TIME

  • Verification time correlates more strongly with the number of ReLUs not provably stable and labels not eliminable than with total ReLU count.Table 3 reports these relationships for MNIST at ϵ = 0.1; LPd-CNNA and Adv-CNNA have identical architectures, yet Adv-CNNA takes two orders of magnitude longer.Source: Table 3 · p. 8, §5.2.1 · p. 8

6 DISCUSSION

The discussion identifies the verifier’s scope and the conditions under which it can handle new perturbation classes. The accompanying methods formulate ReLU and maximum operations and tighten variable bounds through procedures with different cost–tightness trade-offs.

6 DISCUSSION

  • New perturbation classes are supported when the set of perturbed images is a union of polytopes, while defining perceptually similar perturbations remains an open direction.The paper focuses on evaluating networks against the perturbation classes they were designed to resist.Source: §6 · p. 9

A.1 FORMULATING RELU IN AN MILP MODEL

  • The formulation for rectified linearities is sharp when no further information about x is available; if x is affine in z, it is no longer sharp, but bounds on z can improve the formulation.Source: §A.1 · p. 12

A.2 FORMULATING THE MAXIMUM FUNCTION IN AN MILP MODEL

  • The maximum formulation uses binary indicators to select a maximizing input, with exactly one indicator set to 1.When ai = 1, the constraints imply y = xi; when ai = 0, the constraints involving xi are nonbinding.Source: §A.2 · p. 12

A.3.1 l1; A.3.2 l∞; A.3.3 l2

  • For l1 and l∞ distortions, auxiliary variables bound elementwise absolute differences and the maximum absolute difference, respectively.For l2 distortion, the objective is quadratic and requires an MIQP solver, but no auxiliary variables are needed.Source: §A.3.1 · p. 12, §A.3.2 · p. 13, §A.3.3 · p. 13

B DETERMINING TIGHT BOUNDS ON DECISION VARIABLES

  • Tight bounds strengthen the MILP and can eliminate binary variables for stable ReLUs; loose bounds can propagate to later layers.Bounds are computed on a feed-forward computation graph using subgraphs and bounds on their source variables.Source: B DETERMINING TIGHT BOUNDS ON DECISION… · p. 13

B.1 FULL

  • FULL finds optimal bounds if solves reach optimality, but deeper-layer solves can take exponential time in the number of binary variables.Early termination still yields a valid, potentially loose bound from the best certified bound found so far.Source: §B.1 · p. 14

B.2 LINEAR PROGRAMMING (LP); B.3 INTERVAL ARITHMETIC (IA)

  • LP relaxes integer constraints for more efficient bounds, while IA uses only the previous layer’s variable bounds and can become overly conservative in deeper layers.LP is described as a middle ground between FULL’s optimality and IA’s performance; IA uses matrix operations for these applications.Source: §B.2 · p. 14, §B.3 · p. 14

C PROGRESSIVE BOUNDS TIGHTENING

  • Progressive bound tightening processes procedures in increasing computational complexity and removes candidates whose upper bounds fall below the best known lower bound.For maximum constraints, GETBOUNDSFORMAX returns the remaining possible maximizers along with upper and lower bounds.Source: C PROGRESSIVE BOUNDS TIGHTENING · pp. 14–15

D ADDITIONAL EXPERIMENTAL DETAILS

The experimental setup covers classifiers across MNIST and CIFAR-10, including robustly trained and non-robust MNIST networks. Experiments use a specified MILP software stack and shared virtual-machine hardware.

D.1 NETWORKS USED

  • The evaluated networks include MNIST classifiers not designed for robustness and classifiers designed for robustness to perturbations with l∞ norm bounds ε = 0.1, 0.2, 0.3, and 0.4.Source: §D.1 · p. 15
  • The listed robust MNIST models include classifiers from Kolter & Wong (2017) and Wong et al. (2018), plus models trained with PGD adversarial examples.The PGD configurations include ε = 0.1 with 8 steps for Adv-CNNA and ε = 0.15 with 200 steps for Adv-MLP-2×[200].Source: §D.1 · p. 15

D.2 COMPUTATIONAL ENVIRONMENT

  • The MILPs were built in Julia with JuMP and solved using Gurobi 7.5.2 on a shared KVM virtual machine with 8 virtual CPUs and 8GB RAM.The reported processors were Intel Xeon E5-2630 v4 @ 2.20GHz.Source: §D.2 · p. 16

E PERFORMANCE OF VERIFIER WITH OTHER MILP SOLVERS

The solver comparison finds Gurobi performs best, while the verifier also improves on existing bounds with the open-source Cbc solver. GLPK performs worse and times out on almost 4% of samples.

E PERFORMANCE OF VERIFIER WITH OTHER MILP SOLVERS

  • With Cbc, the verifier outperforms the PGD lower bound and the state-of-the-art upper bound on the MNIST LPd-CNNA network at ε = 0.1.The table caption reports that Gurobi gives the best verifier performance; the prose notes that Cbc times out on some samples.Source: Table 4 · p. 16, E PERFORMANCE OF VERIFIER WITH OTHER… · p. 16
  • The comparison evaluates different MILP solvers on the MNIST LPd-CNNA network with ε = 0.1.The caption identifies Gurobi as best overall and reports that Cbc still beats the PGD lower bound and the state-of-the-art upper bound.Source: Table 4 · p. 16
  • Almost 4% of samples time out with GLPK, whose performance is significantly worse than with Gurobi.Verifier performance depends on the underlying MILP solver.Source: E PERFORMANCE OF VERIFIER WITH OTHER… · p. 16

F.1 NODES EXPLORED

The appendix reports solver search-tree statistics and additional measures associated with verification time. These include node counts, eliminated labels, and provably stable ReLUs for MNIST and CIFAR-10 classifiers.

F.1 NODES EXPLORED

  • For LPd-CNNA at ϵ = 0.1, presolve bounds suffice to prove robustness or find an adversarial example without branching for over 95% of samples.The appendix presents node-exploration statistics as a supplement to the main verification results.Source: §F.1 · p. 16

F.2 DETERMINANTS OF VERIFICATION TIME

  • Table 5 reports nodes explored when determining adversarial accuracy for MNIST and CIFAR-10 classifiers under l∞-bounded perturbations, with one linear program solved per search-tree node.The appendix introduces these statistics as additional information on verification-time determinants for networks omitted from Table 3.Source: §F.2 · p. 16, Table 5 · p. 17
  • Table 6 reports the numbers of labels eliminated and ReLUs proved stable during adversarial-accuracy verification for MNIST and CIFAR-10 classifiers under l∞-bounded perturbations.These are additional measures of verification-time determinants for networks omitted from Table 3.Source: §F.2 · p. 16, Table 6 · p. 17

G WHICH ADVERSARIAL EXAMPLES ARE MISSED BY PGD?

The section examines how PGD attack success relates to minimum adversarial distortion for LPd-CNNA networks trained against different perturbation sizes. PGD success declines as distortion approaches the training bound, and the authors note that this can make bounded attacks miss vulnerabilities.

Estimating PGD success

  • The plotted relationship uses a coarser estimate based on one randomly initialized PGD run per sample, rather than multiple starts.Multiple random starts would be needed for the best possible empirical estimate of per-sample PGD success.Source: G WHICH ADVERSARIAL EXAMPLES ARE… · p. 18

PGD success and minimum adversarial distortion

  • PGD is very successful when minimum adversarial distortion is small, but its success rate declines significantly across networks as distortion approaches ϵ.Figure 3 bins samples by minimum distortion and shows attack success within each bin.Source: Figure 3 · p. 18, G WHICH ADVERSARIAL EXAMPLES ARE… · p. 19

Comparing training bounds

  • When minimum distortion is much smaller than both networks’ training bounds, PGD more consistently succeeds against the network trained for the smaller bound.The comparison applies when ˆδ ≪ ϵa and ϵa < ϵb.Source: G WHICH ADVERSARIAL EXAMPLES ARE… · p. 19

Implications for PGD evaluation

  • The authors suggest that training networks to concentrate adversarial examples near ϵ could make them appear robust to bounded PGD attacks while remaining vulnerable within that bound.This suggestion follows the sharp decline in PGD success as minimum distortion approaches ϵ.Source: G WHICH ADVERSARIAL EXAMPLES ARE… · p. 19

H SPARSIFICATION AND VERIFIABILITY

The section tests whether sparsifying SDPd-MLPA improves verifiability by zeroing small weights. Solve time and timeouts improve, but sparsification also affects test error and the certified adversarial-error upper bound.

Sparsification method

  • The heuristic zeros the smallest-magnitude weights in each fully connected layer and rescales the remaining weights to preserve the kernel’s l1 norm.The network has two layers: one hidden layer and one output layer.Source: H SPARSIFICATION AND VERIFIABILITY · p. 19

Verification results

  • Comparing the original and most-sparsified network, mean verification time and the fraction timed out each improve by an order of magnitude.The table summarizes verification of sparse SDPd-MLPA variants, with the original network in the first row.Source: H SPARSIFICATION AND VERIFIABILITY · p. 19, Table 7 · p. 19

Accuracy and certified error

  • Test error rises with sparsification but its impact is not significant until f1 exceeds 0.8; the certified adversarial-error upper bound improves through f1 = 0.8, then worsens at f1 = 0.9.The authors suggest the worsening at f1 = 0.9 may reflect a significant increase in true adversarial error.Source: H SPARSIFICATION AND VERIFIABILITY · p. 19, Table 7 · p. 19

Implications

  • Starting from a robust network, simple sparsification can yield a lower certified adversarial-error upper bound than the best bound for the original network.The authors suggest a more principled approach could improve verifiability without compromising true adversarial error as much.Source: H SPARSIFICATION AND VERIFIABILITY · p. 20

I ROBUST TRAINING AND RELU STABILITY

The section relates robust training to provable ReLU stability under bounded perturbations. Stability becomes harder to prove as the perturbation bound grows, with LPd-CNNA showing a particularly sharp change near ϵ = 0.1.

Robust training and stability

  • Across the robust training procedures considered, a significant fraction of ReLUs are provably stable under bounded l∞ perturbations, with units always active or always inactive over the input domain.The authors believe the need for robustness drives more ReLUs to be provably stable.Source: I ROBUST TRAINING AND RELU STABILITY · p. 20

Varying the perturbation bound

  • The analysis varies the perturbation-domain size to examine how robust networks retain global expressiveness while many ReLUs remain provably stable.The section frames this as a study of how the number of provably stable ReLUs changes with the perturbation bound.Source: I ROBUST TRAINING AND RELU STABILITY · p. 20
  • As the maximum allowed perturbation grows, more ReLUs cannot be proven stable; LPd-CNNA shows a sharp increase beyond 0.102, unlike the other two networks.The comparison concerns networks trained to be robust at ϵ = 0.1.Source: I ROBUST TRAINING AND RELU STABILITY · p. 20, Figure 4 · p. 21

Related papers

Loading 1711.07356v3…