# hierarchical_verification_for_adversarial_robustness__da7cc959.pdf

Hierarchical Verification for Adversarial Robustness

Cong Han Lim 1 Raquel Urtasun 1 2 Ersin Yumer 1

We introduce a new framework for the exact pointwise ℓp robustness verification problem that exploits the layer-wise geometric structure of deep feed-forward networks with rectified linear activations (Re LU networks). The activation regions of the network partition the input space, and one can verify the ℓp robustness around a point by checking all the activation regions within the desired radius. The Geo Cert algorithm (Jordan et al., 2019) treats this partition as a generic polyhedral complex in order to detect which region to check next. In contrast, our Layer Cert framework considers the nested hyperplane arrangement structure induced by the layers of the Re LU network and explores regions in a hierarchical manner. We show that, under certain conditions on the algorithm parameters, Layer Cert provably reduces the number and size of the convex programs that one needs to solve compared to Geo Cert. Furthermore, our Layer Cert framework allows the incorporation of lower bounding routines based on convex relaxations to further improve performance. Experimental results demonstrate that Layer Cert can significantly reduce both the number of convex programs solved and the running time over the state-of-the-art.

1. Introduction

Deep neural networks have been demonstrated to be susceptible to adversarial perturbations of the inputs (e.g., Szegedy et al. (2013); Biggio et al. (2013); Goodfellow et al. (2014)). Hence, it is important to be able to measure how vulnerable a neural network may be to such noise, especially for safety-critical applications. We study the problem of pointwise exact verification for ℓp-norm adver-

Work done as part of first author s AI Residency Program. 1Uber Advanced Technologies Group, Toronto ON, Canada 2Department of Computer Science, University of Toronto, Toronto ON, Canada. Correspondence to: Cong Han Lim <conghan@uber.com>.

Proceedings of the 37 th International Conference on Machine Learning, Online, PMLR 119, 2020. Copyright 2020 by the author(s).

sarial robustness for trained deep feed-forward networks with Re LU activation functions. The point-wise ℓp robustness with respect to an input x Rn and a classifier c : Rn [C] := {1, 2, 3, . . . , C} is defined as

ϵ (x; c) := min v p ϵ ϵ s.t. c(x + v) = c(x). (1)

The goal of exact or complete robustness verification is to check if ϵ > r for some desired radius r. The choices of p studied in the literature are typically 1, 2, and ; our work applies to all p 1. Solving Problem (1) exactly (or within a factor of 1 o(1) ln n) is known to be NP-hard (Weng et al., 2018). Developing methods that perform well in practice would require a better understanding of the mathematical structure of neural networks.

In this work, we approach the problem from the angle of how to directly exploit the geometry induced in input space by the neural network. Each activation pattern (i.e., whether each neuron is on or off) corresponds to a polyhedral region in the input space, and the decision boundary within each region is linear. A natural geometric approach to the verification problem is then to check regions in order of their distance. We illustrate this in Figure 1. We can terminate this process either when we have reached the desired verification radius or when we have exceeded the distance to the closest decision boundary found. In the latter case the distance to that boundary is the solution to Problem (1).

Jordan et al. (2019) proposed the first algorithm for this distance-based exploration of the regions. Their Geo Cert algorithm navigates the regions in order of distance by maintaining a priority queue containing all the polyhedral faces that make up the frontier of all regions that have been visited. The priority associated with each face is computed via an optimization problem that can be solved by a generic convex programming solver. Under a limited time budget, Geo Cert finds a stronger computational lower bound for ϵ (x; c) compared to a complete method that directly uses mixed-integer programming (Tjeng et al., 2019).

In this paper we introduce the Layer Cert framework that makes use of the layer-wise structure of neural networks. The first layer of Re LUs induce a hyperplane arrangement structure, and each subsequent layer induces one within each region of the hyperplane arrangement from the previous layer. This forms a nested hyperplane pattern and a

Hierarchical Verification for Adversarial Robustness

Figure 1. How geometric methods explore the input space. Each square illustrates one step in the process of exploring regions of increasing ℓ2 distance from the initial point x. The box represents the input space to a Re LU network, the inner black lines the regions induced by three first layer Re LUs, and brown lines the regions by another three Re LUs in the second layer. The blue regions are being processed during that step, while the green regions have already been processed.

hierarchy of regions/subregions that our algorithm will use to navigate the input space. This hierarchical approach has two main advantages over Geo Cert:

1. Provable reduction in the number and size of convex programs solved when using a convex distance-based priority function.

2. The ability to incorporate convex-relaxation-based lower bounding/incomplete methods for Problem (1) to reduce the number of regions that are processed.

We demonstrate the first advantage by studying a simplified version of Layer Cert (Layer Cert-Basic), which introduces our hierarchical approach to navigating the regions but does not include the use of additional subroutines to prune the search space. By making use of the nested hyperplane structure, Layer Cert provably reduces the number of convex programs and the sizes of each program that need to be solved compared to Geo Cert when using the same convex distance priority function. This is done by identifying a minimal set of programs that are required and by amortizing the work associated with a single region in Geo Cert across multiple levels of the hierarchy in Layer Cert.

The second advantage comes from the fact that each region R in the i-th level of the hierarchy is associated with a set of children regions in the (i + 1)-th level that is contained entirely within R. This allows us to use incomplete verifiers over just this region to determine if the region might intersect with a decision boundary. If the verifier returns that no such overlap exists, we can then safely remove the

region and all its children from further consideration. One straightforward way to do this is to use efficient reachability methods such as interval arithmetic (Xiang et al., 2018). In this work we also develop a novel method that leverages linear lower bounds on the neural network function (Weng et al., 2018; Zhang et al., 2018) to construct a half-space that is guaranteed not to contain any part of the decision boundary. This can restrict the search space significantly. Furthermore, we can warm start Layer Cert by projecting the input point onto the half-space.

Using the experimental setup of Jordan et al. (2019), we compare the number of programs solved and overall wallclock time of different variants of Geo Cert and Layer Cert. Each Layer Cert method uses a different combination of lower-bounding methods. For Geo Cert, we consider different choices of priority functions. In addition to the standard ℓp distance priority function, Jordan et al. (2019) describes a non-convex priority function that incorporates a Lipschitz term. This Lipschitz variant modifies the order in which regions are processed and also provides an alternative warmstart procedure. Our Layer Cert variants consistently outperform Geo Cert using just the ℓp distance priority function and in most experiments our lower-bounding techniques outperform the Lipschitz variant of Geo Cert.

Notation. We use [k] to denote the index set {1, 2, . . . , k}. Superscripts are used to index distinct objects, with the exception of Rn and R+ to denote the n-dimensional Euclidean space and the nonnegative real numbers respectively. We use subscripts for vectors and matrices to refer to entries in the objects and subscripts for sets to refer to distinct sets. We use typewriter fonts to denote subroutines.

2. Related work

Besides Geo Cert (Jordan et al., 2019), the majority of exact or complete verification methods are based on branch-andbound (e.g. Katz et al. (2017); Wang et al. (2018); Tjeng et al. (2019); Anderson et al. (2019a); Lu & Kumar (2020)), and Bunel et al. (2018; 2019) provide a detailed overview. These methods construct a search tree over the possible individual Re LU activations and use upper and lower bounds to prune the tree. The upper bounds come from adversarial examples, while the lower bounds are obtained by solving a relaxation of the original problem, which we briefly discuss in the next paragraph. Since our focus in this work is on methods that directly leverage the geometry of the neural network function in the input space, we leave a detailed comparison against these methods to future work.

Instead of exactly measuring or verifying, we can instead overapproximate or relax the set reachable by an ϵ-ball around the input point (e.g. Dvijotham et al. (2018); Xiang et al. (2018); Singh et al. (2018); Weng et al. (2018); Wong

Hierarchical Verification for Adversarial Robustness

& Kolter (2018); Zhang et al. (2018); Singh et al. (2019b)). These incomplete approaches give us a lower bound for Problem (1). These can only certify that there is no perturbation that changes the class within some radius r for some r that can be much smaller than ϵ (x; c) The majority of the works focus on different convex relaxations of the Re LU activations (see Salman et al. (2019) for a discussion of the tightness of the different approaches), though recent works have started going beyond single Re LU relaxations (Singh et al., 2019a; Anderson et al., 2019b). Another line of work studies how to efficiently bound the Lipschitz constant of the neural network function (Szegedy et al., 2013; Bartlett et al., 2017; Balan et al., 2017; Weng et al., 2018; Combettes & Pesquet, 2019; Fazlyab et al., 2019; Zou et al., 2019).

The complexity of geometric methods (and many other exact methods) for robustness verification can be upper bounded by a constant (number of activation regions) (complexity of solving a convex program). There have been several works in recent years that study the number of these activation regions in Re LU networks. The current tightest upper and lower bounds for the maximum number of nonempty activation regions, which are exponential in the number of Re LU neurons, is given by Serra et al. (2018). Hanin & Rolnick (2019) provide an upper bound on the expected number of regions (exponential in the lesser of the input dimension and the number of Re LU neurons).

3. Hierarchical Structure of Re LU Networks

In this section, we describe the structure induced by the Re LU neurons in the input space and how this leads naturally to a hierarchy of regions that we use in our approach.

3.1. Hyperplane Arrangements

Definition 3.1. (Hyperplanes and hyperplane arrangements) A hyperplane H Rn is an (n 1)-dimensional affine space that can be written as {x | a x = b} for some a Rn and b R. A hyperplane arrangement H is a finite set of hyperplanes.

Definition 3.2. (Halfspaces) Given a hyperplane H := {x | a x = b}, the halfspaces H and H correspond to the sets {x | a x b} and {x | a x b}, respectively. A polyhedron is a finite intersection of halfspaces.

Definition 3.3. (Patterns and regions in hyperplane arrangements) Given a hyperplane arrangement H and a pattern P : H { 1, +1}, the corresponding region is

P (H)= 1 H \

P (H)=+1 H .

We say that another pattern Q : H { 1, +1} (or region RQ) is a neighbor of P (RP resp.) if P and Q differ only on a single hyperplane.

3.2. Geometric Structure of Deep Re LU Networks

A Re LU network with L hidden layers for classification with C classes and ni neurons in the i-th layer for i [L] can be represented as follows:

x0 := x input,

zi := W i 1xi 1 + bi 1 for i [L + 1], (2)

xi := relu(zi) for i [L],

f(x) := W Lx L + b L = z L+1 output,

where W i, bi describe the weight matrix and bias in the i-th layer and the Re LU function is defined as relu(v))i := max(0, vi). The length of bi is ni+1 for i [L 1] and b0 Rn and b L RC. The classification decision is given by argmaxi(f(x))i, and the decision boundary between classes i and j is the set {x | fi(x) fj(x) = 0}.

Note that layers like batch normalization layers, convolutional layers, and average pooling layers can be included in this framework by using the appropriate weights and biases. We can also have a final softmax layer since it does not affect the decision boundaries as it is a symmetric monotonically increasing function. Definition 3.4. (Full activation patterns) Let ni denote the number of neurons in the i-th layer. A (full) activation pattern A = (A1, . . . , AL) is a collection of functions Ai : [ni] { 1, +1}. Two activation patterns are neighbors if they differ on exactly one layer for exactly one neuron.

We can define a neighborhood graph over the set of activation patterns where each node presents a pattern and we add an edge between neighboring patterns. Definition 3.5. (Activation patterns and the input space) For an input x, the (full) activation pattern of x is Ax where

Ax i (j) :=

( +1 if zi j 0, 1 if zi j < 0, (3)

where the zi j terms are defined according to (2). Conversely, given an activation pattern A, the corresponding activation region is RA := {x | Ax = A}.

Given an activation pattern A and some x RA, the corresponding zi+1 terms for i [L] are given by

zi+1 = W i IAizi + bi (4)

where IAi is the diagonal ni ni binary matrix such that

( 1 if j = k and Ai(j) = 1, 0 otherwise.

k=j+1 W k IAk

Hierarchical Verification for Adversarial Robustness

Figure 2. Left: the activation regions of a Re LU network with one hidden layer forms a hyperplane arrangement. Middle: the activation regions of a Re LU network with two hidden layers. Note that within the regions defined by the previous layer, the lines induce a hyperplane arrangement. Right: The neighborhood graph of the regions.

we can expand Eq. (4) as

j=1 W j IAj

W 0x + ci. (5)

Hence, each zi term and f(x) can be expressed as a linear expression over x involving W i, IAi, and bi terms. This also allows us to write RA in the form of linear inequalities over x as a polyhedron

{x | Ai(j)zi j 0 for i [L], j [ni]} (6)

Since the neural network function f is linear within each activation region, each decision boundary is also linear within each activation region. This allows us to efficiently compute the classification decision boundaries.

The set of activation regions for a network with one hidden layer corresponds to the regions of a hyperplane arrangement (where each row of W 0 and the corresponding entry in b0 defines a hyperplane). With each additional layer, we take the regions corresponding to the previous layer and add a hyperplane arrangement to each region. Thus, this leads to a nested hyperplane arrangement. Figure 2 illustrates this structure and the corresponding neighborhood graph.

In addition to full activation patterns, it is useful to consider the patterns for all neurons up to a particular layer.

Definition 3.6. (Partial activation patterns and regions) Given some l < L, an l-layer partial activation pattern A = (A1, . . . , Al) is a collection of functions Ai : [ni] { 1, +1}. The corresponding partial activation region RA is {x | Ai(j)zi j 0 for i [L], j [ni]}.

The partial activation regions naturally induce a hierarchy of regions. We can describe the relationship between the regions in the different levels in the following terms:

Definition 3.7. For a l-layer activation pattern A = (A1, . . . , Al), let parent(A) := (A1, . . . , Al 1). The terms child and descendant are defined analogously.

Figure 3. The hierarchical structure induced by the partial activation regions. Each partial region is marked by a circle node. The nodes of the same color represent the closest subregion within a parent region to the input point x. For example, the upper left most green nodes in levels 1 and 2 are connected.

Definition 3.8. Two l-layer partial activation patterns are siblings if they share the same parent pattern. They are neighboring siblings if they differ on exactly one neuron in the l-th layer and agree everywhere else.

We can use Defintion 3.7 and 3.8 to define a hierarchical search graph with L + 1 levels. The nodes in the l-th level represent the l-layer activation patterns. We connect two activation patterns in the same level if they are neighboring siblings. We connect a pattern A to parent(A) if RA is the region closest to the input point x out of all its siblings. We introduce a single node in the level 0 and connect it to the first-layer activation pattern that contains x. Figure 3 illustrates this hierarchy of activation regions and the corresponding hierarchical search graph. In Sections 4 and 5, we describe how to leverage this hierarchical structure to design efficient algorithms for verification.

4. Exploring Activation Regions Geometrically

In this section, we first describe the Geo Cert algorithm (Jordan et al., 2019) that provides a method for navigating the activation regions in order of increasing distance from the input. We subsequently consider the hierarchy of partial regions and describe Layer Cert-Basic that leverages the geometric structure to provably reduce the number and size of convex programs compared to Geo Cert. We then introduce the full Layer Cert framework in Section 5.

4.1. Prior Work: Geo Cert

Geo Cert performs a process akin to breadth-first search over the neighbourhood graph (see Figure 2). In each iteration, Geo Cert selects the activation region corresponding to the

Hierarchical Verification for Adversarial Robustness

Algorithm 1 Geo Cert

1: Input: x, y (label of x), U (upper bound) 2: Ax activation pattern of x 3: Q empty priority queue 4: Q.push((0, Ax)) 5: S 6: while Q = do 7: (d, A) Q.pop() 8: if A S then 9: continue 10: S S {A } 11: if U d then 12: return U 13: U min(decision bound(A, x, y), U) 14: for A N(A) \ S do 15: if Face(A, A ) is nonempty then 16: d priority(x, Face(A, A )) 17: Q.push((d , A ))

closest unexplored node neighbouring an explored node and then computes the distance to all regions neighbouring the selected region.

We provide a formal description of Geo Cert in Algorithm 1 and demonstrate an iteration of the algorithm in Figure 4. Setting the input U term to a radius r solves the robustness verification problem for that radius, while setting it sufficiently high measures the robustness (i.e., Problem (1)).

We describe the subroutines in detail below.

Measuring the distance to a distance boundary restricted to a region. The subroutine decision bound with inputs A, x, y solves the problem

min v RA x v p s.t. fy(v) fj(v) = 0 for j = y (7)

or returns if infeasible. This is equivalent to computing the ℓp projection of x onto the respective set. We can use algorithms specifically designed for projection onto sets such as Dykstra s method (Boyle & Dykstra, 1986). We can also use generic convex optimization solvers to handle a wider range of priority functions.

Computing the priority function. From (6), we can write each activation region RA as a polyhedron {x | Ai(j)zi j 0 for i [L], j [ni]}. A neighbouring region R A that differs only on the a-th neuron on the b-th layer will intersect with RA within the hyperplane H = {x | zb a 0}. We name the set RA H = R A H as Face(A, A ) since this set is a face of both A and A . As with RA and (6), we can write Face(A, A ) as

{x | Ai(j)zi j 0 for i [L], j [ni], za b = 0} (8)

Figure 4. One iteration of Geo Cert . The ball represents a level set of the priority function and the blue line the set of boundary faces of the explored regions. After popping the nearest unexplored activation region off a priority queue, Geo Cert computes the distance of previously unseen faces in that region (marked in red).

where zi j can be expressed in terms of the x variables using the expression in (5). Given some function q : Rn Rn R+, the subroutine priority with inputs x, Face(A, A ) solves the following optimization problem:

min v Face(A,A ) q(x, v). (9)

For ℓp-robustness, a natural choice of q is the ℓp distance function. Jordan et al. (2019) also propose an alternative variant of Geo Cert where they incorporate an additional miny =j fy(v) fj(v)

L term in the priority function, where L denotes an upper bound on the Lipschitz constant. This makes the priority function nonconvex. We will refer to the ℓp priority variant of Geo Cert as just Geo Cert and specifically use the term Geo Cert-Lip for the Lipschitz variant.

4.2. Our Approach Layer Cert

Instead of exploring the neighborhood graph of full activation regions, we develop an algorithm that makes use of the nested hyperplane arrangement and the graph induced by it. See Definition 3.7 and Figure 3 for a description of this graph. We first give a description of a basic form of Layer Cert in Algorithm 2, followed by theoretical results about this method.

In each iteration, Layer Cert processes the next nearest partial activation pattern by computing the distances to all sibling patterns to the queue. This is in contrast to Geo Cert which computes the distance to all neighbouring patterns of the next nearest full activation pattern.

The new subroutine in Layer Cert-Basic is next layer, which takes an l-layer activation pattern A and an input vector v and returns the l + 1 layer activation pattern that is a child of A and contains v:

next layer(A, v) :=(A1, . . . , Al, Av l+1)

where Av is the full activation pattern of v (Definition 3.5).

Hierarchical Verification for Adversarial Robustness

Algorithm 2 Layer Cert-Basic

1: Input: x, y (label of x), U (upper bound) 2: Ax activation pattern of x at first layer 3: Q empty priority queue 4: Q.push((0, Ax, x)) 5: S 6: while Q = do 7: (d, A, v) Q.pop() 8: if U d then 9: return U 10: if A is a full activation pattern then 11: U min(decision bound(A, x, y), U) 12: else 13: Q.push((d, next layer(A, v), v))

14: for A Ncurrent layer(A) \ S do 15: if Face(A, A ) is nonempty then 16: v , d priority(x, Face(A, A )) 17: Q.push((d , A , v )) 18: S S {A }

We prove in the appendix that when the priority function is a convex distance function, Layer Cert-Basic visits full activation patterns in ascending order of distance, which implies that it returns the correct solution.

Theorem 4.1. (Correctness of Layer Cert-Basic) If the priority function used is a convex distance function, Layer Cert processes full activation patterns in ascending order of distance and returns the distance of the closest point with a different class from x.

As a corollary of Theorem 4.1, Layer Cert-Basic and Geo Cert equipped with the same priority function visit the activation patterns in the same order (allowing for permutations of patterns with the exact same priority).

The primary difference in computational difficulty between the two methods is that the number and complexity of priority computations is reduced in Layer Cert. There are three main reasons for this. First, Layer Cert-Basic adds A to the set of seen patterns S once we have processed any neighbour of A. Hence, we only do a single priority computation for each A. This is not necessarily the case in Geo Cert. Secondly, the convex programs corresponding to nodes further up the hierarchy have less constraints since they only need to consider all neurons to the respective layer. Finally, in Layer Cert-Basic we do not need to compute priority between two l-layer partial activation patterns that differ on exactly a single neuron that is not in layer l (i.e. these patterns are not siblings). Geo Cert in contrast computes the priority between any two neighbours as long as the corresponding Face is non-empty. This allows us to amortize the number of convex programs to compute for a single full activation region in Geo Cert over

Algorithm 3 Layer Cert Framework

1: Input: x, y (label of x), U (upper bound) 2: d, A, v, M restriction(x, U) 3: Q empty priority queue 4: Q.push((d, A, v)) 5: S 6: while Q = do 7: (d, A, v) Q.pop() 8: if U d then 9: return U 10: if A is a full activation pattern then 11: U min(decision bound(A, x, y), U) 12: else 13: if contains db(A, x, U) = maybe then 14: Q.push((d, next layer(A, v), v))

15: for A Ncurrent layer(A) \ S do 16: if Face(A, A ) M is nonempty then 17: v , d priority(x, Face(A, A ) M) 18: Q.push((d , A , v )) 19: S S {A }

multiple levels in Layer Cert Consider a full activation pattern A = (A1, . . . , AL) and the set of all ancestor patterns B1, . . . , BL 1 where Bi := (A1, . . . , Ai). We have PL i ni potential neighbours for Geo Cert when processing pattern A. For Layer Cert-Basic, we have up to ni siblings when processing each Bi, for a total of PL i ni patterns when processing B1, . . . , BL 1, A.

These facts can be used to prove our main theoretical result about the complexity of Layer Cert-Basic. The proof of these and the main theorem are in the appendix.

Theorem 4.2. (Complexity of Layer Cert-Basic) Given an input x, suppose the distance to the nearest adversary returned by Layer Cert/Geo Cert is not equal to the distance of any activation region from x. Suppose we formulate the convex problems associated with decision bound and next layer using Formulations (6) and (8). We can construct an injective mapping from the set of convex programs solved by Layer Cert to the corresponding set in Geo Cert such that the constraints in the Layer Cert program is a subset of those in the corresponding Geo Cert program.

5. The Layer Cert Framework

We now describe how our hierarchical approach is amenable to the use of convex relaxation-based lower bounds to prune the search space. For simplicity, in this section we will assume that we are performing verification with respect to a targeted class y . The general Layer Cert framework is presented in Algorithm 3. The two new subroutines in the algorithm are contains db and restriction.

Hierarchical Verification for Adversarial Robustness

Let Bp,r(x) denote the ℓp-ball of radius r around x. The subroutine contains db(A, x, r) returns false when RA Bp,r(x) is guaranteed not to intersect with a decision boundary. This means that we can remove A and all its descendants from consideration. Otherwise, it returns maybe and we proceed on to the next level.

The routine restriction(x, r) explicitly computes a convex set M that is a superset of the part of the decision boundary contained in Bp,r(x). This both restricts the search directions we need to consider and also allows us to warm start the algorithm by projecting the initial point onto this set. In the following we describe some possible choices for these subroutines. In the appendix we discuss a version of Layer Cert that recursively applies a modified version of restriction to aggressively prune the search space.

Pruning partial activation regions. We can use incomplete verifiers (see Section 2 for references) to check if the region Bp,U(x) might contain a decision boundary. These methods work by implicitly or explicitly computing some overapproximation of the set

{fy(v) fy (v) | v Bp,U(x)}. (10)

If all values in (10) are strictly positive, then we know that the decision boundary cannot be in RA Bp,U(x).

Many incomplete verifiers work by constructing convex relaxations of each nonlinear Re LU function. If a neuron is guaranteed to be always on or always off over all points in the region of interest, we can use this to tighten the convex relaxation. This allows us to incorporate information from the current partial activation region into incomplete verifiers. For our experiments, we choose to use the efficient interval arithmetic approach (first applied in the context of neural network verification by Xiang et al. (2018)). Below we describe a version of the method that incorporates information about partial regions:

X0 := Bp,U(x),

Zi := W i 1Xi 1 + bi 1 for i [L + 1],

Xi := relu(Box Ai(Zi)) for i [L],

where Box Ai(Zi) is the set of vectors v satisfying

min w Zi wj vj max w Zi wj if Ai(j) = +1,

vj = 0 if Ai(j) = 1.

We can use the fact that f(Bp,U(x) RA) ZL+1 to check if we need to explore the descendants of A.

Warm starts via restricting search area. Certain incomplete verifiers implicitly generate enough information to allow us to efficiently compute a convex set M that contains

Figure 5. Computing a set that contains the decision boundary and warm starting. The red shaded region corresponds to the region that contains any potential decision boundary. By identifying this region, we can warm start the algorithm by initializing the search at the closest point in the red region.

the decision boundary. We will describe how to do this for verifiers based on simple linear underestimates of fy fy in the ball Bp,U(x) such as Fast-Lin (Weng et al., 2018) and CROWN (Zhang et al., 2018). These methods construct a linear function g fy fy by propagating linear and upper bounds of the Re LUs through the layers. The resulting set {v | g(v) 0} is a halfspace that we can efficiently project onto. Figure 5 illustrates this concept. For the purposes of this paper we use the lower bound from the CROWN verifier (Zhang et al., 2018) to compute a halfspace M.

Once we have computed M, we can use it throughout our algorithm. In particular, if a face does not overlap with M, we can remove it from consideration in our algorithm. We discuss this in more detail in the appendix.

Instead of just using linear approximations, we can also use tighter approximations such as the linear programming relaxation that models single Re LUs tightly (see for example Salman et al. (2019)) These result in a smaller convex set M that is still guaranteed to contain the decision boundary but overlaps with less regions, resulting in a reduction in the search space. The drawback of using such methods is that the representation of M can get significantly more complicated, which in turn increases the cost of solving Problems (7) and (9).

6. Experimental Evaluation

We use an experimental setup similar to the one used in Jordan et al. (2019). The two experiments presented here are taken directly from them, except for an additional neural network in the first and a larger neural network in the second. Additional results are presented in the appendix.

We consider a superset of the networks used in Geo Cert. The fully connected Re LU networks we use in the paper have two to five hidden layers, with between 10 to 50 neurons in each layer. As with Jordan et al. (2019), we train our

Hierarchical Verification for Adversarial Robustness

Table 1. Average number of convex programs and running time over 100 inputs for 12 different networks for ℓ -distance. The green shaded entries indicate the best performing method for each neural network under each metric. The gray shaded entries indicates the algorithm timed out before an exact solution to Problem (1) could be found for at least one input. Whenever a timeout occurs, we use a time of 1800 seconds in its place, which leads to an underestimate of the true time.

networks to classify the digits 1 and 7 in the MNIST dataset and used the same training parameters. We consider ℓ distance here and also ℓ2 distance in the appendix.

Methods evaluated. We test the following variants of Geo Cert and Layer Cert. All variants of Layer Cert use an ℓp distance priority function.

Geo Cert with ℓp distance priority function.

Geo Cert-Lip: Geo Cert with x v p + miny =j fy(v) fj(v)

L priority function, where L denotes an upper bound on the Lipschitz constant found by the Fast-Lip method (Weng et al., 2018).

Layer Cert-Basic.

Layer Cert with interval arithmetic pruning.

Layer Cert with warmstart in the initial iteration using CROWN (Zhang et al., 2018) to underestimate fy fj.

Layer Cert-Both: with both interval arithmetic pruning and CROWN-based warm start.

We initialize each algorithm with a target verification radius of 0.3. Each method terminates when we have exactly computed the answer to (1) or when it has determined that the lower bound is at least the radius. Implementation details. Our implementation of Geo Cert (Jordan et al., 2019) starts with the original code provided by the authors at https://github.com/revbucket/ geometric-certificates and modifies it to make

use of open-source convex programming solvers to enable further research to a wider community, as the original code uses Gurobi (Gurobi Optimization, 2019), which is a commercial software. We use CVXPY (Diamond & Boyd, 2016) to model the convex programs and the open-source ECOS solver (Domahidi et al., 2013) as the main solver. Since ECOS can occasionally fail, we also use OSQP (Stellato et al., 2017) and SCS (O donoghue et al., 2016) as backup solvers. In our tests, ECOS and OSQP are significantly faster than SCS which we use only as a last resort.

We implemented Layer Cert in Python using the packages numpy, Py Torch, numba (for the lower bounding methods), and the aforementioned packages for solving convex programs. Our experiments were performed on an Ubuntu 18.04 server on an Intel Xeon Gold 6136 CPU with 12 cores. We restricted the algorithms to use only a single core and do not allow the use of the GPU. All settings, external packages, and compute are identical for all the methods compared.

6.1. Exact measurement experiments.

We randomly picked 100 1 s and 7 s from MNIST and collected the wall-clock time and number of linear programs solved. Since some instances can take a very long time to solve fully, we set a time limit of 1800s for each instance.

Averaged metrics. We measure (1) the average of the wall-clock time taken to measure the distances and (2) the average of number of linear programs solved. The first metric is what matters in practice but is heavily dependent

Hierarchical Verification for Adversarial Robustness

Figure 6. Performance profiles comparing Layer Cert-Both (orange, x markers) with Geo Cert-Lip (blue, dotted, circle markers) over 12 different networks using ℓ norm. Marks are placed for every 10 input points.

on the machine and the solver used, whereas the second metric provides a system-independent proxy for time. We present the results in Table 1. The basic Geo Cert method is consistently outperformed in both metrics by our methods, while Geo Cert-Lip always improves on Geo Cert in terms of number of LPs and often in terms of run time. The method with the fastest run time is always one of the three Layer Cert variants that use lower bounds. With the exception of the 3 [50] network where all methods timed out, the method with the least number of convex programs solved is always Layer Cert-Both. Plain Layer Cert always outperforms both Geo Cert methods in terms of timing, while it often outperforms Geo Cert-Lip in number of LPs. In some cases only one of the two lower bounding methods helps significantly, though the use of both methods at most includes a small overhead. Thus, we recommend in general using both.

Performance profiles. Performance profiles (Dolan & Mor e, 2002) are a commonly-used technique to benchmark the performance of different optimization methods over sets of instances. A performance profile is a plot of a cumulative distribution, where the x-axis denotes the amount of time each method is allowed to run for, and the y-axis the number of problems that can be solved within that time period. If the performance profile of a method is consistently above the performance profile of another method, it indicates that

the former method is always able to solve more problems regardless of the time limit. We illustrate the performance profiles for Geo Cert-Lip and Layer Cert-Both in Figure 6. Layer Cert-Both consistently dominates Geo Cert-Lip.

7. Conclusion

We have developed a novel hierarchical framework Layer Cert for exact robustness verification that leverages the nested hyperplane arrangement structure of Re LU networks. We prove that a basic version of Layer Cert is able to reduce the number and size of the convex programs over Geo Cert using the equivalent priority functions. We showed that Layer Cert is amenable to the use of lower bounding methods that use convex relaxations to both prune and warm start the algorithm. Our experiments showed that Layer Cert can significantly outperform variants of Geo Cert.

Acknowledgments

We would like to thank the anonymous reviewers for suggestions that helped greatly to improve the presentation of this work. We would also like to thank Eilyan Bitar, Ricson Cheng, and Jerry Liu for helpful discussions.

Hierarchical Verification for Adversarial Robustness

Anderson, G., Pailoor, S., Dillig, I., and Chaudhuri, S. Optimization and abstraction: a synergistic approach for analyzing neural network robustness. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pp. 731 744, Phoenix, AZ, USA, June 2019a. Association for Computing Machinery. ISBN 978-1-4503-6712-7.

Anderson, R., Huchette, J., Tjandraatmadja, C., and Vielma, J. P. Strong Mixed-Integer Programming Formulations for Trained Neural Networks. In Lodi, A. and Nagarajan, V. (eds.), Integer Programming and Combinatorial Optimization, Lecture Notes in Computer Science, pp. 27 42. Springer International Publishing, 2019b. ISBN 978-3-030-17953-3.

Balan, R., Singh, M., and Zou, D. Lipschitz properties for deep convolutional networks. ar Xiv preprint ar Xiv:1701.05217, 2017.

Bartlett, P. L., Foster, D. J., and Telgarsky, M. J. Spectrallynormalized margin bounds for neural networks. In Advances in Neural Information Processing Systems, pp. 6240 6249, 2017.

Biggio, B., Corona, I., Maiorca, D., Nelson, B., ˇSrndi c, N., Laskov, P., Giacinto, G., and Roli, F. Evasion attacks against machine learning at test time. In Joint European conference on machine learning and knowledge discovery in databases, pp. 387 402. Springer, 2013.

Boyle, J. P. and Dykstra, R. L. A Method for Finding Projections onto the Intersection of Convex Sets in Hilbert Spaces. In Dykstra, R., Robertson, T., and Wright, F. T. (eds.), Advances in Order Restricted Statistical Inference, Lecture Notes in Statistics, pp. 28 47, New York, NY, 1986. Springer. ISBN 978-1-4613-9940-7.

Bunel, R., Turkaslan, I., Torr, P. H., Kohli, P., and Kumar, M. P. A Unified View of Piecewise Linear Neural Network Verification. In Proceedings of the 32Nd International Conference on Neural Information Processing Systems, NIPS 18, pp. 4795 4804, USA, 2018. Curran Associates Inc. event-place: Montr eal, Canada.

Bunel, R., Lu, J., Turkaslan, I., Torr, P. H. S., Kohli, P., and Kumar, M. P. Branch and Bound for Piecewise Linear Neural Network Verification. ar Xiv:1909.06588 [cs, stat], November 2019. ar Xiv: 1909.06588.

Combettes, P. L. and Pesquet, J.-C. Lipschitz certificates for neural network structures driven by averaged activation operators. ar Xiv preprint ar Xiv:1903.01014, 2019.

Diamond, S. and Boyd, S. CVXPY: A Python-embedded modeling language for convex optimization. Journal of Machine Learning Research, 17(83):1 5, 2016.

Dolan, E. D. and Mor e, J. J. Benchmarking optimization software with performance profiles. Mathematical Programming, 91(2):201 213, January 2002. ISSN 14364646.

Domahidi, A., Chu, E., and Boyd, S. ECOS: An SOCP solver for embedded systems. In European Control Conference (ECC), pp. 3071 3076, 2013.

Dvijotham, K., Stanforth, R., Gowal, S., Mann, T., and Kohli, P. A dual approach to scalable verification of deep networks. In Proceedings of the Thirty-Fourth Conference Annual Conference on Uncertainty in Artificial Intelligence (UAI-18), pp. 162 171, Corvallis, Oregon, 2018. AUAI Press.

Fazlyab, M., Robey, A., Hassani, H., Morari, M., and Pappas, G. J. Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks. ar Xiv:1906.04893 [cs, math, stat], June 2019. ar Xiv: 1906.04893.

Goodfellow, I. J., Shlens, J., and Szegedy, C. Explaining and harnessing adversarial examples. ar Xiv preprint ar Xiv:1412.6572, 2014.

Gurobi Optimization, L. Gurobi optimizer reference manual, 2019. URL http://www.gurobi.com.

Hanin, B. and Rolnick, D. Deep relu networks have surprisingly few activation patterns. In Wallach, H., Larochelle, H., Beygelzimer, A., d Alch e Buc, F., Fox, E., and Garnett, R. (eds.), Advances in Neural Information Processing Systems 32, pp. 359 368. Curran Associates, Inc., 2019.

Jordan, M., Lewis, J., and Dimakis, A. G. Provable Certificates for Adversarial Examples: Fitting a Ball in the Union of Polytopes. In Wallach, H., Larochelle, H., Beygelzimer, A., Alch e-Buc, F. d., Fox, E., and Garnett, R. (eds.), Advances in Neural Information Processing Systems 32, pp. 14059 14069. Curran Associates, Inc., 2019.

Katz, G., Barrett, C., Dill, D. L., Julian, K., and Kochenderfer, M. J. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Majumdar, R. and Kunˇcak, V. (eds.), Computer Aided Verification, Lecture Notes in Computer Science, pp. 97 117, Cham, 2017. Springer International Publishing. ISBN 978-3-319-63387-9.

Lu, J. and Kumar, M. P. Neural Network Branching for Neural Network Verification. In International Conference on Learning Representations, 2020.

O donoghue, B., Chu, E., Parikh, N., and Boyd, S. Conic optimization via operator splitting and homogeneous selfdual embedding. Journal of Optimization Theory and Applications, 169(3):1042 1068, 2016.

Hierarchical Verification for Adversarial Robustness

Salman, H., Yang, G., Zhang, H., Hsieh, C.-J., and Zhang, P. A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks. In Wallach, H., Larochelle, H., Beygelzimer, A., Alch e-Buc, F. d., Fox, E., and Garnett, R. (eds.), Advances in Neural Information Processing Systems 32, pp. 9832 9842. Curran Associates, Inc., 2019.

Serra, T., Tjandraatmadja, C., and Ramalingam, S. Bounding and Counting Linear Regions of Deep Neural Networks. In Dy, J. and Krause, A. (eds.), Proceedings of the 35th International Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Research, pp. 4558 4566, Stockholmsm assan, Stockholm Sweden, July 2018. PMLR.

Singh, G., Gehr, T., Mirman, M., P uschel, M., and Vechev, M. Fast and Effective Robustness Certification. In Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa Bianchi, N., and Garnett, R. (eds.), Advances in Neural Information Processing Systems 31, pp. 10802 10813. Curran Associates, Inc., 2018.

Singh, G., Ganvir, R., P uschel, M., and Vechev, M. Beyond the Single Neuron Convex Barrier for Neural Network Certification. In Wallach, H., Larochelle, H., Beygelzimer, A., Alch e-Buc, F. d., Fox, E., and Garnett, R. (eds.), Advances in Neural Information Processing Systems 32, pp. 15072 15083. Curran Associates, Inc., 2019a.

Singh, G., Gehr, T., P uschel, M., and Vechev, M. An Abstract Domain for Certifying Neural Networks. Proc. ACM Program. Lang., 3(POPL):41:1 41:30, January 2019b. ISSN 2475-1421.

Stellato, B., Banjac, G., Goulart, P., Bemporad, A., and Boyd, S. OSQP: An operator splitting solver for quadratic programs. Ar Xiv e-prints, November 2017.

Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., and Fergus, R. Intriguing properties of neural networks. ar Xiv preprint ar Xiv:1312.6199, 2013.

Tjeng, V., Xiao, K. Y., and Tedrake, R. Evaluating Robustness of Neural Networks with Mixed Integer Programming. In International Conference on Learning Representations, 2019.

Wang, S., Pei, K., Whitehouse, J., Yang, J., and Jana, S. Formal Security Analysis of Neural Networks using Symbolic Intervals. In 27th USENIX Security Symposium (USENIX Security 18), pp. 1599 1614, Baltimore, MD, August 2018. USENIX Association. ISBN 978-1-93913304-5.

Weng, L., Zhang, H., Chen, H., Song, Z., Hsieh, C.-J., Daniel, L., Boning, D., and Dhillon, I. Towards Fast

Computation of Certified Robustness for Re LU Networks. In International Conference on Machine Learning, pp. 5276 5285, July 2018.

Wong, E. and Kolter, Z. Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. In International Conference on Machine Learning, pp. 5286 5295, July 2018.

Xiang, W., Tran, H.-D., and Johnson, T. T. Output Reachable Set Estimation and Verification for Multilayer Neural Networks. IEEE Transactions on Neural Networks and Learning Systems, 29(11):5777 5783, November 2018. ISSN 2162-2388.

Zhang, H., Weng, T.-W., Chen, P.-Y., Hsieh, C.-J., and Daniel, L. Efficient Neural Network Robustness Certification with General Activation Functions. In Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., and Garnett, R. (eds.), Advances in Neural Information Processing Systems 31, pp. 4939 4948. Curran Associates, Inc., 2018.

Zou, D., Balan, R., and Singh, M. On lipschitz bounds of general convolutional neural networks. IEEE Transactions on Information Theory, 2019.