# boosting_robustness_certification_of_neural_networks__24c79e5f.pdf

Published as a conference paper at ICLR 2019

BOOSTING ROBUSTNESS CERTIFICATION OF NEURAL NETWORKS

Gagandeep Singh, Timon Gehr, Markus P uschel, Martin Vechev Department of Computer Science ETH Zurich, Switzerland {gsingh,timon.gehr,pueschel,martin.vechev}@inf.ethz.ch

We present a novel approach for the certiﬁcation of neural networks against adversarial perturbations which combines scalable overapproximation methods with precise (mixed integer) linear programming. This results in signiﬁcantly better precision than state-of-the-art veriﬁers on challenging feedforward and convolutional neural networks with piecewise linear activation functions.

1 INTRODUCTION

Neural networks are increasingly applied in critical domains such as autonomous driving (Bojarski et al., 2016), medical diagnosis (Amato et al., 2013), and speech recognition (Hinton et al., 2012). However, it has been shown by Goodfellow et al. (2014) that neural networks can be vulnerable against adversarial attacks, i.e., imperceptible input perturbations cause neural networks to misclassify. To address this challenge and prove that a network is free of adversarial examples (usually, in a region around a given input), recent work has started investigating the use of certiﬁcation techniques. Current veriﬁers can be broadly classiﬁed as either complete or incomplete.

Complete veriﬁers are exact, i.e., if the veriﬁer fails to certify a network then the network is nonrobust (and vice-versa). Existing complete veriﬁers are based on Mixed Integer Linear Programming (MILP) (Lomuscio & Maganti, 2017; Fischetti & Jo, 2018; Dutta et al., 2018; Cheng et al., 2017) or SMT solvers (Katz et al., 2017; Ehlers, 2017). Although precise, these can only handle networks with a small number of layers and neurons. To scale, incomplete veriﬁers usually employ overapproximation methods and hence they are sound but may fail to prove robustness even if it holds. Incomplete veriﬁers use methods such as duality (Dvijotham et al., 2018), abstract interpretation (Gehr et al., 2018; Singh et al., 2018; 2019), linear approximations (Weng et al., 2018; Wong & Kolter, 2018; Zhang et al., 2018), semideﬁnite relaxations (Raghunathan et al., 2018), combination of linear and non-linear approximation (Xiang et al., 2017), or search space discretization (Huang et al., 2017). Incomplete veriﬁers are more scalable than complete ones, but can suffer from precision loss for deeper networks. In principle, incomplete veriﬁers can be made asymptotically complete by iteratively reﬁning the input space (Wang et al., 2018a) or the neurons (Wang et al., 2018b); however, in the worst case, this may eliminate any scalability gains and thus defeat the purpose of using overapproximation in the ﬁrst place.

This work: boosting complete and incomplete veriﬁers. A key challenge then is to design a veriﬁer which improves the precision of incomplete methods and the scalability of complete ones. In this work, we make a step towards addressing this challenge based on two key ideas: (i) a combination of state-of-the-art overapproximation techniques used by incomplete methods, including LP relaxations, together with MILP solvers, often employed in complete veriﬁers; (ii) a novel heuristic, which points to neurons whose approximated bounds should be reﬁned. We implemented these ideas in a system called Reﬁne Zono, and showed that is is faster than state-of-the-art complete veriﬁers on small networks while improving precision of existing incomplete veriﬁers on larger networks.

The recent works of (Wang et al., 2018b) and Tjeng et al. (2019) have also explored the combination of linear programming with overapproximation. However, both use simpler and coarser overapproximations than ours. Our evaluation shows that Reﬁne Zono is faster than both for complete veriﬁcation. For example, Reﬁne Zono is faster than the work of Tjeng et al. (2019) for the complete

Published as a conference paper at ICLR 2019

max(0, x12)

max(0, x13)

+0.5 η1 l1 = 0

+0.5 η2 l2 = 0

+0.5 η1 +0.5 η2 l3 = 0

ˆ x4 = 0.5 η1 0.5 η2 l4 = 1

+0.5 η1 +0.5 η2 l5 = 0

ˆ x6 = 0.25

+0.25 η1 0.25 η2 +0.25 η3 l6 = 0.5

ˆ x7 = 1.75

+0.25 η1 +0.75 η2 0.25 η3 l7 = 1

ˆ x8 = 0.25

+0.25 η1 +0.75 η2 0.25 η3 l8 = 1

ˆ x9 = 1.75

+0.25 η1 +0.75 η2 0.25 η3 l9 = 1

ˆ x10 = 0.125

+0.125 η1 +0.375 η2 0.125 η3 +0.25 η4 l10 = 0.5

ˆ x11 = 4.875

+0.625 η1 +1.875 η2 0.625 η3 +0.25 η4 l11 = 3.25

ˆ x12 = 2.625

+0.125 η1 +0.375 η2 0.125 η3 0.25 η4 l12 = 2

ˆ x13 = 4.875

+0.625 η1 +1.875 η2 0.625 η3 +0.25 η4 l13 = 3.25

ˆ x14 = 2.625

+0.125 η1 +0.375 η2 0.125 η3 0.25 η4 l14 = 2

Figure 1: Robustness analysis of a toy example neural network using our method. Here, approximation results computed with Deep Z (blue box) are reﬁned using MILP whereas those in green are reﬁned using LP.

veriﬁcation of a 3 50 network, while for the larger 9 200 network their method does not ﬁnish within multiple days on images which Reﬁne Zono veriﬁes in 14 minutes.

Main contributions. Our main contributions are:

A reﬁnement-based approach for certifying neural network robustness that combines the strengths of fast overapproximation methods with MILP solvers and LP relaxations.

A novel heuristic for selecting neurons whose bounds should be further reﬁned.

A complete end-to-end implementation of our approach in a system called Reﬁne Zono, publicly available at https://github.com/eth-sri/eran.

An evaluation, showing that Reﬁne Zono is more precise than existing state-of-the-art incomplete veriﬁers on larger networks and faster (while being complete) than complete veriﬁers on smaller networks.

We now demonstrate how our method improves the precision of a state-of-the-art incomplete veriﬁer. The main objective here is to provide an intuitive understanding of our approach; full formal details are provided in the next section.

Consider the simple fully connected feedforward neural network with Re LU activations shown in Fig. 1. There are two inputs to the network, both in the range [0, 1]. The network consists of an input layer, two hidden layers, and one output layer. Each layer consist of two neurons each. For our explanation, we separate each neuron into two parts: one represents the output of the afﬁne transformation while the other captures the output of the Re LU activation. The weights for the afﬁne transformation are represented by weights on the edges. The bias for each node is shown above or below it. Our goal is to verify that for any input in [0, 1] [0, 1], the output at neuron x13 is greater than the output at x14.

We now demonstrate how our veriﬁer operates on this network. We assume that the analysis results after the second afﬁne transformation are reﬁned using a MILP formulation of the network whereas the results after the third afﬁne transformation are reﬁned by an LP formulation of the network. In

Published as a conference paper at ICLR 2019

lx l x ux u x

Figure 2: Re LU transformers, computing an afﬁne form. Here, lx, ux are the original bounds, whereas l x, u x are the reﬁned bounds. The slope of the two non-vertical parallel blue lines is λ = ux/(ux lx) and the slope of the two non-vertical parallel green lines is λ = u x/(u x l x). The blue parallelogram is used to compute an afﬁne form in Deep Z, whereas the green parallelogram is used to compute the output of the reﬁned Re LU transformer considered in this work.

the next section, we will explain our heuristic for selecting MILP or LP formulations of different neurons in the network. Our analysis leverages the Zonotope domain (Ghorbal et al., 2009) together with the abstract Zonotope transformers specialized to neural network activations as used in Deep Z (Singh et al., 2018), a state of the art veriﬁer for neural network robustness. The Zonotope domain associates an afﬁne form ˆx with each neuron x in the network:

Here, c0, ci R are real coefﬁcients and ηi [si, ti] [ 1, 1] are the noise symbols, which are shared between the afﬁne forms for different neurons. This sharing makes the domain relational and thus more precise than non-relational domains such as Interval (Box). An abstract element in our analysis is an intersection between a Zonotope (given as a list of afﬁne forms) and a bounding box. Thus, for each neuron x, we keep the afﬁne form ˆx and an interval [lx, ux].

First layer. Our analysis starts by setting

ˆx1 = 0.5 + 0.5 η1, l1 = 0, u1 = 1

and ˆx2 = 0.5 + 0.5 η2, l2 = 0, u2 = 1, representing the input [0, 1] at x1 and [0, 1] at x2 in our domain, respectively. Next, an afﬁne transformation is applied on the inputs resulting in the output

ˆx3 = ˆx1 + ˆx2 = 1 + 0.5 η1 + 0.5 η2, l3 = 0, u3 = 2

and ˆx4 = ˆx1 ˆx2 = 0.5 η1 0.5 η2, l4 = 1, u4 = 1. Note that the Zonotope afﬁne transformer is exact for this transformation. Next, the Zonotope Re LU transformer is applied. We note that as l3 0, the neuron x3 provably takes only non-negative values. Thus, the Re LU Zonotope transformer outputs ˆx5 = ˆx3 and we set l5 = l3, u5 = l3 which is the exact result. For x4, l4 < 0 and u4 > 0 and thus neuron x4 can take both positive and negative values. The corresponding output does not have a closed afﬁne form and hence the approximation in blue shown in Fig. 2 is used to compute the result. This approximation minimizes the area of the result in the input-output plane and introduces a new noise symbol η3 [ 1, 1]. The result is

ˆx6 = 0.25 + 0.25 η1 0.25 η2 + 0.25 η3, l6 = 0.5, u6 = 1.

Note that the Zonotope approximation for x6 from Fig. 2 permits negative values whereas x6 can only take non-negative values in the concrete. This overapproximation typically accumulates as the analysis progresses deeper into the network, resulting in overall imprecision and failure to prove properties that actually hold.

Published as a conference paper at ICLR 2019

MILP-based reﬁnement at second layer. Next, the analysis handles the second afﬁne transformation and computes

ˆx7 = ˆx5 ˆx6 + 1 = 1.75 + 0.25 η1 + 0.75 η2 0.25 η3, l7 = 0.5, u7 = 3

ˆx8 = ˆx5 ˆx6 1 = 0.25 + 0.25 η1 + 0.75 η2 0.25 η3, l8 = 1.5, u8 = 1.

Here, x7 is provably positive, whereas x8 can take both positive and negative values. Due to the approximation for x6, the bounds for x7 and x8 are imprecise. Note that the Deep Z Re LU transformer for x8 applied next will introduce more imprecision and although the Re LU transformer for provably positive inputs such as x7 does not lose precision with respect to the input, it still propagates the imprecision in the computation of the abstract values for x7.

Thus, to reduce precision loss, in our method we reﬁne the bounds for both x7 and x8 by formulating the network up to (and including) the second afﬁne transformation as a MILP instance based on a formulation from Tjeng et al. (2019) and compute bounds for x7 and x8, respectively. The MILP solver improves the lower bounds for x7 and x8 to 1 and 1, respectively, which then updates the corresponding lower bounds in our abstraction, i.e., l7 = 1 and l8 = 1.

Next, the Re LU transformer is applied. Since x7 is provably positive, we get ˆx9 = ˆx7, l9 = l7, and u9 = u7. We note that x8 can take both positive and negative values and is therefore approximated. However, the Re LU transformer now uses the reﬁned bounds instead of the original bounds and thus the approximation shown in green from Fig. 2 is used. This approximation has smaller area in the input-output plane compared to the blue one and thus reduces the approximation error. The result is

ˆx10 = 0.125 + 0.125 η1 + 0.375 η2 0.125 η3 + 0.25 η4, l8 = 0.5, u8 = 1.

LP-based reﬁnement at ﬁnal layer. Continuing with the analysis, we now process the ﬁnal afﬁne transformation, which yields

ˆx11 = 4.875 + 0.625 η1 + 1.875 η2 0.625 η3 + 0.25 η4, l11 = 1.75, u11 = 8.25

ˆx12 = 2.625 + 0.125 η1 + 0.375 η2 0.125 η3 0.25 η4, l12 = 1.75, u12 = 3.5.

Due to the approximations from previous layers, the computed values can be imprecise. We note that, as the analysis proceeds deeper into the network, reﬁning bounds with MILP becomes expensive. Thus, we reﬁne the bounds by encoding the network up to (and including) the third afﬁne transformation using the faster LP relaxation of the network based on Ehlers (2017) and compute the bounds for x11 and x12, respectively. This leads to better results for l11 = 3.25, l12 = 2, and u12 = 3. As both x11 and x12 are provably positive, the subsequent Re LU transformations set ˆx13 = ˆx11, l13 = l11, u13 = u11 and ˆx14 = ˆx12, l14 = l12, u14 = u12.

Proving robustness. Since the lower bound l13 for x13 is greater than the upper bound u14 for x14, our analysis can prove that the given neural network provides the same label for all inputs in [0, 1] [0, 1] and is thus robust. In contrast, Deep Z without our reﬁnement would compute

ˆx13 = 4.95 + 0.6 η1 + 1.8 η2 0.6 η3 + 0.3 η4, l13 = 1.65, u13 = 8.25

and ˆx14 = 2.55 + 0.15 η1 + 0.45 η2 0.15 η3 0.3 η4, l14 = 1.5, u14 = 3.6.

As a result, Deep Z fails to prove that x13 is greater than x14, and thus fails to prove robustness.

Generalization to other abstractions. We note that our reﬁnement-based approach is not restricted to the Zonotope domain. It can be extended for reﬁning the results computed by other abstractions such as Polyhedra (Singh et al., 2017) or the abstraction used in Deep Poly (Singh et al., 2019). For example, the Re LU transformer in Singh et al. (2019) also depends on the bounds of input neurons and thus it will beneﬁt from the precise bounds computed using our reﬁnement. Since Deep Poly often produces more precise results than Deep Z, we believe a combination of this work with Deep Poly will further improve veriﬁcation results.

Published as a conference paper at ICLR 2019

3 OUR APPROACH

We now describe our approach in more formal terms. As in the previous section, we will consider afﬁne transformations and Re LU activations as separate layers. As illustrated earlier, the key idea will be to combine abstract interpretation (Cousot & Cousot, 1977) with exact and inexact MILP formulations of the network, which are then solved, in order to compute more precise results for neuron bounds. We begin by describing the core ingredients of abstract interpretation.

Our approach requires an abstract domain An over n variables (i.e., some set whose elements can be encoded symbolically) such as Interval, Zonotope, the abstraction in Deep Poly, or Polyhedra. An abstract domain has a bottom element An as well as the following components:

A (potentially non-computable) concretization function γn : An P(Rn) that associates with each abstract element a An the set of concrete points from Rn that it abstracts. We have γn( ) = . An abstraction function αn : Bn An, where X γn(αn(X)) for all X Bn. We assume that αn(Q

i[li, ui]) is a computable function of l, u Rn. Here, Bn = S

i[li, ui] and Q

i[li, ui] = {x Rn | li xi ui}. (For many abstract domains, αn can be deﬁned on a larger domain Bn, but in this work, we only consider Interval input regions.) A bounding box function ιn : An Rn Rn, where γn(a) Q

i[li, ui] for (l, u) = ιn(a) for all a An. A meet operation a L for each a An and linear constraints L over n real variables, where {x γn(a) | L(x)} γn(a L).

An afﬁne abstract transformer T # x7 Ax+b : Am An for each transformation of the form (x 7 Ax + b): Rm Rn, where

{Ax + b | x γn(a)} γn(T # x7 Ax+b(a)) for all a Am.

A Re LU abstract transformer T # Re LU|Q i[li,ui] : An An, where

{Re LU(x) | x γn(a) Y

i [li, ui]} T # Re LU|Q i[li,ui](a)

for all abstract elements a An and for all lower and upper bounds l, u Rn on input activations of the Re LU operation.

Veriﬁcation via Abstract interpretation. As ﬁrst shown by Gehr et al. (2018), any such abstract domain induces a method for robustness certiﬁcation of neural networks with Re LU activations.

For example, assume that we want to certify that a given neural network f : Rm Rn considers class i more likely than class j for all inputs x with || x x|| ϵ for a given x and ϵ. We can ﬁrst use the abstraction function αm to compute a symbolic overapproximation of the set of possible inputs x, namely ain = αm({ x Rm | || x x|| ϵ}).

Given that the neural network can be written as a composition of afﬁne functions and Re LU layers, we can then propagate the abstract element ain through the corresponding abstract transformers to obtain a symbolic overapproximation aout of the concrete outputs of the neural network.

For example, if the neural network f(x) = A Re LU(Ax + b) + b has a single hidden layer with h hidden neurons, we ﬁrst compute a = T # x7 Ax+b(ain), which is a symbolic overapproximation of the input to the Re LU activation function. We then compute (l, u) = ιh(a ) to obtain opposite corners of a bounding box of all possible Re LU input activations, such that we can apply the Re LU abstract transformer: a = T # Re LU|Q i[li,ui](a ).

Finally, we apply the afﬁne abstract transformer again to obtain aout = T # x7 A x+b (a ). Using our assumptions, we can conclude that the set γn(aout) contains all output activations that f can possibly produce when given any of the inputs x. Therefore, if aout (xi xj) = , we have proved the property: for all x, the neural network considers class i more likely than class j.

Published as a conference paper at ICLR 2019

Incompleteness. While this approach is sound (i.e., whenever we prove the property, it actually holds), it is incomplete (i.e., we might not prove the property, even if it holds), because the abstract transformers produce a superset of the set of concrete outputs that the corresponding concrete executions produce. This can be quite imprecise for deep neural networks, because the overapproximations introduced in each layer accumulate.

Reﬁning the bounds. To combat spurious overapproximation, we use mixed integer linear programming (MILP) to compute reﬁned lower and upper bounds l , u after applying each afﬁne abstract transformer (except for the ﬁrst layer). We then reﬁne the abstract element using the meet operator of the underlying abstract domain and the linear constraints l i xi u i for all input activations i, i.e., we replace the current abstract element a by a = a (V

i l i xi u i), and continue analysis with the reﬁned abstract element.

Importantly, we obtain a more reﬁned abstract transformer for Re LU than the one used in Deep Z by leveraging the new lower and upper bounds. That is, using the tighter bounds l x, u x for x, we deﬁne the Re LU transformer for y := max(0, x) as follows:

ˆx, if l x > 0, 0, if u x 0, λ ˆx + µ + µ ϵnew, otherwise.

Here λ = u x u x l x , µ = u x l x 2 (u x l x), and ϵnew [ 1, 1] is a new noise symbol.

The reﬁned Re LU transformer beneﬁts from the improved bounds. For example, when lx < 0 and ux > 0 holds for the original bounds then after reﬁnement:

If l x > 0, then the output is the same as the input and no overapproximation is added. Else if u x 0, then the output is exact. Otherwise, as shown in Fig. 2, the approximation with the tighter l x and u x has smaller area in the input-output plane than the original transformer that uses the imprecise lx and ux.

Obtaining constraints for reﬁnement. To enable reﬁnement with MILP, we need to obtain constraints which fully capture the behavior of the neural network up to the last layer whose abstract transformer has been executed. In our encoding, we have one variable for each neuron and we write x(k) i to denote the variable corresponding to the activation of the i-th neuron in the k-th layer, where the input layer has k = 0. Similarly, we write l(k) i and u(k) i to denote the best derived lower and upper bounds for this neuron.

From the input layer, we obtain constraints of the form l0 i x(0) i u0 i , from afﬁne layers, we obtain constraints of the form x(k) i = P

j a(k 1) ij x(k 1) j + b(k 1) i and from Re LU layers we obtain

constraints of the form x(k) i = max(0, x(k 1) i ).

MILP. Let ϕ(k) denote the conjunction of all constraints up to and including those from layer k. To obtain the best possible lower and upper bounds for layer k with p neurons, we need to solve the following 2 p optimization problems:

l (k) i = min x(0) 1 ,...,x(k) p s.t. ϕ(k)(x(0) 1 ,...,x(k) p )

x(k) i , for i = 1, . . . , p,

u (k) i = max x(0) 1 ,...,x(k) p s.t. ϕ(k)(x(0) 1 ,...,x(k) p )

x(k) i , for i = 1, . . . , p.

As was shown by Tjeng et al. (2019), such optimization problems can be encoded exactly as MILP instances using the bounds computed by abstract interpretation and the instances can then be solved using off-the-shelf MILP solvers to compute l (k) i and u (k) i .

Published as a conference paper at ICLR 2019

LP relaxation. While not introducing any approximation, unfortunately, current MILP solvers do not scale to larger neural networks. It becomes increasingly more expensive to reﬁne bounds with the MILP-based formulation as the analysis proceeds deeper into the network. However, for soundness it is not crucial that the produced bounds are the best possible: for example, plain abstract interpretation uses sound bounds produced by the bounding box function ι instead. Therefore, for deeper layers in the network, we explore the trade-off between precision and scalability by also considering an intermediate method, which is faster than exact MILP, but also more precise than abstract interpretation. We relax the constraints in ϕ(k) using the bounds computed by abstract interpretation in the same way as Ehlers (2017) to obtain a set of weaker linear constraints ϕ(k) LP . We then use the solver to solve the relaxed optimization problems that are constrained by ϕ(k) LP instead of ϕ(k), producing possibly looser bounds l (k) and u (k). Note that the encoding of subsequent layers depends on the bounds computed in previous layers, where tighter bounds reduce the amount of newly introduced approximation.

Anytime MILP relaxation. MILP solvers usually provide the option to provide an explicit timeout after which the solver must terminate. In return, the solver may not be able to solve the instance exactly, but it will instead provide lower and upper bounds on the objective function in a best-effort fashion. This provides another way to compute sound but inexact bounds l (k) and u (k).

In practice, we choose a fraction θ (0, 1] of neurons in a given layer k and compute bounds for them using MILP with a timeout T in a ﬁrst step. In the second step, for a fraction δ [0, 1 θ] of neurons in the layer, we set the timeout to β T, where T is the average time taken by the MILP solver to solve one of the instances from the ﬁrst step and β [0, 1] is a parameter.

Neuron selection heuristic. To select the θ-fraction of neurons for the ﬁrst step of the anytime MILP relaxation for the k-th layer, we rank the neurons. If the next layer is a Re LU layer, we ﬁrst ignore all neurons whose activations can be proven to be non-positive using abstract interpretation (i.e., using the bounds produced by ι), because in this case it is already known that Re LU will map the activation to 0. The remaining neurons are ordered in up to two different ways, once by width (i.e. neuron i has key u(k) i l(k) i ), and possibly once by the sum of absolute output weights. i.e., if the next layer is a fully connected layer x 7 Ax + b, the key of neuron i is P

j |Ai,j|. If the next layer is a Re LU layer, we skip the Re LU layer and use the weights from the fully connected layer that follows it (if any). The two ranks of a neuron in both orders are added, and the θ-fraction with smallest rank sum is selected and their bounds are reﬁned with a timeout of T whereas the next δ-fraction of neurons are reﬁned with a timeout of β T.

Reﬁne Zono: end-to-end approach. To certify robustness of deep neural networks, we combine MILP, LP relaxation, and abstract interpretation. We ﬁrst pick numbers of layers k MILP, k LP, k AI that sum to the total number of layers of the neural network. For the analysis of the ﬁrst k MILP layers, we reﬁne bounds using anytime MILP relaxation with the neuron selection heuristic. As an optimization, we do not perform reﬁnement after the abstract transformer for the ﬁrst layer in case it is an afﬁne transformation, as the abstract domain computes the tightest possible bounding box for an afﬁne transformation of a box (this is always the case in our experiments). For the next k LP layers, we reﬁne bounds using LP relaxation (i.e., the network up to the layer to be reﬁned is encoded using linear constraints) combined with the neuron selection heuristic. For the remaining k AI layers, we use abstract interpretation without additional reﬁnement (however, this also beneﬁts from reﬁnement that was performed in previous layers), and compute the bounds using ι.

Final property certiﬁcation. Let k be the index of the last layer and p be the number of output classes. We can encode the ﬁnal certiﬁcation problem using the output abstract element aout obtained after applying the abstract transformer for the last layer in the network. If we want to prove that class i is assigned a higher probability than class j, it sufﬁces to show that aout (x(k) i x(k) j ) = . If this fails, one can resort to complete veriﬁcation using MILP: the property is satisﬁed if and only if the set of constraints ϕ(k)(x(0) 1 , . . . , x(k) p ) (x(k) i x(k) j ) is unsatisﬁable.

Published as a conference paper at ICLR 2019

Table 1: Neural network architectures used in our experiments.

Dataset Model Type #Neurons #layers Defense

MNIST 3 50 fully connected 160 3 None 5 100 fully connected 510 5 Diff AI 6 100 fully connected 610 6 None 9 100 fully connected 910 9 None 6 200 fully connected 1 210 6 None 9 200 fully connected 1 810 9 None Conv Small convolutional 3 604 3 None Conv Big convolutional 34 688 6 Diff AI Conv Super convolutional 88 500 6 Diff AI

CIFAR10 6 100 fully connected 610 6 None Conv Small convolutional 4 852 3 Diff AI

ACAS Xu 6 50 fully connected 305 6 None

4 EVALUATION

We evaluate the effectiveness of our approach for the robustness veriﬁcation of Re LU-based feedforward and convolutional neural networks. The results show that our approach enables faster complete veriﬁcation than the state-of-the-art complete veriﬁers: Wang et al. (2018b) and Tjeng et al. (2019), and produces more precise results than state-of-the-art incomplete veriﬁers: Deep Z (Singh et al., 2018) and Deep Poly (Singh et al., 2019), when complete certiﬁcation becomes infeasible.

We implemented our approach in a system called Reﬁne Zono. Reﬁne Zono uses Gurobi (Gurobi Optimization, LLC, 2018) for solving MILP and LP instances and is built on top of the ELINA library (eli, 2018; Singh et al., 2017) for numerical abstract domains. All of our code, neural networks, and images used in our experiments are publicly available at https://github.com/eth-sri/eran.

Evaluation datasets. We used the popular MNIST (Lecun et al., 1998), CIFAR10 (Krizhevsky, 2009), and ACAS Xu (Julian et al., 2018) datasets in our experiments. MNIST contains grayscale images of size 28 28 pixels whereas CIFAR10 contains RGB images of size 32 32. ACAS Xu contains 5 inputs representing aircraft sensor data.

Neural networks. Table 1 shows 12 different MNIST, CIFAR10, and ACAS Xu feedforward (FNNs) and convolutional networks (CNNs) with Re LU activations used in our experiments. Out of these 4 were trained to be robust against adversarial attacks using Diff AI (Mirman et al., 2018) whereas the remaining 8 had no adversarial training. The largest network in our experiments contains > 88K neurons whereas the deepest network contains 9 layers.

Robustness properties. For MNIST and CIFAR10, we consider the L -norm (Carlini & Wagner, 2017) based adversarial region parameterized by ϵ R. Our goal here is to certify that the network produces the correct label on all points in the adversarial region. For ACAS Xu, our goal is to verify that the property φ9 (Katz et al., 2017) holds for the 6 50 network (known to be hard).

Experimental setup. All experiments for the 3 50 MNIST FNN and all CNNs were carried out on a 2.6 GHz 14 core Intel Xeon CPU E5-2690 with 512 GB of main memory; the remaining FNNs were evaluated on a 3.3 GHz 10 Core Intel i9-7900X Skylake CPU with a main memory of 64 GB.

Benchmarks. For each MNIST and CIFAR10 network, we selected the ﬁrst 100 images from the respective test set and ﬁltered out those images that were not classiﬁed correctly. We consider complete certiﬁcation with Reﬁne Zono on the ACAS Xu network and the 3 50 MNIST network. For the 3 50 network, we choose an ϵ for which the incomplete veriﬁer Deep Z certiﬁed < 40% of all candidate images. We consider incomplete certiﬁcation for the remaining networks and choose an ϵ for which complete certiﬁcation with Reﬁne Zono becomes infeasible.

Published as a conference paper at ICLR 2019

Table 2: Precision and runtime of Reﬁne Zono vs. Deep Z and Deep Poly.

Dataset Model ϵ Deep Z Deep Poly Reﬁne Zono

precision(%) time(s) precision(%) time(s) precision(%) time(s)

MNIST 5 100 0.07 38 0.6 53 0.3 53 381 6 100 0.02 31 0.6 47 0.2 67 194 9 100 0.02 28 1.0 44 0.3 59 246 6 200 0.015 13 1.8 32 0.5 39 567 9 200 0.015 12 3.7 30 0.9 38 826 Conv Small 0.12 7 1.4 13 6.0 21 748 Conv Big 0.2 79 7 78 61 80 193 Conv Super 0.1 97 133 97 400 97 665

CIFAR10 6 100 0.0012 31 4.0 46 0.6 46 765 Conv Small 0.03 17 5.8 21 20 21 550

4.1 COMPLETE CERTIFICATION

Reﬁne Zono ﬁrst runs Deep Z analysis on the whole network collecting the bounds for all neurons in the network. If Deep Z fails to certify the network, then the collected bounds are used to encode the robustness certiﬁcation as a MILP instance (discussed in section 3).

ACAS Xu 6 50 network. As this network has only 5 inputs, we uniformly split the pre-condition deﬁned by φ9 to produce 6 300 smaller input regions. We certify that the post-condition deﬁned by φ9 holds for each region with Reﬁne Zono. Reﬁne Zono certiﬁes that φ9 holds for the network in 227 seconds which is > 4x faster than the fastest veriﬁer for ACAS Xu from Wang et al. (2018b).

MNIST 3 50 network. We use ϵ = 0.03 for the L -norm attack. We compare Reﬁne Zono against the state-of-the-art complete veriﬁer for MNIST from Tjeng et al. (2019). This approach is also MILP-based like ours, but it uses Interval analysis and LP to determine neuron bounds. We implemented the Interval analysis and LP-based analysis to determine the initial bounds. We call the MILP solver only if LP analysis (or Interval analysis) fails to certify. All complete veriﬁers certify the neural network to be robust against L -norm perturbations on 85% of the images. The average runtime of Reﬁne Zono, MILP with bounds from the Interval analysis, and MILP with bounds from the LP analysis are 28, 123, and 35 seconds respectively. Based on our result, we believe that the Zonotope analysis offers a good middle ground between the speed of the Interval analysis and the precision of LP for bound computation, as it produces precise bounds faster than LP.

4.2 INCOMPLETE CERTIFICATION

We next compare Reﬁne Zono against Deep Z and Deep Poly for the incomplete robustness certiﬁcation of the remaining networks. We note that Deep Z has the same precision as Fast-Lin (Weng et al., 2018) and Deep Poly has the same precision as CROWN (Zhang et al., 2018). The ϵ values used for the L -norm attack are shown in Table 2. The ϵ values for networks trained to be robust are larger than for networks that are not. For each veriﬁer, we report the average runtime per image in seconds and the precision measured by the % of images for which the veriﬁer certiﬁed the network to be robust. We note that running the Interval analysis to obtain initial bounds is too imprecise for these large networks with the ϵ values considered in our experiments. As a result, the approach from Tjeng et al. (2019) has to rely on applying LP per neuron to obtain precise bounds for the MILP solver which does not scale. For example, on the 9 200 network, determining bounds with LP already takes > 20 minutes (without calling the MILP solver which is more expensive than LP) whereas Reﬁne Zono has an average running time of 14 minutes.

Parameter values. We experimented with different values of the analysis parameters k MILP, k LP, k AI, θ, δ, β, T and chose values that offered the best tradeoff between performance and precision for the certiﬁcation of each neural network. We reﬁne the neuron bounds after all afﬁne transformations

Published as a conference paper at ICLR 2019

that are followed by a Re LU except the ﬁrst one. In a given layer, we consider all neurons that can take positive values after the afﬁne transformation as reﬁnement candidates.

For the MNIST FNNs, we reﬁne the bounds of the candidate neurons in layers 2-4 with MILP and those in the remaining layers using LP. For MILP based reﬁnement, we use θ = ω 5k 2 p where ω is the number of candidates and p is the total number of neurons in layer k. For LP based reﬁnement, we use θ = ω 2k 5 p. We use timeout T = 1 second, β = 0.5, and δ = ω

p θ for both MILP and LP based reﬁnements. For the CIFAR10 FNN, we use the same values except that we use θ = ω 2k 2 p for MILP reﬁnement and set T = 6 seconds for both MILP and LP based reﬁnement as it is more expensive to reﬁne neuron bounds in CIFAR10 networks due to these having more input neurons.

For the CNNs, the convolutional layers have large number of candidates so we do not reﬁne these. Instead, we reﬁne all candidates in the fully connected layers with a larger timeout so to compensate for the more difﬁcult problem instances for the solver. For the MNIST Conv Small, Conv Big and CIFAR10 Conv Small networks, we reﬁne all the candidate neurons using MILP with T = 10 seconds. For the MNIST Conv Super network, we reﬁne similarly but use LP with T = 15 seconds.

Results for incomplete certiﬁcation. Table 2 shows the precision and the average runtime of all three veriﬁers. Reﬁne Zono either improves or achieves the precision of the state-of-the-art veriﬁers on all neural networks. It certiﬁes more images than Deep Z on all networks except the MNIST Conv Super network. This is because Deep Z is already very precise for the ϵ considered. We could not try larger ϵ for this network, as the Deep Z analysis becomes too expensive. Reﬁne Zono certiﬁes the network to be more robust on more images than Deep Poly on 6 out of 10 networks.

It can be seen that the number of neurons in the network is not the determining factor for the average runtime of Reﬁne Zono. We observe that Reﬁne Zono runs faster on the networks trained to be robust and the top three networks with the largest runtime for Reﬁne Zono are all networks not trained to be robust. This is because robust networks are relatively easier to certify and produce only a small number of candidate neurons for reﬁnement, which are easier to reﬁne by the solver. For example, even though the same parameter values are used for reﬁning the results on the MNIST Conv Small and Conv Big networks, the average runtime of Reﬁne Zono on the robustly trained Conv Big network with 35K neurons, 6 layers and a perturbation region deﬁned using ϵ = 0.2 is almost 4 times less than on the non-robust Conv Small network with only 3 604 neurons, 3 layers and a smaller ϵ = 0.12.

4.3 EFFECT OF NEURON SELECTION HEURISTIC

We use the neuron selection heuristic from section 3 to determine neurons which need to be reﬁned more than others for FNNs, as reﬁning all neurons in a layer with MILP can signiﬁcantly slow down the analysis. To check whether our heuristic can identify important neurons, we ran the analysis on the MNIST 9 200 FNN by keeping all analysis parameters the same, except instead of selecting the neurons with the smallest rank sum ﬁrst we selected the neurons with the largest rank sum ﬁrst (thus reﬁning neurons more if our heuristic deems them unimportant). With this change, the average runtime does not change signiﬁcantly. However, the modiﬁed analysis loses precision and fails to certify two images that the analysis reﬁning with our neuron selection heuristic succeeds on.

5 CONCLUSION

We presented a novel reﬁnement-based approach for effectively combining overapproximation techniques used by incomplete veriﬁers with linear-programming-based methods used in complete veriﬁers. We implemented our method in a system called Reﬁne Zono and showed its effectiveness on veriﬁcation tasks involving feedforward and convolutional neural networks with Re LU activations.

Our evaluation demonstrates that Reﬁne Zono can certify robustness properties beyond the reach of existing state-of-the-art complete veriﬁers (these can fail due to scalability issues) while simultaneously improving on the precision of existing incomplete veriﬁers (which can fail due to using too coarse of an overapproximation).

Overall, we believe combining the strengths of overapproximation methods with those of mixed integer linear programming as done in this work is a promising direction for further advancing the state-of-the-art in neural network veriﬁcation.

Published as a conference paper at ICLR 2019

ELINA: ETH Library for Numerical Analysis, 2018. URL http://elina.ethz.ch.

Filippo Amato, Alberto L opez, Eladia Mar ıa Pe na-M endez, Petr Vaˇnhara, Aleˇs Hampl, and Josef Havel. Artiﬁcial neural networks in medical diagnosis. Journal of Applied Biomedicine, 11(2):47 58, 2013.

Mariusz Bojarski, Davide Del Testa, Daniel Dworakowski, Bernhard Firner, Beat Flepp, Prasoon Goyal, Lawrence D. Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, Xin Zhang, Jake Zhao, and Karol Zieba. End to end learning for self-driving cars. Co RR, abs/1604.07316, 2016.

Nicholas Carlini and David A. Wagner. Towards evaluating the robustness of neural networks. In Proc. IEEE Symposium on Security and Privacy (SP), pp. 39 57, 2017.

Chih-Hong Cheng, Georg N uhrenberg, and Harald Ruess. Maximum resilience of artiﬁcial neural networks. In Automated Technology for Veriﬁcation and Analysis (ATVA), 2017.

Patrick Cousot and Radhia Cousot. Abstract interpretation: a uniﬁed lattice model for static analysis of programs by construction or approximation of ﬁxpoints. In Proceedings of the 4th ACM symposium on Principles of programming languages (POPL), pp. 238 252, 1977.

Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. Output range analysis for deep feedforward neural networks. In NASA Formal Methods (NFM), 2018.

Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy A. Mann, and Pushmeet Kohli. A dual approach to scalable veriﬁcation of deep networks. Co RR, abs/1803.06567, 2018.

R udiger Ehlers. Formal veriﬁcation of piece-wise linear feed-forward neural networks. In Automated Technology for Veriﬁcation and Analysis (ATVA), 2017.

Matteo Fischetti and Jason Jo. Deep neural networks and mixed integer linear optimization. Constraints, 23(3):296 309, 2018.

T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev. AI2: Safety and robustness certiﬁcation of neural networks with abstract interpretation. In Proc. IEEE Symposium on Security and Privacy (SP), volume 00, pp. 948 963, 2018.

Khalil Ghorbal, Eric Goubault, and Sylvie Putot. The zonotope abstract domain taylor1+. In Proc. Computer Aided Veriﬁcation (CAV), pp. 627 633, 2009.

Ian J Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. ar Xiv preprint ar Xiv:1412.6572, abs/1706.07351, 2014.

Gurobi Optimization, LLC. Gurobi optimizer reference manual, 2018. URL http://www. gurobi.com.

G. Hinton, L. Deng, D. Yu, G. E. Dahl, A. Mohamed, N. Jaitly, A. Senior, V. Vanhoucke, P. Nguyen, T. N. Sainath, and B. Kingsbury. Deep neural networks for acoustic modeling in speech recognition: The shared views of four research groups. IEEE Signal Processing Magazine, 29(6):82 97, 2012.

Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety veriﬁcation of deep neural networks. In Computer Aided Veriﬁcation (CAV), pp. 3 29, 2017.

Kyle D. Julian, Mykel J. Kochenderfer, and Michael P. Owen. Deep neural network compression for aircraft collision avoidance systems. Co RR, abs/1810.04240, 2018.

Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efﬁcient SMT solver for verifying deep neural networks. In Computer Aided Veriﬁcation (CAV), pp. 97 117, 2017.

Alex Krizhevsky. Learning multiple layers of features from tiny images. Technical report, 2009.

Published as a conference paper at ICLR 2019

Yann Lecun, L eon Bottou, Yoshua Bengio, and Patrick Haffner. Gradient-based learning applied to document recognition. In Proc. of the IEEE, pp. 2278 2324, 1998.

Alessio Lomuscio and Lalit Maganti. An approach to reachability analysis for feed-forward Re LU neural networks. Co RR, 2017.

Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for provably robust neural networks. In Proc. International Conference on Machine Learning (ICML), pp. 3575 3583, 2018.

Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semideﬁnite relaxations for certifying robustness to adversarial examples. In Proc. Advances in Neural Information Processing Systems (Neur IPS), pp. 10900 10910. 2018.

Gagandeep Singh, Markus P uschel, and Martin Vechev. Fast polyhedra abstract domain. In Proc. Principles of Programming Languages (POPL), pp. 46 59, 2017.

Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus P uschel, and Martin Vechev. Fast and effective robustness certiﬁcation. In Proc. Advances in Neural Information Processing Systems (Neur IPS), pp. 10825 10836. 2018.

Gagandeep Singh, Timon Gehr, Markus P uschel, and Martin Vechev. An abstract domain for certifying neural networks. Proc. ACM Program. Lang., 3(POPL):41:1 41:30, 2019. ISSN 2475-1421.

Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In Proc. International Conference on Learning Representations (ICLR), 2019.

Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. In USENIX Security Symposium (USENIX Security 18), pp. 1599 1614, 2018a.

Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efﬁcient formal safety analysis of neural networks. In Proc. Advances in Neural Information Processing Systems (Neur IPS), pp. 6369 6379. 2018b.

Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards fast computation of certiﬁed robustness for Re LU networks. In Proc. International Conference on Machine Learning (ICML), volume 80, pp. 5276 5285, 2018.

Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In Proc. International Conference on Machine Learning (ICML), volume 80, pp. 5286 5295, 2018.

Weiming Xiang, Hoang-Dung Tran, and Taylor T. Johnson. Output reachable set estimation and veriﬁcation for multi-layer neural networks. Co RR, abs/1708.03322, 2017.

Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efﬁcient neural network robustness certiﬁcation with general activation functions. In Proc. Advances in Neural Information Processing Systems (Neur IPS), pp. 4944 4953. 2018.