Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for the Hamming Distance

1 Introduction

Safety certification for DNNs is challenging owing to the lack of symbolic models and formal specifications. An important requirement specification for DNNs is their robustness to input perturbations. DNNs have been shown to suffer from poor robustness because of their susceptibility to adversarial examples [Szegedy et al., 2014; Biggio et al., 2013]. These are small modifications to an input, sometimes imperceptible to humans, that make the neural network unstable. As a result, significant effort has been directed towards approaches for crafting adversarial examples [Goodfellow et al., 2015; Papernot et al., 2016; Carlini and Wagner, 2017]. However, these provide no formal guarantees, i.e., no conclusion can be drawn on whether adversarial examples remain.

By contrast, recent efforts in the area of automated verification, e.g.,[Huang et al., 2017; Katz et al., 2017; Lomuscio and Maganti, 2017; Narodytska et al., 2017; Dutta et al., 2017;

Ruan et al., 2018a; Wu et al., 2018; Gehr et al., 2018; Mirman et al., 2018], have focused on methods that generate adversarial examples, if they exist, and provide rigorous local robustness proofs otherwise. This paper proposes a novel approach to quantify the robustness of DNNs that offers a balance between the guaranteed accuracy of the method (thus, a feature so far exclusive to formal approaches) and the computational efficiency of algorithms that search for adversarial examples (without providing any guarantees).

We focus on the Hamming distance (i.e., the L0 norm), which measures the number of different vector components given two inputs. In the case of images, this is the number of pixels that are different. On the other hand, L1, L2 and L∞ norms compare how much each pixel has changed. The L0 distance is fast to compute and is an upper bound on the size of an adversarial perturbation [Papernot et al., 2016; Carlini et al., 2017]. However, the non-continuity and non-differentiability of L0 is a challenge for the discovery of adversarial attacks. Furthermore, the existing safety verification methods that are designed for other distance metrics are not efficient when using the Hamming distance. This includes SMT/SAT-based methods [Katz et al., 2017], MILP-based work [Dutta et al., 2017], exhaustive search or MCTS-based methods [Huang et al., 2017; Wu et al., 2018], and methods based on abstract interpretation [Gehr et al., 2018]. We remark that, while all Lp norms can be used to identify physical adversarial attacks and have a role to play, on their own or in combination, we hypothesise that the Hamming distance is a good proxy for a particular category of realistic physical attacks in which small modifications (e.g., a sticker) are applied to objects that the system is trained to recognise (e.g., a street sign), leaving the rest of the image unchanged.

In this paper we consider the global robustness problem, defined as the expected maximum safe radius over a (finite) test dataset, which is a generalisation of the local, pointwise robustness problem. The key idea of our approach is to generate sequences of lower and upper bounds for global robustness simultaneously for a set of inputs by using tensor-based parallelisation. Thus, global robustness aims to capture the worst case local robustness (worst case maximal safety radius) among a set of inputs. The usefulness of global robustness lies in that it quantifies the size of the perturbation that the system can withstand for a set of inputs, instead of just a single input, since it gives both lower and upper bounds on the maximal safe radius. Intuitively, a lower bound x means that no adversarial example is possible for perturbation of up to x pixel changes, whereas an upper bound x means that x pixel changes are sufficient to attack a network. By considering a distribution over the set of inputs, we can quantify the robustness of a DNN for this input distribution. Our definition is thus a natural extension of the robustness concept of [Peck et al., 2017].

Our method is anytime, tensor-based, and offers provable guarantees. First, the method is anytime in the sense that it can return intermediate results, including upper and lower bounds and robustness estimates. We prove that our approach can gradually, but strictly, improve these bounds and estimates as the computation proceeds. Second, it is tensor-based. As we are working with a set of inputs, a straightforward approach is to perform robustness evaluation for the inputs individually and to then merge the results. However, this is inefficient, as the set of inputs is large. To exploit the parallelism offered by GPUs, our approach uses tensors. A tensor can formulate a finite set of inputs (e.g., images) into a multi-dimensional array which can be efficiently processed by GPUs in parallel. An algorithm that is well-suited for GPUs uses tensor operations whenever possible. Third, our approach offers provable guarantees. We show that the intermediate bounds and robustness estimates converge to optimal values in finite time. Our experimental results suggest that the algorithm converges quickly in practice.

We implement our approach in a tool we name DeepTRE 1 ("Tensor-based Robustness Evaluation for Deep Neural Networks"), and present experiments via five case studies, including global robustness evaluation; competitive L0 attacks; saliency map generation for model interpretability and local robustness evaluation on ImageNet DNNs including AlexNet, VGG-16/19 and ResNet-50/101; guidance to the design of robust DNN architectures; and test case generation. All applications above require only simple adaptations of our method, e.g., slight modifications of the constraints or objective functions, or adding further constraints. This demonstrates that our tool is flexible enough to deliver a wide range of promising applications.

Owing to space limitations, we focus on describing the core theoretical concepts, tensor-based parallelization and convergence guarantees, and make an extended companion paper available as [Ruan et al., 2018b].

2 ProblemFormulation

Let f : Rn → Rm be an N-layer neural network such that, for a given input x ∈ Rn , f(x) = (c1(x), . . . , cm(x)) ∈ Rm represents the confidence values for m classification labels.

Without loss of generality, we normalise the input to x ∈ [0, 1]n . The output f(x) is usually normalised to be in [0, 1]m using a softmax layer. We denote the classification label of input x by cl(f, x) = argmaxj=1,...,m cj(x). Note that both f and cl can be generalised to apply to a set T0 of inputs, i.e., f(T0) and cl(f, T0), in the standard way.

Definition 1 (Maximum Radius of a Safe Norm Ball) Given a network f : Rn → Rm, a distance metric || · ||D, an input x0 ∈ Rn and a real number d ∈ R, a norm ball B(f, x0, || · ||D, d) is a subspace of Rn such that B(f, x0, || · ||D, d) = {x | ||x0 - x||D ≤ d}. The number d is called the radius of B(f, x0, || · ||D, d). A norm ball B(f, x0, || · ||D, d) is safe if for all x ∈ B(f, x0, || · ||D, d) we have cl(f, x) = cl(f, x0). Furthermore, if for all d′ > d we have that B(f, x0, || · ||D, d′ ) is not safe, then d is called the maximum safe radius, and denoted by dm(f, x0, || · ||D).

1 Available on GitHub: https://github.com/TrustAI/L0-TRE.

Intuitively, a norm ball B(f, x0, || · ||D, d) includes all inputs whose distance to x0, measured by || · ||D, is within d.

We define the (global) robustness evaluation problem over a test dataset T, which is a set of i.i.d. inputs sampled from a distribution µ representing the problem f is working on. We use |T| to denote the number of inputs in T. When |T| = 1, we call it local robustness.

Definition 2 (Robustness Evaluation) Given a network f, a finite set T0 of inputs, and || · ||D, robustness evaluation, denoted as R(f, T0, || · ||D), is an optimisation problem:

Intuitively, we aim to find a minimum distance between the original set T0 and a new, homogeneous set 2 T of inputs such that all inputs in T0 are mis-classified.

L0 Norm The distance metric || · ||D can be any mapping || · ||D : Rn ×Rn → [0,∞] that satisfies the metric conditions. In this paper, we focus on the L0 norm 3 . For two inputs x0 and x, their L0 distance, denoted as ||x-x0||0, is the number of their components that are different. When working with a test dataset T0 (all inputs in T0 are i.i.d.), we define

where x ∈ T is a homogeneous input to x0 ∈ T0. While other norms such as L1, L2 and L∞ have been widely applied for generating adversarial examples [Papernot et al., 2016; Kurakin et al., 2016], studies of robustness evaluation for DNNs based on the L0 norm are few and far between [Papernot et al., 2016; Carlini et al., 2017; Wicker et al., 2018; Huang et al., 2017; Wu et al., 2018]. In Appendix B of [Ruan et al., 2018b], we discuss why L0 is an important distance metric from various perspectives.

3 Anytime Robustness Evaluation

The evaluation of robustness following Definition 2 is hard for the L0-norm. In Appendix A.1 of [Ruan et al., 2018b], we discuss its computational complexity and prove that the problem is NP-hard. We propose to compute lower and upper bounds on robustness, and then gradually, but strictly, improve the bounds so that the gap between them can eventually be closed. Although in practice run times can be long, this anytime approach provides pragmatic means to make progress. Section 5 shows that our approach achieves tight bounds efficiently on difficult instances.

2 Two sets T0 and T are homogeneous if they have the same number of elements and are of the same type.

3 Strictly speaking, L0 is not a norm, but it is commonly referred to as such.

Definition 3 (Sequences of Bounds) Given a robustness evaluation problem R(f, T0, || · ||D), a sequence L(T0) = {l1, l2, . . . , lk} ∈ R is an incremental lower bound sequence if, for all 1 ≤ i < j ≤ k, we have li ≤ lj ≤ R(f, T0, ||·||D). The sequence is strict, denoted as Ls(T0), if for all 1 ≤ i < j ≤ k, we have either li < lj or li = lj = R(f, T0, || · ||D). Similarly, we can define a decremental upper bound sequence U(T0) and a strict decremental upper bound sequence Us(T0).

We will, in Section 4, introduce our algorithms for computing these two sequences of lower and upper bounds. For now, assume they exist, then at a certain time t > 0,

holds.

Definition 4 (Anytime Robustness Evaluation) Based on two given bounds [lt, ut], we define its centre and radius as follows.

The anytime evaluation of R(f, T0, || · ||D) at time t, denoted as Rt(f, T0, || · ||D), is the pair (Uc(lt, ut), Ur(lt, ut)).

The anytime evaluation will be returned whenever the computational procedure is interrupted. Intuitively, we use the centre Uc(lt, ut) to represent the current estimate, and the radius Ur(lt, ut) to represent its error bound. Essentially, we can bound the true robustness R(f, T0, || · ||D) via the anytime robustness evaluation.

4 Tensor-based Algorithms for Upper and Lower Bounds

We present our approach to generate the sequence of bounds. For both the lower bounds and the upper bounds, we need the following definition.

Definition 5 (Complete Set of Subspaces for an Input)

Given an input x0 ∈ [0, 1]n and a set of t dimensions T ⊆ {1, ..., n} such that |T| = t, the subspace for x0, denoted by Xx0,T , is a set of inputs x ∈ [0, 1]n such that x(i) ∈ [0, 1] for i ∈ T and x(i) = x0(i) for i ∈ {1, ..., n}\T . Furthermore, given an input x0 ∈ [0, 1]n and a number t ≤ n, we define

as the complete set of subspaces for input x0.

Intuitively, elements in Xx0,T share the same value with x0 on the dimensions other than T , and may take any legal value for the dimensions in T . Moreover, X(x0, t) includes all sets Xx0,T for any possible combination T with t dimensions.

Next, we define the subspace sensitivity for a subspace w.r.t. a neural network f, an input x0 and a test dataset T0. Recall that f(x) = (c1(x), . . . , cm(x)).

Definition 6 (Subspace Sensitivity) Given an input subspace X ⊆ [0, 1]n , an input x0 ∈ [0, 1]n and a label j, the subspace sensitivity w.r.t. X, x0, and j is defined as

Let t be an integer. We define the subspace sensitivity for T0

where jx0 = argmaxi∈{1,...,m} ci(x0) is the classification label of x0 by network f.

Intuitively, S(X, x0, j) is the maximal decrease of confidence value of the output label j that can be witnessed from the set X, and S(T0, t) is the two-dimensional array of the maximal decreases of confidence values of the classification labels for all subspaces in X(x0, t) and all inputs in T0. It is not hard to see that S(X, x0, j) ≥ 0.

Given a test dataset T0 and an integer t > 0, the number of elements in S(T0, t) is in O(|T0| · nt ), i.e., polynomial in |T0| and exponential in t. Note that, by Equation (6), every element in S(T0, t) represents an optimisation problem. That is, for T0, a set of 20 MNIST images, and t = 1, this would be 28 × 28 × 20 = 15,680 one-dimensional optimisation problems. In the next section, we give a tensor-based formulation and an algorithm to solve this challenging problem via GPU parallelisation.

4.1 Tensor-based Parallelisation for Computing Subspace Sensitivity

A tensor T ∈ RI1×I2×...×IN in an N-dimensional space is a mathematical object that has ∏Nm=1 Im components and obeys certain transformation rules. Intuitively, tensors are generalisations of vectors (i.e., one index) and matrices (i.e., two indices) to an arbitrary number of indices. Many state-of-theart deep learning libraries, such as Tensorflow and pyTorch, are utilising tensors to parallelise the computation with GPUs. However, it is nontrivial to write an algorithm working with tensors owing to the limited set of operations on tensors.

The basic idea of our algorithm is to transform a set of nonlinear, non-convex optimisation problems as given in Equation (7) into a tensor formulation, and solve a set of optimisation problems via a few DNN queries. First, we introduce the following operations on tensors that are used in our algorithm.

Definition 7 (Mode-n Unfolding and Folding) Given a tensor T ∈ RI1×I2×...×IN , the mode-n unfolding of T is a matrix U[n](T ) ∈ RIn×IM such that M = ∏Nk=1,k̸=n Ik and U[n](T ) is defined by the mapping from element (i1, . . . , iN) to (in, j), with

Similarly, the tensor folding F folds an unfolded tensor back from a matrix into a full tensor. Tensor unfolding and folding are dual operations and link tensors and matrices.

Given a neural network f, a number t and a test dataset T0, each xi ∈ T0 generates a complete set X(xi, t) of subspaces. Let |T0| = p and |X(xi, t)| = k. Note that, for different xi and xj, we have |X(xi, t)| = |X(xj, t)|. Given an error tolerance ϵ > 0, by applying grid search, we can recursively sample ∆ = 1/ϵ numbers in each dimension, and turn each subspace Xxi ∈ X(xi, t) into a two-dimensional grid G(Xxi ) ∈ Rn×∆t . We thus can formulate the following tensor:

In Appendix A.2 of [Ruan et al., 2018b], we show that grid search provides the guarantee of reaching the global minimum by utilising the Lipschitz continuity in DNNs.

Then, we apply the mode-1 tensor unfolding operation to have T[1](T (T0, t)) ∈ Rn×M such that M = ∆t · p · k. Then this tensor can be fed into the DNN f to obtain

After computing Y (T0, t), we apply a tensor folding opera-

Here, we should note the difference between R∆t ·p·k and R∆t×p×k , with the former being a one-dimensional array and the latter a tensor. On Y(T0, t), we search the minimum values along the first dimension to obtain 4

Thus, we have now solved all p × k optimisation problems. We then construct the tensor

from the set T0. Recall that jxi = argmaxk∈{1,...,m} ck(xi). Intuitively, V (T0, t) is the tensor that contains the starting points of the optimisation problems and V (T0, t)min the resulting optimal values. The following theorem shows the correctness of our computation, where S(T0, t) has been defined in Definition 6.

Theorem 1 Let T0 be a test dataset and t an integer. We have S(T0, t) = V (T0, t) - V (T0, t)min.

We remark that we only need a single DNN query in Equation (10) to perform the computation above.

4.2 Tensor-based Parallelisation for Computing Lower and Upper Bounds

Let S(T0, t) ∈ Rn×p×k be the tensor obtained by replacing every element in S(T0, t) by its corresponding input that, according to the computation of V (T0, t)min, causes the largest decreases of the confidence values of the classification labels. We call S(T0, t) the solution tensor of S(T0, t). The computation of S(T0, t) can be done using very few tensor operations over T (T0, t) and Y(T0, t), which have been given in Section 4.1. We omit the details.

4 Here we use the Matlab notation min(Y, k), which computes the minimum values over the k-th dimension for a multi-dimensional array Y . We use similar notation in the remainder of the paper.

Lower Bounds

We reorder S(T0, t) and S(T0, t) w.r.t. decreasing values in S(T0, t). Then, we retrieve the first row of the third dimension in tensor S(T0, t), i.e., S(T0, t)[:, :, 1] ∈ Rn×p , and check whether cl(f, S(T0, t)[:, :, 1]) = cl(f, T0). The result is an array of Boolean values, each of which is associated with an input xi ∈ T0. If any element associated with xi in the resulting array is false, we conclude that dm(f, xi, || · ||D) = t - 1, i.e., the maximum safe radius has been obtained and the computation for xi has converged. On the other hand, if the element associated with xi is true, we update the lower bound for xi to t. After computing S(T0, t), no further DNN query is needed to compute the lower bounds.

Upper Bounds

The upper bounds are computed by iteratively applying perturbations based on the matrix S(T0, t) for every input in T0 until a misclassification occurs. However, doing this sequentially for all inputs would be inefficient, since we need to query the network f after every perturbation on each image.

We present an efficient tensor-based algorithm, which enables GPU parallelisation. The key idea is to construct a new tensor N ∈ Rn×p×k to maintain all the accumulated perturbations over the original inputs T.

• Initialisation: N[:, :, 1] = S(T0, t)[:, :, 1].
• Iteratively construct the i-th row until i = k:

where ⊟, ⋒, and ⋓ are tensor operations: N1 ⊟N2 removes the corresponding non-zero elements in N2 fromN1; further, N1 ⋒ N2 retains those elements that have the same values and sets the other elements to 0; finally, N1 ⋓ N2 merges the non-zero elements from two tensors. The two operands of these operations are required to have the same type. Intuitively, N[:, :, i] represents the result of applying the first i perturbations recorded in S(T0, t)[:, :, 1 : i], which contains the perturbations up to index i - 1 (i.e., N:,i,:) plus the new perturbation recorded in ˜ X:,i,: .

Subsequently, we unfold N and pass the result to the DNN f , which yields the classification labels Y (U[1](N)) ∈ {1, . . . ,m}p·k . After that, a tensor folding operation is applied to obtain Y(U[1](N)) ∈ {1, . . . ,m}p×k . Then we do the tensor folding operation to obtain C = fold(Yc) ∈ RK×P . Finally, we can compute the minimum column index along each row such that a misclassification occurs, denoted by {m1, ...,mp} such that 1 ≤ mi ≤ k. Then we let

which is the optimal set of inputs as required in Definition 2.

After computing S(T0, t), we only need one further DNN query to obtain all upper bounds for a given test dataset T0.

Tightening the Upper Bounds

There may be redundancies in T-T0, i.e., not all the changes in T - T0 are necessary to observe a misclassification. We therefore remove the redundancies and thereby tighten the upper bounds. We reduce the tightening problem to an optimisation problem similar to that of Definition 2, which enables us to reuse the tensor-based algorithms given above. Assume that x0,i and xi are two corresponding inputs in T and T0, respectively, for i ∈ {1, . . . , |T0|}. By abuse of notation, we let z0,i = x0,i - xi be the part of x0,i on which x0,i and xi are different, and l0,i = xi ⋒ x0,i be the part of x0,i on which x0,1 and xi are the same. Therefore, x0,i = z0,i ⋓ l0,i.

Figure 2: Robustness evaluation of DNN-0 for t ∈ {1, 2} and box-plots of computation time.

Definition 8 (Tightening the Upper Bounds) Given a network f, a finite test dataset T0 with their upper bounds T, and || · ||D, the tightening problem is an optimisation problem:

where i ∈ {1, . . . , |L0|}, L0 = (l0,i)i=1...|T0|, L1 = (l1,i)i=1...|L0|, and l1,i, l0,i ∈ [0, 1]|L0| . To solve this optimisation problem, we can re-use the tensor-based algorithm for computing lower bounds with minor modifications to the DNN query: before querying the DNN, we apply the ⋓ operation to merge with z0,i as in the above equation. Owing to space limitations, we provide the convergence analysis in Appendix A.2 of [Ruan et al., 2018b].

5 Experimental Results

We report experimental evidence for the utility of our algorithm. Some experiments require simple modifications of the optimisation problem given in Definition 2, e.g., small changes to the constraints. No significant modification to our algorithm is needed to process these variants. In this section, we use five case studies to demonstrate the broad applicability of our tool.

5.1 Convergence Analysis and Global Robustness Evaluation

We study the convergence and running time of our anytime global robustness evaluation algorithm on several DNNs in terms of the L0-norm. To the best of our knowledge, no baseline method exists for this case study. Adversarial attack algorithms for the L0 norm, which we compare against in Section 5.2, cannot perform robustness evaluation based on both lower and upper bounds with provable guarantees.

We train two DNNs on the MNIST dataset. DNN-0 is trained on the original images with size 28 × 28 and sDNN on images resized to 14 × 14. The latter is less robust and used here for the purpose of discussing the convergence of our method. The DNN models are given in Appendix D of [Ruan et al., 2018b], together with training and accuracy statistics. For DNN-0, we work with a set of 2,400 randomly sampled images, and for sDNN we use a set of 5,300 images. We perform the computation on a PC with I7-7700HQ CPU, 16 GB of RAM and NVIDIA GTX-1050Ti GPU.

sDNN: Convergence and Robustness Evaluation

Figure 1 (Left) illustrates the speed of convergence of lower and upper bounds and the estimate for dm (i.e., the maximum safe radius) for an image with a large initial upper bound at L0 distance 27. This image is chosen to demonstrate the worst case for our approach. Working with a single image (i.e., local robustness) is the special case of our optimisation problem where |T| = 1. We choose one of the worst examples among our dataset since the initial upper bound computed is very large: The L0 distance to the original image is 27. We observe that, when transitioning from t = 1 to t = 2, the uncertainty radius Ur(lt, ut) of dm is reduced significantly from 26 to 1. Figure 1 (Middle) illustrates the speed of convergence of the global robustness evaluation on the test dataset: our method obtains tight lower and upper bounds efficiently and converges quickly. Notably, we have Uc(lt, ut) = 1.97 at t = 1; the final global robustness is 2.1, so the relative error of the global robustness at t = 1 is < 7%. The estimate at t = 1 can be obtained in polynomial time, and thus the results demonstrate that our approach is able to provide a good approximation with reasonable error at very low computational cost. Figure 1 (Right) gives the box-plots of the computational time required for individual iterations (i.e., subspace dimension t). We remark that at t = 1 it takes less than 0.1 s to process one image, which suggests that the algorithm has potential for real-time applications.

Figure 3 shows the upper and lower bounds as well as the estimate for dm for all tested images. The images are ordered using their upper bounds at t = 1. The dashed blue line indicates that all images to the left of this line have converged. The charts show a clear overall trend: our algorithm converges for most images after a few iterations.

DNN-0: Global Robustness Evaluation

Figure 4 illustrates the convergence trends for all 2,400 images for a large DNN. We observe that, even for a DNN with tens of thousands of hidden neurons, DeepTRE still achieves tight estimates for dm for most images. Figure 2 gives the results of anytime global robustness evaluation at t = 1 and t = 2 for DNN-0, which demonstrates the efficiency of our approach for anytime global robustness evaluation on DNNs. Figure 14 in Appendix D of [Ruan et al., 2018b] features some ground-truth adversarial images 5 returned by our upper bound algorithm.

5.2 Competitive L0 Attacks

While the generation of attacks is not the primary goal of our method, we observe that our upper bound generation method is highly competitive with state-of-the-art methods for the computation of adversarial images in terms of the L0 distance. We train MNIST and CIFAR-10 DNNs and compare with JSMA [Papernot et al., 2016], C&W [Carlini and Wagner, 2017], DLV [Huang et al., 2017], SafeCV [Wicker et al.,

5 Ground-truth adversarial images are images at the boundary of a safe norm ball, which was proposed in [Carlini et al., 2017].

2018] and DeepGame [Wu et al., 2018], on 1,000 test images. Details of the experimental setup are given in Appendix E of [Ruan et al., 2018b].

Adversarial L0 Distance

Figure 5 depicts the average and standard deviations of L0 distances of the adversarial images produced by the five methods. A smaller L0 distance indicates an adversarial example closer to the original image. For MNIST, the performance of our method is better than JSMA, DLV, and SafeCV, and comparable to C&W and DeepGame. For CIFAR-10, the bar chart reveals that our tool DeepTRE achieves the smallest L0 distance (modifying 2.62 pixels on average) among all competitors. For this experiment, we stop at t = 1 without performing further iterations.

Computational Cost

Figure 6 (note in log-scale) gives running times. Our tensorbased parallelisation delivers extremely efficient attacks. For example, for MNIST, our method is 18×, 100×, 1050×, and 357× faster than JSMA, C&W, DLV, and SafeCV, respectively. Figure 7 shows that the tensor-based parallelisation significantly improves the computational efficiency: 38 times faster on MNIST DNN and 93 times faster on CIFAR-10 DNN 6 . Appendix E of [Ruan et al., 2018b] compares some of the adversarial examples found by the five methods. The examples illustrate that the modification of 1 to 3 pixels suffices to trigger misclassification of well-trained neural networks.

5.3 Local Robustness Evaluation for ImageNet

We apply our method to five state-of-the-art ImageNet DNN models, including AlexNet (8 layers), VGG-16 (16 layers), VGG-19 (19 layers), ResNet50 (50 layers), and ResNet101 (101 layers). We set t = 1 and generate the lower/upper bounds and estimates of local robustness for an input image. Figure 9 gives the local robustness estimates and their bounds for these networks. The adversarial images on the upper boundaries are featured in the top row of Figure 8. For AlexNet, on this specific image, DeepTRE is able to find its ground-truth adversarial example (local robustness converges at L0 = 2). We also observe that, for this image, the most robust model is VGG-16 (local robustness = 15) and the most vulnerable one is AlexNet (local robustness = 2). Figure 9 also reveals that, for similar network structures such as VGG-16 and VGG-19, ResNet50 and ResNet101, a model with deeper layers is less robust to adversarial perturbations.

As a byproduct, our method can also generate a saliency map for each input image as shown by the bottom row of Figure 8. Details of the experimental setup are given in Appendix F of [Ruan et al., 2018b].

5.4 Guiding the Design of Robust DNN Architectures

In this case study, we show how to use our tool DeepTRE for guiding the design of robust DNN architectures.

6 The hardware setups are as follows. CPU-1: Tensorflow on i5-4690S CPU; GPU-1: Tensorflow with parallelisation on NVIDIA GTX TITAN GPU. CPU-2: Deep Learning Toolbox (Matlab2018b) on an i7-7700HQ CPU; GPU-2: Deep Learning Toolbox (Matlab2018b) with parallelisation on NVIDIA GTX-1050Ti GPU.

We trained seven DNNs, named DNN-i for i ∈ {1, . . . , 7}, on the MNIST dataset using the same hardware and software platform and identical training parameters. The DNNs differ in their architecture, i.e., the number of layers and the types of the layers. The architecture matters: while all DNNs achieve 100% accuracy during training, we observe accuracy down to 97.75% on the test dataset. Details of the models are in Appendix G of [Ruan et al., 2018b]. We aim to identify architectural choices that affect robustness.

Figure 10 gives the estimates for global robustness, and their upper and lower bounds at t = 1 and t = 2 for all seven DNNs. Figure 11 illustrates the means and standard deviations of the dm estimates and the uncertainty radius for all 1,000 sampled testing images. We also find that the local robustness (i.e., robustness evaluated on a single image) of a network is coincident with its global robustness, and so is the uncertainty radius.

We observe the following: i) number of layers: a very deep DNN (i.e., too many layers relative to the size of the training dataset) is less robust, such as DNN-7; ii) convolutional layers: DNNs with large numbers of convolutional layers are less robust, e.g., compared with DNN-5, DNN-6 has an additional convolutional layer, but is significantly less robust; iii) batchnormalisation layers: adding a batch-normalisation layer may improve robustness, e.g., DNN-3 is more robust than DNN-2.

We remark that accuracy measured on a test dataset is not a good proxy for robustness: a DNN with higher accuracy is not necessarily more robust, e.g., DNN-1 and DNN-3 are more robust than DNN-6 and DNN-7, which have higher accuracy.

DNNs may require a balance between robustness and their ability to generalise (proxied by testing accuracy) [Tsipras et al., 2018]. DNN-4 is a good example, among our limited set.

Therefore, our tool DeepTRE can be used to perform model selection, given two neural networks with similar accuracy, or to find a model that offers a good balance between robustness and performance.

5.5 Test Case Generation for DNNs

A variety of methods to automate testing of DNNs have been proposed recently [Pei et al., 2017; Sun et al., 2018]. The most widely used metric for the exhaustiveness of test suites for DNNs is neuron coverage [Pei et al., 2017]. Neuron coverage quantifies the percentage of hidden neurons in the network that are activated at least once. We use ne to range over hidden neurons, and V (ne, x) to denote the activation value of ne for test input x. Then V (ne, x) > 0 implies that ne is covered by the test input x.

The application of our algorithm to coverage-driven test case generation is straightforward; it only requires a minor modification to the optimisation problem in Definition 2. Given any neuron ne that is not activated by the test suite T0, we find the input with the smallest distance to any input in T0 that activates ne. We replace the constraint cl(f, xi) ̸= cl(f, x0,i) in Equation 1 by

The optimisation problem now searches for new inputs that activate the neuron ne, and the objective is to minimise the distance from the current set of test inputs T0.

We compare our tool DeepTRE with other state-of-the-art test case generation methods, including DeepConcolic [Sun et al., 2018] and DeepXplore [Pei et al., 2017]. All results are averaged over 10 runs or more. Table 1 gives the neuron coverage obtained by the three tools. We observe that DeepTRE

yields much higher neuron coverage than both DeepConcolic and DeepXplore in any of its three modes of operation ('light', 'occlusion', and 'blackout'). Figure 12 depicts adversarial examples generated by our tool DeepTRE. We also observe that a significant proportion of the adversarial examples can be found using a relatively small L0 distance. More experimental results can be found in Appendix H of [Ruan et al., 2018b]. Overall, our tool DeepTRE offers an efficient approach to coverage-driven testing of DNNs.

6 RelatedWork

Global robustness evaluation is related to adversarial example generation. Most existing algorithms for this problem first compute a gradient (either a cost gradient or a forward gradient) and then perturb the input in different ways along the most promising direction on fooling the neural network. In view of the space limit, we omit the discussion of related work on adversarial attacks, and just mention that we have shown experimentally that our approach can obtain tighter upper bounds (i.e., smaller adversarial distances) at lower computational cost. We remark that we focus on the prevailing concept of robustness against small perturbations, called epsilon-adversarial examples in [Jacobsen et al., 2019]; at present our method is unable to deal with invariance-based adversarial examples discussed there.

Robustness evaluation is usually performed w.r.t. a similarity metric on inputs, with Lp norms typically employed for this purpose. The L0 metric has been used in [Papernot et al., 2016; Carlini et al., 2017; Huang et al., 2017; Wicker et al., 2018; Wu et al., 2018] for adversarial attacks; our method is the first to provide anytime lower and upper bounds on robustness guarantees for the L0 metric.

In addition to providing anytime upper/lower bounds on global robustness, our method also guarantees convergence. Existing approaches that offer guarantees instead focus on local (pointwise) robustness. These include reduction to constraint solving [Pulina and Tacchella, 2010; Katz et al., 2017], abstract interpretation [Gehr et al., 2018; Mirman et al., 2018], exhaustive search [Huang et al., 2017] or Monte Carlo tree search (MCTS) for Lipschitz networks [Wu et al., 2018]. Another group of papers considers the problem of whether an output value of a DNN is reachable from a given input subspace [Lomuscio and Maganti, 2017; Ruan et al., 2018a; Dutta et al., 2017], by either reducing the problem to a MILP problem [Lomuscio and Maganti, 2017], or by considering the range of values [Dutta et al., 2017], or by employing global optimisation [Ruan et al., 2018a]. We also mention [Peck et al., 2017], who compute a lower bound of local robustness for the L2 norm. This is incomparable with our result because of the different distance metrics. In recent work [Gopinath et al., 2018] the input vector space is partitioned using clustering and then the method of [Katz et al., 2017] is used to check the individual partitions. However, none of the methods and tools above support the L0 distance and provide anytime and guaranteed convergence to the true global robustness. Thus, our tool, DeepTRE, is complementary to existing approaches.

7 Conclusions

To the best of our knowledge, this is the first algorithm that evaluates global robustness of DNNs based on the Hamming distance with provable guarantees. We provide a tensor-based implementation of the technique to exploit the inherent parallelism. Our experimental results demonstrate wide applicability and efficiency of the method, with potential for real-time deployment. We hypothesise that the approach computes a good proxy for the robustness against physical attacks that rely on the manipulation of a small part of the objects that are to be recognised.

Acknowledgements

MK and WR have been partially supported by the EPSRC Programme Grant on Mobile Autonomy (EP/M019918/1). MW has been supported by the CSC-PAG Oxford Scholarship.