While neural networks have achieved high accuracy on standard image classification benchmarks, their accuracy drops to nearly zero in the presence of small adversarial perturbations to test inputs. Defenses based on regularization and adversarial training have been proposed, but often followed by new, stronger attacks that defeat these defenses. Can we somehow end this arms race? In this work, we study this problem for neural networks with one hidden layer. We first propose a method based on a semidefinite relaxation that outputs a certificate that for a given network and test input, no attack can force the error to exceed a certain value. Second, as this certificate is differentiable, we jointly optimize it with the network parameters, providing an adaptive regularizer that encourages robustness against all attacks. On MNIST, our approach produces a network and a certificate that no that perturbs each pixel by at most $\epsilon = 0.1$ can cause more than $35\%$ test error.
 Despite the impressive (and sometimes even superhuman) accuracies of machine learning on diverse tasks such as object recognition BID18 , speech recognition BID55 , and playing Go BID46 , classifiers still fail catastrophically in the presence of small imperceptible but adversarial perturbations BID50 BID17 BID25 . In addition to being an intriguing phenonemon, the existence of such "adversarial examples" exposes a serious vulnerability in current ML systems BID13 BID45 . While formally defining an "imperceptible" perturbation is difficult, a commonly-used proxy is perturbations that are bounded in ∞ -norm BID17 BID31 BID53 ; we focus on this attack model in this paper, as even for this proxy it is not known how to construct high-performing image classifiers that are robust to perturbations.While a proposed defense (classifier) is often empirically shown to be successful against the set of attacks known at the time, new stronger attacks are subsequently discovered that render the defense useless. For example, defensive distillation BID42 and adversarial training against the Fast Gradient Sign Method BID17 were two defenses that were later shown to be ineffective against stronger attacks BID53 . In order to break this arms race between attackers and defenders, we need to come up with defenses that are successful against all attacks within a certain class.However, even computing the worst-case error for a given network against all adversarial perturbations in an ∞ -ball is computationally intractable. One common approximation is to replace the worst-case loss with the loss from a given heuristic attack strategy, such as the Fast Gradient Sign Method BID17 or more powerful iterative methods BID7 BID31 . Adversarial training minimizes the loss with respect to these heuristics. However, this essentially minimizes a lower bound on the worst-case loss, which is problematic since points where the bound is loose have disproportionately lower objective values, which could lure and mislead an optimizer. Indeed, while adversarial training often provides robustness against a specific attack, it often fails to generalize to new attacks, as described above. Another approach is to compute the worst-case perturbation exactly using discrete optimization BID21 (b) Figure 1 : Illustration of the margin function f (x) for a simple two-layer network. (a) Contours of f (x) in an ∞ ball around x. Sharp curvature near x renders a linear approximation highly inaccurate, and f (A fgsm (x)) obtained by maximising this approximation is much smaller than f (A opt (x)).(b ) Vector field for ∇f (x) with length of arrows proportional to ∇f (x) 1 . In our approach, we bound f (A opt (x)) by bounding the maximum of ∇f (x) 1 over the neighborhood (green arrow).In general, this could be very different from ∇f (x) 1 at just the point x (red arrow).et al., 2017) . Currently , these approaches can take up to several hours or longer to compute the loss for a single example even for small networks with a few hundred hidden units. Training a network would require performing this computation in the inner loop, which is infeasible.In this paper, we introduce an approach that avoids both the inaccuracy of lower bounds and the intractability of exact computation, by computing an upper bound on the worst-case loss for neural networks with one hidden layer, based on a semidefinite relaxation that can be computed efficiently. This upper bound serves as a certificate of robustness against all attacks for a given network and input. Minimizing an upper bound is safer than minimizing a lower bound, because points where the bound is loose have disproportionately higher objective values, which the optimizer will tend to avoid. Furthermore , our certificate of robustness, by virtue of being differentiable, is trainable-it can be optimized at training time jointly with the network, acting as a regularizer that encourages robustness against all ∞ attacks.In summary, we are the first (along with the concurrent work of BID24 ) to demonstrate a certifiable, trainable, and scalable method for defending against adversarial examples on two-layer networks. We train a network on MNIST whose test error on clean data is 4.2%, and which comes with a certificate that no attack can misclassify more than 35% of the test examples using ∞ perturbations of size = 0.1.Notation. For a vector z ∈ R n , we use z i to denote the i th coordinate of z. For a matrix Z ∈ R m×n , Z i denotes the i th row. For any activation function σ : R → R (e.g., sigmoid, ReLU) and a vector z ∈ R n , σ(z) is a vector in R n with σ(z) i = σ(z i ) (non-linearity is applied element-wise). We use B (z) to denote the ∞ ball of radius around z ∈ R d : B (z) = {z | |z i − z i | ≤ for i = 1, 2, . . . d}. Finally, we denote the vector of all zeros by 0 and the vector of all ones by 1. In this work, we proposed a method for producing certificates of robustness for neural networks, and for training against these certificates to obtain networks that are provably robust against adversaries.Related work. In parallel and independent work, BID24 also provide provably robust networks against ∞ perturbations by using convex relaxations. While our approach uses a single semidefinite program to compute an upper bound on the adversarial loss, Kolter & Wong (2017) use separate linear programs for every data point, and apply their method to networks of depth up to four. In theory, neither bound is strictly tighter than the other, and our experiments TAB2 suggest that the two bounds are complementary. Combining the approaches seems to be a promising future direction. BID21 and the follow-up BID10 also provide certificates of robustness for neural networks against ∞ perturbations. That work uses SMT solvers, which are a tool from the formal verification literature. The SMT solver can answer the binary question "Is there an adversarial example within distance of the input x?", and is correct whenever it terminates. The main drawback of SMT and similar formal verification methods is that they are slow-they have worst-case exponential-time scaling in the size of the network; moreover, to use them during training would require a separate search for each gradient step. BID20 use SMT solvers and are able to analyze state-of-the-art networks on MNIST, but they make various approximations such that their numbers are not true upper bounds. BID2 provide tractable certificates but require to be small enough to ensure that the entire ∞ ball around an input lies within the same linear region. For the networks and values of that we consider in our paper, we found that this condition did not hold. Recently, Hein & Andriushchenko (2017) proposed a bound for guaranteeing robustness to p -norm perturbations, based on the maximum p p−1 -norm of the gradient in the -ball around the inputs. BID19 show how to efficiently compute this bound for p = 2, as opposed to our work which focuses on ∞ and requires different techniques to achieve scalability. BID31 perform adversarial training against PGD on the MNIST and CIFAR-10 datasets, obtaining networks that they suggest are "secure against first-order adversaries". However, this is based on an empirical observation that PGD is nearly-optimal among gradient-based attacks, and does not correspond to any formal robustness guarantee.Finally, the notion of a certificate appears in the theory of convex optimization, but means something different in that context; specifically, it corresponds to a proof that a point is near the optimum of a convex function, whereas here our certificates provide upper bounds on non-convex functions. Additionally, while robust optimization BID3 provides a tool for optimizing objectives with robustness constraints, applying it directly would involve the same intractable optimization for A opt that we deal with here.Other approaches to verification. While they have not been explored in the context of neural networks, there are approaches in the control theory literature for verifying robustness of dynamical systems, based on Lyapunov functions (Lyapunov, 1892; BID29 . We can think of the activations in a neural network as the evolution of a time-varying dynamical system, and attempt to prove stability around a trajectory of this system BID51 BID52 . Such methods typically use sum-of-squares verification BID38 BID43 and are restricted to relatively low-dimensional dynamical systems, but could plausibly scale to larger settings. Another approach is to construct families of networks that are provably robust a priori, which would remove the need to verify robustness of the learned model; to our knowledge this has not been done for any expressive model families.Adversarial examples and secure ML. There has been a great deal of recent work on the security of ML systems; we provide only a sampling here, and refer the reader to BID0 , BID4 , BID41 , and BID14 for some recent surveys.Adversarial examples for neural networks were first discovered by BID50 , and since then a number of attacks and defenses have been proposed. We have already discussed gradientbased methods as well as defenses based on adversarial training. There are also other attacks based on, e.g., saliency maps BID40 , KL divergence BID33 , and elastic net optimization BID11 ; many of these attacks are collated in the cleverhans repository . For defense, rather than making networks robust to adversaries, some work has focused on simply detecting adversarial examples. However, BID7 recently showed that essentially all known detection methods can be subverted by strong attacks.As explained in BID0 , there are a number of different attack models beyond the testtime attacks considered here, based on different attacker goals and capabilities. For instance, one can consider data poisoning attacks, where an attacker modifies the training set in an effort to affect test-time performance. BID35 , BID26 , and BID5 have demonstrated poisoning attacks against real-world systems.Other types of certificates. Certificates of performance for machine learning systems are desirable in a number of settings. This includes verifying safety properties of air traffic control systems BID21 and self-driving cars (O' Kelly et al., 2016; , as well as security applications such as robustness to training time attacks BID48 . More broadly, certificates of performance are likely necessary for deploying machine learning systems in critical infrastructure such as internet packet routing BID54 BID47 . In robotics, certificates of stability are routinely used both for safety verification BID30 BID32 and controller synthesis BID1 BID51 .In traditional verification work, Rice's theorem BID44 ) is a strong impossibility result essentially stating that most properties of most programs are undecidable. Similarly, we should expect that verifying robustness for arbitrary neural networks is hard. However, the results in this work suggest that it is possible to learn neural networks that are amenable to verification, in the same way that it is possible to write programs that can be formally verified. Optimistically, given expressive enough certification methods and model families, as well as strong enough specifications of robustness, one could even hope to train vector representations of natural images with strong robustness properties, thus finally closing the chapter on adversarial vulnerabilities in the visual domain.
We demonstrate a certifiable, trainable, and scalable method for defending against adversarial examples. Proposes a new defense against security attacks on neural networks with the atack model that outputs a security certificate on the algorithm. Derives an upper bound on adversarial perturbation for neural networks with one hidden layer