{'fraction_non_alphanumeric': 0.043176223433734166, 'fraction_numerical': 0.00929255435693204, 'mean_word_length': 4.427771948233648, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 3, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Game-Based Approximate Verification of Deep Neural Networks with Provable Guarantees

Despite the improved accuracy of deep neural networks, the discovery of adversarial examples has raised serious safety concerns. In this paper, we study two variants of pointwise robustness, the maximum safe radius problem, which for a given input sample computes the minimum distance to an adversarial example, and the feature robustness problem, which aims to quantify the robustness of individual features to adversarial perturbations. We demonstrate that, under the assumption of Lipschitz continuity, both problems can be approximated using finite optimisation by discretising the input space, and the approximation has provable guarantees, i.e., the error is bounded. We then show that the resulting optimisation problems can be reduced to the solution of two-player turn-based games, where the first player selects features and the second perturbs the image within the feature. While the second player aims to minimise the distance to an adversarial example, depending on the optimisation objective the first player can be cooperative or competitive. We employ an anytime approach to solve the games, in the sense of approximating the value of a game by monotonically improving its upper and lower bounds. The Monte Carlo tree search algorithm is applied to compute upper bounds for both games, and the Admissible A* and the Alpha-Beta Pruning algorithms are, respectively, used to compute lower bounds for the maximum safety radius and feature robustness games. When working on the upper bound of the maximum safe radius problem, our tool demonstrates competitive performance against existing adversarial example crafting algorithms. Furthermore, we show how our framework can be deployed to evaluate pointwise robustness of neural networks in safety-critical applications such as traffic sign recognition in self-driving cars.


Introduction
Deep neural networks (DNNs or networks, for simplicity) have been developed for a variety of tasks, including malware detection [1], abnormal network activity detection [2], and self-driving cars [3,4,5]. A classification network N can be used as a decision-making algorithm: given an input α, it suggests a decision N (α) among a set of possible decisions. While the accuracy of neural networks has greatly improved, matching the cognitive ability of humans [6], they are susceptible to adversarial examples [7,8]. An adversarial example is an input which, though initially classified correctly, is misclassified after a minor, perhaps imperceptible, perturbation. Adversarial examples pose challenges for self-driving cars, where neural network solutions have been proposed for tasks such as end-to-end steering [3], road segmentation [4], and traffic sign classification [5]. In the context of steering and road segmentation, an adversarial example may cause a car to steer off the road or drive into barriers, and misclassifying traffic signs may cause a vehicle to drive into oncoming traffic. Figure 1 shows an image of a traffic light correctly classified by a state-of-the-art network, which is then misclassified after only a few pixels have been changed. Though somewhat artificial, since in practice the controller would rely on additional sensor input when making a decision, such cases strongly suggest that, before deployment in safety-critical tasks, DNNs' resilience (or robustness) to adversarial examples must be strengthened.
Robustness of neural networks is an active topic of investigation and a number of approaches have been proposed to search for adversarial examples (see Related Work). They are based on computing the gradients [9], along which a heuristic search moves; computing a Jacobian-based saliency map [10], based on which pixels are selected to be changed; transforming the existence of adversarial examples into an optimisation problem [11], on which an optimisation algorithm can be applied; transforming the existence of adversarial examples into a constraint solving problem [12], on which a constraint solver can be applied; or discretising the neighbourhood of a point and searching it exhaustively in a layer-by-layer manner [13].
In this paper, we propose a novel game-based approach for safety verification of DNNs. We consider two pointwise robustness problems, referred to as the maximum safe radius problem and feature robustness problem, respectively. The former aims to compute for a given input the minimum distance to an adversarial example, and therefore can be regarded as the computation of an absolute safety radius, within which no adversarial example exists. The latter problem studies whether the crafting of adversarial examples can be controlled by restricting perturbations to only certain features (disjoint sets of input dimensions), and therefore can be seen as the computation of a relative safety radius, within which the existence of adversarial examples is controllable.
Both pointwise robustness problems are formally expressed in terms of nonlinear optimisation, which is computationally challenging for realistically-sized networks. We thus utilise Lipschitz continuity of DNN layers, which bounds the maximal rate of change of outputs of a function with respect to the change of inputs, as proposed for neural networks with differentiable layers in [14,15]. This enables safety verification by relying on Lipschitz constants to provide guaranteed bounds on DNN output for all possible inputs. We work with modern DNNs whose layers, e.g., ReLU, may not be differentiable, and reduce the verification to finite optimisation. More precisely, we prove that under the assumption of Lipschitz continuity [16] it is sufficient to consider a finite number of uniformly sampled inputs when the distances between the inputs are small, and that this reduction has provable guarantees, in the sense of the error being bounded by the distance between sampled inputs.
We then show that the finite optimisation problems can be computed as the solution of two-player turn-based games, where Player I selects features and Player II then performs a perturbation within the selected features. After both players have made their choices, the input is perturbed and the game continues. While Player II aims to minimise the distance to an adversarial example, Player I can be cooperative or competitive. When it is cooperative, the optimal reward of Player I is equal to the maximum safe radius. On the other hand, when it is competitive the optimal reward of Player I quantifies feature robustness. Finally, because the state space of the game models is intractable, we employ an anytime approach to compute the upper and lower bounds of Player I optimal reward. The anytime approach ensures that the bounds can be gradually, but strictly, improved so that they eventually converge. More specifically, we apply Monte Carlo tree search algorithm to compute the upper bounds for both games, and Admissible A* and Alpha-Beta Pruning, respectively, to compute the lower bounds for the games.
We implement the method in a software tool DeepGame 2 , and conduct experiments on DNNs to show convergence of lower and upper bounds for the maximum safe radius and feature robustness problems. Our approach can be configured to work with a variety of feature extraction methods that partition the input, for example image segmentation, with simple adaptations. For the image classification networks we consider in the experiments, we employ both the saliency-guided grey-box approach adapted from [17] and the featureguided black-box method based on the SIFT object detection technique [18]. For the maximum safety radius problem, our experiments show that, on networks trained on the benchmark datasets such as MNIST [19], CIFAR10 [20] and GTSRB [21], the upper bound computation method is competitive with state-of-the-art heuristic methods (i.e., without provable guarantees) that rely on white-box saliency matrices or sophisticated optimisation procedures. Finally, to show that our framework is well suited to safety testing and decision support for deploying DNNs in safety-critical applications, we experiment on state-of-the-art networks, including the winner of the Nexar traffic light challenge [22].
The paper significantly extends work published in [23], where the game-based approach was first introduced for the case of cooperative games and evaluated on the computation of upper bounds for the maximum safety radius problem using the SIFT feature extraction method. In contrast, in this paper we additionally study feature robustness, generalise the game to allow for the competitive player, and develop algorithms for the computation of both lower and upper bounds. We also give detailed proofs of the theoretical guarantees and error bounds.
The structure of the paper is as follows. After introducing preliminaries in Section 2, we formalise the maximum safety radius and feature robustness problems in Section 3. We present our game-based approximate verification approach and state the guarantees in Section 4. Algorithms and implementation are described in Section 5, while experimental results are given in Section 6. We discuss the related work in Section 7 and conclude the paper in Section 8.

Preliminaries
Let N be a neural network with a set C of classes. Given an input α and a class c ∈ C, we use N (α, c) to denote the confidence (expressed as a probability value obtained from normalising the score) of N believing that α is in class c. Moreover, we write N (α) = arg max c∈C N (α, c) for the class into which N classifies α. We let P 0 be the set of input dimensions, n = |P 0 | be the number of input dimensions, and remark that without loss of generality the dimensions of an input are normalised as real values in [0,1]. The input domain is thus a vector space D = [0, 1] n .
For image classification networks, the input domain D can be represented as 255] , where w, h, ch are the width, height, and number of channels of an image, respectively. That is, we have P 0 = w × h × ch. We may refer to an element in w × h as a pixel and an element in P 0 as a dimension. We use α[i] for i ∈ P 0 to denote the value of the i-th dimension of α.

Distance Metric and Lipschitz Continuity
As is common in the field, we will work with L k distance functions to measure the distance between inputs, denoted ||α − α || k with k ≥ 1, and satisfying the standard axioms of a metric space: • ||α − α || k = 0 implies that α = α (identity of indiscernibles), While we focus on L k distances, including L 1 (Manhattan distance), L 2 (Euclidean distance), and L ∞ (Chebyshev distance), we emphasise that the results of this paper hold for any distance metric and can be adapted to image similarity distances such as SSIM [24]. Though our results do not generalise to L 0 (Hamming distance), we utilise it for the comparison with existing approaches to generate adversarial examples, i.e., without provable guarantees (Section 6.4).
Since we work with pointwise robustness [25], we need to consider the neighbourhood of a given input. Definition 1. Given an input α, a distance function L k , and a distance d, we as the set of inputs whose distance to α is no greater than d with respect to L k .
The d-neighbourhood of α is simply the L k ball with radius d. For example, η(α, L 1 , d) includes those inputs such that the sum of the differences of individual dimensions from the original input α is no greater than d, i.e., ||α − α|| 1 = We will sometimes work with dneighbourhood, where, given a number d, d = d + for any real number > 0 denotes a number greater than d.
We will restrict the neural networks we consider to those that satisfy the Lipschitz continuity assumption, noting that all networks whose inputs are bounded, including all image classification networks we studied, are Lipschitz continuous. Specifically, it is shown in [25,16] that most known types of layers, including fully-connected, convolutional, ReLU, maxpooling, sigmoid, softmax, etc., are Lipschitz continuous. Definition 2. Network N is a Lipschitz network with respect to distance function L k if there exists a constant c > 0 for every class c ∈ C such that, for all α, α ∈ D, we have where c is the Lipschitz constant for class c.

Input Manipulations
To study the crafting of adversarial examples, we require the following operations for manipulating inputs. Let τ > 0 be a positive real number representing the manipulation magnitude, then we can define input manipulation operations δ τ,X,ψ : D → D for X ⊆ P 0 , a subset of input dimensions, and ψ : P 0 → N, an instruction function by: for all i ∈ P 0 . Note that if the values are bounded, e.g., in the interval [0, 1], then δ τ,X,ψ (α[i]) needs to be restricted to be within the bounds. Let Ψ be the set of possible instruction functions.
The following lemma shows that input manipulation operations allow one to map one input to another by changing the values of input dimensions, regardless of the distance measure L k . Lemma 1. Given any two inputs α 1 and α 2 , and a distance ||α 1 − α 2 || k for any measure L k , there exists a magnitude τ > 0, an instruction function ψ ∈ Ψ, and a subset X ⊆ P 0 of input dimensions, such that where > 0 is an error bound.
Intuitively, any distance can be implemented through an input manipulation with an error bound .
The error bound is needed because input α ∈ D = [0, 1] n is bounded, and thus reaching another precise input point via a manipulation is difficult when each input dimension is a real number.
We will also distinguish a subset of atomic input manipulations, each of which changes a single dimension for a single magnitude.
While the existence of a sequence of atomic manipulations implementing a given manipulation is determined, there may exist multiple sequences. On the other hand, from a given sequence of atomic manipulations we can construct a single input manipulation by sequentially applying the atomic manipulations.

Feature-Based Partitioning
Natural data, for example natural images and sounds, forms a high-dimensional manifold, which embeds tangled manifolds to represent their features [26]. Feature manifolds usually have lower dimensions than the data manifold. Intuitively, the set of features form a partition of the input dimensions P 0 . In this paper, we use a variety of feature extraction methods to partition the set P 0 into disjoint subsets.
Definition 4. Let λ be a feature of an input α ∈ D, then we use P λ ⊆ P 0 to denote the dimensions represented by λ. Given an input α, a feature extraction function Λ maps an input α into a set of features Λ(α) such that (1) P 0 = λ∈Λ(α) P λ , and (2) P λi ∩ P λj = ∅ for any λ i , λ j ∈ Λ(α) with i = j. We remark that our technique is not limited to image classification networks and is able to work with general classification tasks, as long as there is a suitable feature extraction method that generates a partition of the input dimensions.
In our experiments we focus on image classification for illustrative purposes and to enable better comparison, and employ saliency-guided grey-box and featureguided black-box approaches to extract features, described in Section 4.

Problem Statement
In this paper we focus on pointwise robustness [25], defined as the invariance of the network's classification over a small neighbourhood of a given input. This is a key concept, which also allows one to define robustness as a network property, by averaging with respect to the distribution of the test data set. Pointwise robustness can be used to define safety of a classification decision for a specific input, understood as the non-existence of an adversarial example in a small neighbourhood of the input. We work with this notion and consider two problems for quantifying the robustness of the decision, the computation of the maximum safe radius and feature robustness, which we introduce next.
First we recall the concept of an adversarial example, as well as what we mean by targeted and non-targeted safety.
Definition 5. Given an input α ∈ D, a distance measure L k for some k ≥ 0, and a distance d, an adversarial example α of class c is such that α ∈ η(α, L k , d), N (α) = N (α ), and N (α ) = c. Moreover, we write adv k,d (α, c) for the set of adversarial examples of class c and let A targeted safety of class c is defined as adv k,d (α, c) = ∅, and non-targeted safety is adv k,d (α) = ∅.
The following formalisation focuses on targeted safety of a fixed input α and a fixed class c = N (α) for a network N . The case of non-targeted safety (misclassification into class other than c) is similar.

The Maximum Safe Radius Problem
Given a targeted safety problem for α, we aim to compute the distance ||α − α || k to the nearest adversarial example within the d-neighbourhood of α, or in other words the radius of the maximum safe ball, illustrated in Figure 2.
Definition 6 (Maximum Safe Radius). The maximum safe radius problem is to compute the minimum distance from the original input α to an adversarial example, i.e., Intuitively, MSR(k, d, α, c) represents an absolute safety radius within which all inputs are safe. In other words, within a distance of less than MSR(k, d, α, c), no adversarial example is possible. When no adversarial example can be found within radius d, i.e., adv k,d (α, c) = ∅, the maximum safe radius cannot be computed, but is definitely greater than d. Therefore, we let MSR(k, d, α, c) = d . Intuitively, finding an adversarial example can only provide a loose upper bound of MSR. Instead, this paper investigates a more fundamental problemhow to approximate the true MSR distance with provable guarantees.
Approximation Based on Finite Optimisation. Note that the sets adv k,d (α, c) and adv k,d (α) of adversarial examples can be infinite. We now present a discretisation method that allows us to approximate the maximum safe radius using finite optimisation, and show that such a reduction has provable guarantees, provided that the network is Lipschitz continuous. Our approach proceeds by constructing a finite 'grid' of points in the input space. Lipschitz continuity enables us to reduce the verification problem to manipulating just the grid points, through which we can bound the output behaviour of a DNN on the whole input space, since Lipschitz continuity ensures that the network behaves well within each cell. The number of grid points is inversely proportional to the Lipschitz constant. However, estimating a tight Lipschitz constant is difficult, and so, rather than working with the Lipschitz constant directly, we assume the existence of a (not necessarily tight) Lipschitz constant and work instead with a chosen fixed magnitude of an input manipulation, τ ∈ (0, 1]. We show how to determine the largest τ for a given Lipschitz network and give error bounds for the computation of MSR that depend on τ . We discuss how Lipschitz constants can be estimated in Section 6.2 and Related Work.
Intuitively, we aim to find a set Λ of features, a set X of dimensions within Λ , and a manipulation instruction ψ such that the application of the atomic manipulation δ τ,X,ψ on the original input α leads to an adversarial example δ τ,X,ψ (α) that is nearest to α among all adversarial examples. Compared to Definition 6, the search for another input by min α ∈D over an infinite set is implemented by minimisation over the finite sets of feature sets and instructions.
Since the set of input manipulations is finite for a fixed magnitude, the above optimisation problems need only explore a finite number of 'grid' points in the input domain D. We have the following lemma. To ensure the lower bound of MSR(k, d, α, c) in Lemma 3, we utilise the fact that the network is Lipschitz continuous [16]. First, we need the concepts of a τgrid input, for a manipulation magnitude τ , and a misclassification aggregator. The intuition for the τ -grid is illustrated in Figure 3. We construct a finite set of grid points uniformly spaced by τ in such a way that they can be covered by small subspaces centred on grid points. We select a sufficiently small value for τ based on a given Lipschiz constant so that all points in these subspaces are are classified the same. We then show that an optimum point on the grid is within an error bound dependent on τ from the true optimum, i.e., the closest adversarial example.
We note that τ -grid inputs in the set G(α, k, d) are reachable from each other by applying an input manipulation. The main purpose of defining τ -grid inputs is to ensure that the space η(α, L k , d) can be covered by small subspaces centred on grid points. To implement this, we need the following lemma.
Intuitively, if a misclassification aggregator α 1 with respect to β is classified correctly, then all inputs in η(α 1 , L k , β) are classified correctly.

Lemma 5.
If all τ -grid inputs are misclassification aggregators with respect to Proof: We prove by contradiction. Assume that FMSR(τ, k, d, α, c) = d for some d > 0, and MSR(k, d, α, c) < d − 1 2 d(k, τ ). Then there must exist an input α such that α ∈ adv k,d (α, c) and Figure 3: Provable guarantees for the MSR and FR Λ problems on a dense τ -grid (green dots) that is reached upon convergence. In the worst case, the true optimum (the red dot) lies in the middle between two hyper-points of the τ -grid, with the distance of at most 1 2 d(k, τ ) from the found optimum. and α is not a τ -grid input. By Lemma 4, there must exist a τ -grid input α such that α ∈ η(α , L k , 1 2 d(k, τ )). Now because all τ -grid inputs are misclassification aggregators with respect to 1 2 d(k, τ ), we have α ∈ adv k,d (α, c). By α ∈ adv k,d (α, c) and the fact that α is a τ -grid input, we have that Now, combining Equations (5) and (6), we have that FMSR(τ, k, d, α, c) < d , which contradicts the hypothesis that FMSR(τ, k, d, α, c) = d .
In the following, we discuss how to determine the largest τ for a Lipschitz network in order to satisfy the condition in Lemma 5 that all τ -grid inputs are misclassification aggregators with respect to 1 2 d(k, τ ).
Definition 10. Given a class label c, we let be a function maintaining for an input α the minimum confidence margin between the class c and another class c = N (α ).
Note that, given an input α and a class c, we can compute g(α , c) in constant time. The following lemma shows that the above-mentioned condition about misclassification aggregators can be obtained if τ is sufficiently small. Lemma 6. Let N be a Lipschitz network with a Lipschitz constant c for every class c ∈ C. If for all τ -grid input α ∈ G(α, k, d), then all τ -grid inputs are misclassification aggregators with respect to 1 2 d(k, τ ).
Proof: For any input α whose closest τ -grid input is α , we have Now, to ensure that no class change occurs between α and α , we need to have g(α , N (α )) ≥ 0, which means that g(α , N (α )) − g(α , N (α )) ≤ g(α , N (α )). Therefore, we can let Note that g(α , N (α )) is dependent on the τ -grid input α , and thus can be computed when we construct the grid. Finally, we let Therefore, if we have the above inequality for every τ -grid input, then we can conclude g(α , N (α )) ≥ 0 for any α ∈ η(α , k, d), i.e., N (α , N (α )) ≥ N (α , c) for all c ∈ C. The latter means that no class change occurs. Combining Lemmas 3, 5, and 6, we have the following theorem which shows that the reduction has a provable guarantee, dependent on the choice of the manipulation magnitude.
Proof: By Lemma 3, we have MSR(k, d, α, c) ≤ FMSR(τ, k, d, α, c) for any τ > 0. By Lemma 5 and Lemma 6, when FMSR(τ, k, d, α, c) = d , we have MSR(k, d, α, c) ≥ Figure 4: Illustration of the feature robustness (FR Λ ) problem, which aims to find, on an original image α, a feature, or a subset of features, that is the most robust against adversarial perturbations. Given a benign image, we first apply feature extraction or semantic partitioning methods to produce a set of disjoint features ('Sky', 'Trees', 'Cat', etc.), then we find a set of robust features that is most resilient to adversarial perturbations ('Grass' in the figure), which quantifies the most robust direction in a safe norm ball.

The Feature Robustness Problem
The second problem studied in this paper concerns which features are the most robust against perturbations, illustrated in Figure 4. The feature robustness problem has been studied in explainable AI. For example, [27] explains the decision making of an image classification network through different contributions of the superpixels (i.e., features) and [28] presents a general additive model for explaining the decisions of a network by the Shapley value computed over the set of features.
Let P 0 (α 1 , α 2 ) ⊆ P 0 be the set of input dimensions on which α 1 and α 2 have different values.
Definition 11 (Feature Robustness). The feature robustness problem is defined as follows.
where Λ is a feature extraction function, and α m , α m+1 (m ∈ N) are the inputs before and after the application of some manipulation on a feature λ m , respectively. If after selecting a feature λ m no adversarial example can be reached, i.e., ∀α m+1 : Intuitively, the search for the most robust feature alternates between maximising over the features and minimising over the possible input dimensions within the selected feature, with the distance to the adversarial example as the objective. Starting from FR Λ (k, d, α 0 , c) where α 0 is the original image, the process moves to FR Λ (k, d, α 1 , c) by a max-min alternation on selecting feature λ 0 and next input α 1 . This continues until either an adversarial example is found, or the next input α i for some i > 0 is outside the d-neighbourhood η(α, L k , d).
The value d is used is to differentiate from the case where the minimal adversarial example has exactly distance d from α 0 and the manipulations are within λ 0 . In such a case, according to Equation (13) Assuming FR Λ (k, d, α, c) has been computed and a distance budget d ≤ d is given to manipulate the input α, the following cases can be considered.
• If FR Λ (k, d, α, c) > d, then there are robust features, and if manipulations are restricted to those features no adversarial example is possible.
then, no matter how one restricts the features to be manipulated, an adversarial example can be found within the budget.
then the existence of adversarial examples is controllable, i.e., we can choose a set of features on which the given distance budget d is insufficient to find an adversarial example. This differs from the first case in that an adversarial example can be found if given a larger budget d.
Therefore, studying the feature robustness problem enables a better understanding of the robustness of individual features and how the features contribute to the robustness of an image.
It is straightforward to show that Compared to the absolute safety radius by MSR(k, d, α, c), FR Λ (k, d, α, c) can be seen as a relative safety radius, within which the existence of adversarial examples can be controlled. Theoretically, the MSR(k, d, α, c) problem can be seen as a special case of the FR Λ (k, d, α, c) problem, when we let |Λ(α)| = 1.
We study them separately, because the MSR(k, d, α, c) problem is interesting on its own, and, more importantly, we show later that they can be solved using different methods.
One can also consider a simpler variant of this problem, which aims to find a subset of features that are most resilient to perturbations, and which can be solved by only considering singleton sets of features. We omit the formalisation for reasons of space.
We illustrate the two problems, the maximum safe radius (MSR) and (the simpler variant of) feature robustness (FR Λ ), through Example 1. Figure 5, the minimum distance from the original image to an adversary is two pixels, i.e., MSR = 2 (for simplicity here we take the L 0 -norm). That is, for a norm ball with radius less than 2, the image is absolutely safe. Note that, for MSR, the manipulations can span different features. After feature extraction, we find the maximum safe radius of each feature, i.e., MSR λ1 = 3, MSR λ2 = 4, MSR λ3 = 3, MSR λ4 = 5.

Example 1. As shown in
Assume that we have a norm ball of radius d, and a distance budget d , then: • if d = 4, then by definition we have FR Λ = 4 , i.e., manipulating 'Grass' cannot change the classification; • if d = 10 and d = 7 then we have FR Λ = 5 < d < d, i.e., all the features are fragile; • if d = 10 and d = 4 then d < FR Λ = 5 < d, i.e., the existence of an adversary is controllable by restricting perturbations to 'Grass'.
Approximation Based on Finite Optimisation. Similarly to the case of the maximum safe radius, we reduce the feature robustness problem to finite optimisation by implementing the search for adversarial examples using input manipulations.
Definition 12. Let τ ∈ (0, 1] be a manipulation magnitude. The finite feature robustness problem FFR Λ (τ, k, d, α, c) based on input manipulation is as follows: where Λ is a feature extraction function, and α m , δ τ,X,ψ (α m ), m ∈ N, are the perturbed inputs before and after the application of manipulation δ τ,X,ψ on a feature λ m , respectively. If after selecting a feature λ m no adversarial example can be reached, i.e., ∀X ⊆ P λm ∀ψ ∈ Ψ : Compared to Definition 11, the search for another input by min αm+1∈η(α,L k ,d) is implemented by combinatorial search over the finite sets of feature sets and instructions.
Error Bounds. The case for the feature robustness problem largely follows that of the maximum safe radius problem. First of all, we have the following lemma which bounds the error of FFR Λ (τ, k, d, α, c) to 1 2 d(k, τ ), which depends on the value of magnitude.
Combining Lemmas 3, 6, and 7, we have the following theorem which shows that the reduction has a provable guarantee under the assumption of Lipschitz continuity. The approximation error depends linearly on the prediction confidence on discretised 'grid' inputs and is inversely proportional with respect to the Lipschitz constants of the network.

A Game-Based Approximate Verification Approach
In this section, we define a two-player game and show that the solutions of the two finite optimisation problems, FMSR(k, d, α, c) and FFR Λ (k, d, α, c), given in Expressions (4) and (15) can be reduced to the computation of the rewards of Player I taking an optimal strategy. The two problems differ in that they induce games in which the two players are cooperative or competitive, respectively.
The game proceeds by constructing a sequence of atomic input manipulations to implement the optimisation objectives in Equations (4) and (15).

Problem Solving as a Two-Player Turn-Based Game
The game has two players, who take turns to act. Player I selects features and Player II then selects an atomic input manipulation within the selected features. While Player II aims to minimise the distance to an adversarial example, depending on the optimisation objective designed for either FMSR(k, d, α, c) or FFR Λ (k, d, α, c), Player I can be cooperative or competitive. We remark that, in contrast to [23] where the games were originally introduced, we do not consider the nature player.
• S is a set of game states belonging to Player I such that each state represents an input in η(α, L k , d), and S ×Λ(α) is a set of game states belonging to Player II where Λ(α) is a set of features of input α. We write α(s) for the input associated to the state s ∈ S.  Figure 6: Two-player turn-based solution for finite optimisation. Player I selects features and Player II then performs an atomic input manipulation within the selected features. For the Maximum Safe Radius problem, both Player I and Player II aim to minimise the distance to an adversarial example; for the Feature Robustness problem, while Player II has the same objective, Player I plays against this, i.e., aiming to prevent the reaching of adversarial examples by taking suitable actions. The game terminates when an adversary is found or the distance budget for adversarial perturbation has been reached.
• s 0 ∈ S is the initial game state such that α(s 0 ) is the original input α.
• The transition relation T I : S × Λ(α) → S × Λ(α) is defined as and transition relation T II : (S × Λ(α)) × P(P 0 ) × Ψ → S is defined as where X ⊆ P λ is a set of input dimensions within feature λ, ψ : P 0 → {−1, +1} is a manipulation instruction, and δ τ,X,ψ is an atomic dimension manipulation as defined in Definition 3. Intuitively, in every game state s ∈ S, Player I will choose a feature λ, and, in response to this, Player II will choose an atomic input manipulation δ τ,X,ψ .
• The labelling function L : S ∪ (S × Λ(α)) → C assigns to each state s or (s, λ) a class N (α(s)). Figure 6 illustrates the game model with a partially-expanded game tree.
Strategy Profile. A path (or game play) of the game model is a sequence s 1 u 1 s 2 u 2 ... of game states such that, for all k ≥ 1, we have u k = T I (s k , λ k ) for some feature λ k and s k+1 = T II ((s k , λ k ), X k , ψ k ) for some (X k , ψ k ). Let last(ρ) be the last state of a finite path ρ, and P ath F a be the set of finite paths such that last(ρ) belongs to player a ∈ {I, II}.
Definition 13. A stochastic strategy σ I : P ath F I → D(Λ(α)) of Player I maps each finite path to a distribution over the next actions, and similarly for σ II : P ath F II → D(P(P 0 ) × I) for Player II. We call σ = (σ I , σ II ) a strategy profile.
Rewards. We define a reward R(σ, ρ) for a given strategy profile σ = (σ I , σ II ) and a finite path ρ ∈ a∈{I,II} P ath F a . The idea of the reward is to accumulate the distance to the adversarial example found over a path. Note that, given σ, the game becomes a deterministic system. Let α ρ = α(last(ρ)) be the input associated with the last state of the path ρ. We write representing that the path has reached a state whose associated input either is in the target class c or lies outside the region η(α, L k , d). The path ρ can be terminated whenever t(ρ) is satisfied. It is not hard to see that, due to the constraints in Definition 5, every infinite path has a finite prefix which can be terminated (that is, either when an adversarial example is found or the distance to the original image has exceeded d). During each expansion of the game model, an atomic manipulation is employed, which excludes the possibility that an input dimension is perturbed in smaller and smaller steps.
Intuitively, if an adversarial example is found then the reward assigned is the distance to the original input, otherwise it is the weighted summation of the rewards of its children.
Players' Objectives. Players' strategies are to maximise their rewards in a game. The following players' objectives are designed to match the finite optimisation problems stated in Equations (4) and (15).
Definition 15. In a game, Player II chooses a strategy σ II to minimise the reward R((σ I , σ II ), s 0 ), whilst Player I has different goals depending on the optimisation problem under consideration.
• For the maximum safe radius problem, Player I chooses a strategy σ I to minimise the reward R((σ I , σ II ), s 0 ), based on the strategy σ II of Player II.
That is, the two players are cooperative.
• For the feature robustness problem, Player I chooses a strategy σ I to maximise R((σ I , σ II ), s 0 ), based on the strategy σ II of Player II. That is, the two players are competitive.
The goal of the game is for Player I to choose a strategy σ I to optimise its objective, to be formalised below.

Safety Guarantees via Optimal Strategy
For different objectives x ∈ {MSR(k, d, α, c), FR Λ (k, d, α, c)} of Player I, we construct different games. Given a game model M (k, d, α, c) and an objective x of Player I, there exists an optimal strategy profile σ = (σ I , σ II ), obtained by both players optimising their objectives. We will consider the algorithms to compute the optimal strategy profile in Section 5. Here we focus on whether the obtained optimal strategy profile σ is able to implement the finite optimisation problems in Equations (4) and (15).
First of all, we formally define the goal of the game.
That is, the goal is to compute the reward of the initial state s 0 based on σ.
Note that an initial state s 0 is also a finite path, and it is a Player I state.
We have the following Theorems 3 and 4 to confirm that the game can return the optimal values for the two finite optimisation problems.
Finally, we notice that the above minimum value of ||α − α || k is equivalent to the optimal value required by Equation (4).
Proof: First of all, let Λ 1 be the set of features and ∆ 1 be the set of atomic input manipulations in achieving the optimal value of FFR Λ (τ, k, d, α, c). We can construct a game play for (Λ 1 , ∆ 1 ). More specifically, the game play leads from the initial state to a terminal state, by recursively selecting an unused input manipulation and its associated feature and defining the corresponding moves for Player I and Player II, respectively. Therefore, because the strategy profile σ is optimal, we have val(M (k, d, α, c), On the other hand, we notice that the ordering of the applications of atomic input manipulations does not matter, because the reward of the terminal state is the distance from its associated input to the original input. Therefore, because the game explores exactly all the possible applications of atomic input manipulations and FFR Λ (τ, k, d, α, c) is the optimal value by its definition, by Lemma 2 we have that val(M (k, d, α, c), FR Λ (k, d, α, c)) ≤ FFR Λ (τ, k, d, α, c).
Combining Theorems 3, 4 with Theorems 1, 2, we have the following corollary, which states that the optimal game strategy is able to achieve the optimal value for the maximum safe radius problem MSR(k, d, α, c) and the feature robustness problem FR Λ (k, d, α, c) with an error bound 1 2 d(k, τ ).
Corollary 1. The two-player turn-based game is able to solve the maximum safe radius problem of Equation (3) and the feature robustness problem of Equation (12) with an error bound 1 2 d(k, τ ), when the magnitude τ is such that Furthermore, we have the following lemma.

Complexity of the Problem
As a by-product of Lemma 8, the theoretical complexity of the problems is in PTIME, with respect to the size of the game model M (k, d, α, c). However, the size of the game is exponential with respect to the number of input dimensions. More specifically, we have the following complexity result with respect to the manipulation magnitude τ , the pre-specified range size d, and the number of input dimensions n.
Proof: We can see that the size of the grid, measured as the number |G(α, k, d)| of τ -grid inputs in η(α, L k , d), is polynomial with respect to d/τ and exponential with respect to n. From a τ -grid to any of its neighbouring τ -grids, each player needs to take a move. Therefore, the number of game states is doubled (i.e., polynomial) over |G(α, k, d)|. This yields PTIME complexity of solving the game.
Considering that the problem instances we work with usually have a large input dimensionality, this complexity suggests that directly working with the explicit game models is impractical. If we consider an alternative representation of a game tree (i.e., an unfolded game model) of finite depth to express the complexity, the number of nodes on the tree is O(n h ) for h the length of the longest finite path without a terminating state. While the precise size of O(n h ) is dependent on the problem (including the image α and the difficulty of crafting an adversarial example), it is roughly O(50000 100 ) for the images used in the ImageNet competition and O(1000 20 ) for smaller images such as GTSRB, CIFAR10, and MNIST. This is beyond the capability of existing approaches for exact or -approximate computation of probability (e.g., reduction to linear programming [29], value iteration, and policy iteration, etc.) that are used in probabilistic verification.

Algorithms and Implementation
In this section we describe the implementation of the game-based approach introduced in this paper. Figure 7 presents an overview of the reductions from the original problems to the solution of a two-player game for the case of Lipschitz networks, described in Section 3. Because exact computation of optimal rewards is computationally hard, we approximate the rewards by means of algorithms that unfold the game tree based on Monte Carlo tree search (MCTS), Admissible A * , and Alpha-Beta Pruning.
We take a principled approach to compute for each of the two game values, MSR(k, d, α, c) and FR Λ (k, d, α, c), an upper bound and a lower bound. Our algorithms can gradually, but strictly, improve the bounds, so that they gradually converge as the computation proceeds. For x ∈ {MSR(k, d, α, c), FR Λ (k, d, α, c)}, we write l x and u x for their lower and upper bound, respectively. The bounds can be interesting in their own. For example, a lower bound l MSR(k,d,α,c) suggests absolute safety of an L k norm ball with radius l MSR(k,d,α,c) from the original input α, and an upper bound u MSR(k,d,α,c) suggests the existence of an adversarial We consider two feature extraction approaches to generate feature partitioning: a saliency-guided grey-box approach and a feature-guided black-box approach. For the grey-box approach, adapted from [17], each dimension of an input is evaluated on its sensitivity to the classification outcome of a DNN. For the black-box procedure, Scale Invariant Feature Transform (SIFT) [18] is used to extract image features, based on which a partition is computed. SIFT is a reasonable proxy for human perception, irrelevant to any image classifier, and its extracted features have a set of invariant characteristics, such as scaling, rotation, translation, and local geometric distortion. Readers are referred to Section 6.1 for an experimental illustrations of these two approaches.
Next we present the algorithms we employ to compute the upper and lower bounds of the values of the games, as well as their convergence analysis.

Upper Bounds: Monte Carlo Tree Search (MCTS)
We present an approach based on Monte Carlo tree search (MCTS) [30] to find an optimal strategy asymptotically. As a heuristic search algorithm for decision processes notably employed in game play, MCTS focuses on analysing the most promising moves via expanding the search tree based on random sampling of the search space. The algorithm, whose pseudo-code is presented in Algorithm 1, gradually expands a partial game tree by sampling the strategy space of the model M (k, d, α, c). With the upper confidence bound (UCB) [31] as the exploration-exploitation trade-off, MCTS has a theoretical guarantee that it converges to the optimal solution when the game tree is fully explored. In the following, we explain the components of the algorithm.
Concerning the data structure, we maintain the set of nodes on the partial tree T (k, d, α, c). For every node o on the partial tree, we maintain three variables, r o , n o , e o , which represent the accumulated reward, the number of visits, and the current best input with respect to the objective of the player, respectively. We remark that e o is usually different from α(s o ), which is the input While(¬tc): 6: leaf ← selection(root) 7: newnodes ← expansion(M (k, d, α, c), leaf ) 8: for node in newnodes: 9: v ← Simulation (M (k, d, α, c), node) 10: backP ropogation(node, v) 11: return optimal value of the root node associated with the game state s o . Moreover, for every node o, we record its parent node p o and a set C o of its children nodes. The value val(M (k, d, α, c), x) of the game is approximated by ||e root − α|| k , which represents the distance between the original input and the current best input maintained by the root node of the tree.
The selection procedure starts from the root node, which contains the original image, and conducts a tree traversal until reaching a leaf node (Line 6). From a node, the next child node to be selected is dependent on an explorationexploitation balance, i.e., UCB [31]. More specifically, on a node o, for every be the weight of choosing o as the next node from o. Then the actual choice of a next node is conducted by sampling over a probabilistic distribution P rob o : which is a normalisation over the weights of all children. On a leaf node o, the expansion procedure returns a set of children nodes C o by applying the transition relation in the game model M (k, d, α, c) (Line 7). These new nodes are added into the partial tree T (k, d, α, c). This is the only way for the partial tree to grow. After expanding the leaf node to have its children added to the partial tree, we call the Simulation procedure on every child node (Line 9). A simulation on a new node o is a play of the game from o until it terminates. Players act randomly during the simulation. Every simulation terminates when reaching a terminal node α . Once a terminal node α is reached, a reward ||α − α || k can be computed. This reward, together with the input α , is then backpropagated from the new child node through its ancestors until reaching the root (Line 10 For the FR Λ (k, d, α, c) game, Player II also takes the above approach, i.e., Equation (28), to update e o , but for Player I we let e o be e o such that We remark the game is not zero-sum for the maximum safe radius problem.

Lower Bounds: Admissible A* in a Cooperative Game
To enable the computation of lower bounds with a guarantee, we consider algorithms which can compute optimal strategy deterministically, without relying on the asymptotic convergence as MCTS does. In this section, we exploit Admissible A* to achieve the lower bound of Player I reward when it is cooperative, i.e., MSR(k, d, α, c), and in Section 5.3 we use Alpha-Beta Pruning to obtain the lower bound of Player I reward when it is competitive, i.e., FR Λ (k, d, α, c).
The A* algorithm gradually unfolds the game model into a tree. It maintains a set of leaf nodes of the unfolded partial tree, computes an estimate for every node in the set, and selects the node with the least estimated value to expand. The estimation consists of two components, one for the exact cost up to now and the other for the estimated cost of reaching the goal node. In our case, for each game state s, we assign an estimated distance value distances(s) = ||α(s) − α(s 0 )|| k + heuristic(α(s)) (30) where the first component ||α(s) − α(s 0 )|| k represents the distance from the initial state s 0 to the current state s, and the second component heuristic(α(s)) denotes the estimated distance from the current state s to a terminal state.
An admissible heuristic function is to, given a current input, never overestimate the cost of reaching the terminal game state. Therefore, to achieve the lower bound, we need to take an admissible heuristic function. We remark that, if the heuristic function is inadmissible (i.e., does not guarantee the underestimation of the cost), then the A* algorithm cannot be used to compute the lower bound, but instead can be used to compute the upper bound.
We utilise the minimum confidence margin g(α , N (α )) defined in Definition 10 to obtain an admissible heuristic function.
Lemma 9. For any game state s such that α(s) = α , the following heuristic function is admissible: and applied. We add +τ and −τ to each dimension, and make sure that it does not exceed the upper and lower bounds of the input dimension, e.g., 1 and 0 if the input is pre-processed (normalised). If exceeded, the bound value is used instead. This procedure essentially places adversarial perturbations on the image, and all manipulated images become the newnodes (Line 9). For each node in the newnodes, the DistanceEstimation function in Equation (30) is used to compute a value, which is then added into the set distances. The set distances maintains the estimated values for all leaf nodes (Line 10-11). Among all the leaf nodes whose values are maintained in distances, we select the one with the minimum M aximumSaf eRadius as the new root (Line 12). As for the termination condition ¬tc, the algorithm gradually unfolds the game tree with increasing tree depth td = 1, 2, .... Because all nodes on the same level of the tree have the same distance to the original input α, every tree depth td > 0 is associated with a distance d(td), such that d(td) is the distance of the nodes at level td. For a given tree depth td, we have a termination condition tc(td) requiring that either • all the tree nodes up to depth td have been explored, or • the current root is an adversarial example.
For the latter, ||α(root) − α(s 0 )|| k is returned and the algorithm converges. For the former, we update d(td) as the current lower bound of the game value val (M (k, d, α, c), MSR(k, d, α, c)). Note that the termination condition guarantees the closest adversarial example that corresponds to FMSR, which is within distance 1 2 d(k, τ ) from the actual closest adversarial example corresponding to MSR.

Lower Bounds: Alpha-Beta Pruning in a Competitive Game
Alpha-Beta Pruning is an adversarial search algorithm, applied commonly in two-player games, to minimise the possible cost in a maximum cost scenario. In this paper, we apply Alpha-Beta Pruning to compute the lower bounds of Player I reward in a competitive game, i.e., FR Λ (k, d, α, c).

Lemma 10.
For any game state s ∈ S ∪ (S × Λ(α)), we let σ I (s) ∈ S × Λ(α) be the next state of s ∈ S after Player I taking an action σ I , and σ II (s) ∈ S be the next state of s ∈ S × Λ(α) after Player II taking an action σ II . If using alpha(s) (initialised as −∞) to denote Player I current maximum reward on state s and beta(s) (initialised as +∞) to denote Player II current minimum reward on state s, and let then alpha(s 0 ) is a lower bound of the value val(M (k, d, α, c), FR Λ (k, d, α, c)). for f eature in f eatures: 8: f eature.beta ← +∞ 9:

13:
else: node.alpha ←AlphaBeta(node, tc) 14: f eature.beta ← min(newnodes.alpha) 15: root.alpha ← max(f eatures.beta) 16: return root.alpha Note that, for a game state s, whenever alpha(s) ≥ beta(s ) for some s = σ I (s) is satisfied, Player I does not need to consider the remaining strategies of Player II on state s , as such will not affect the final result. This is the pruning of the game tree. The Alpha-Beta Pruning algorithm is presented in Algorithm 3. Many components of the algorithm are similar to those of Admissible A*, except that each node maintains two values: alpha value and beta value. For every node, its alpha value is initialised as −∞ and its beta value is initialised as +∞. For each f eature, its beta value is the minimum of all the alpha values of the perturbed inputs whose manipulated dimensions are within this feature (Line 14); for root in each recursion, the alpha value is the maximum of all the beta values of the features (Line 15). Intuitively, beta maintains the MSR of each feature, while alpha maintains the FR Λ of an input.

Anytime Convergence
In this section, we show the convergence of our approach, i.e., that both bounds are monotonically improved with respect to the optimal values.
Upper Bounds: 1/ -Convergence and Practical Termination Condition (tc). Because we are working with a finite game, MCTS is guaranteed to converge when the game tree is fully expanded, but the worst case convergence time may be prohibitive. In practice, we can work with 1/ -convergence by letting the program terminate when the current best bound has not been improved for e.g., 1/ iterations, where > 0 is a small real number. We can also impose time constraint tc, and ask the program to return once the elapsed time of the computation has exceeded tc.
In the following, we show that the intermediate results from Algorithm 1 can be the upper bounds of the optimal values, and the algorithm is continuously improving the upper bounds, until the optimal values are reached. Lemma 11. Let ||α − e root || k be the returned result from Algorithm 1. For an FMSR(k, d, α, c) game, we have that ||α − e root || k ≥ val (M (k, d, α, c), MSR(k, d, α, c)). (38) Moreover, the discrepancy between ||α −e root || k and val (M (k, d, α, c), MSR(k, d, α, c)) improves monotonically as the computation proceeds.
Proof: Assume that we have a partial tree T (k, d, α, c). We prove by induction on the structure of the tree. As the base case, for each leaf node o we have that its best input e o is such that because a random simulation can always return a current best, which is an upper bound to the global optimal value. The equivalence holds when the simulation found an adversarial example with minimum distance. Now, for every internal node o, by Equation (28) we have that which, together with Equation (39) and induction hypothesis, implies that ||α − e o || k ≥ val(M (k, d, α, c), MSR(k, d, α, c)). Equation (38) holds since the root node is also an internal node. The monotonic improvement can be seen from Equation (28), namely that, when, and only when, the discrepancy for the leaf node is improved after a new round of random simulation, can the discrepancy for the root node be improved. Otherwise, it remains the same.
Similarly, we have the following lemma for the feature robustness game.
Proof: The proof is similar to that of Lemma 11, except that, according to Equation (29), for the nodes of Player I (including the root node) to reduce the discrepancy, i.e., ||α − e o || k − val(M (k, d, α, c), FR Λ (k, d, α, c)), it requires that all its children nodes reduce their discrepancy.
Lower Bounds: Gradual Expansion of the Game Tree. The monotonicity of the lower bounds is achieved by gradually increasing the tree depth td. Because, in both algorithms, the termination conditions are the full exploration of the partial trees up to the depth td, it is straightforward that the results returned by the algorithms are either the lower bounds or the converged results.

Experimental Results
This section presents experimental results for the proposed game-based approach for safety verification of deep neural networks, focused on demonstrating convergence and comparison with state-of-the art techniques. . Middle row: feature extraction using the SIFT approach [18]. Bottom row: image partition using K-means clustering and superpixels [32].

Feature-Based Partitioning
Our game-based approach, where Player I determines features and Player II selects pixels or dimensions within the selected feature, requires an appropriate feature partitioning method into disjoint sets of dimensions. In Figure 8 we illustrate three distinct feature extraction procedures on a colour image from the ImageNet dataset and a grey-scale image from the MNIST dataset. Though we work with image classifier networks, our approach is flexible and can be adapted to a range of feature partitioning methods.
The first technique for image segmentation is based on the saliency map generated from an image classifier such as a DNN. As shown Figure 8 (top row), the heat-map is produced by quantifying how sensitive each pixel is to the classification outcome of the DNN. By ranking these sensitivities, we separate the pixels into a few disjoint sets. The second feature extraction approach, shown in Figure 8 (middle row), is independent of any image classifier, but instead focuses on abstracting the invariant properties directly from the image. Here we show segmentation results from the SIFT method [18], which is invariant to image translation, scaling, rotation, and local geometric distortion. More details on how to adapt SIFT for safety verification on DNNs can be found in [23]. The third feature extraction method is based on superpixel representation, a dimensionality reduction technique widely applied in various computer vision applications. Figure 8 (bottom row) demonstrates an example of how to generate superpixels (i.e., the pixel clusters marked by the green grids) using colour features and K-means clustering [32].

Lipschitz Constant Estimation
Our approach assumes knowledge of a (not necessarily tight) Lipschitz constant. Several techniques can be used to estimate such a constant, including FastLin/FastLip [33], Crown [34] and DeepGO [16]. For more information see the Related Work section.
The size of the Lipschitz constant is inversely proportional to the number of grid points and error bound, and therefore affects computational performance. We remark that, due to the high non-linearity and high-dimensionality of modern DNNs, it is non-trivial to conduct verification even if the Lipschitz constant is known.

Convergence Analysis of the Upper and Lower Bounds
We demonstrate convergence of the bound computation for the maximum safe radius and feature robustness problems, evaluated on standard benchmark datasets MNIST, CIFAR10, and GTSRB. The architectures of the corresponding trained neural networks as well as their accuracy rates can be found in Appendix A.1.
Convergence of MSR in a Cooperative Game. First, we illustrate convergence of MSR in a cooperative game on the MNIST and GTSRB datasets. For the MNIST image (index 67) in Figure 9, the black line denotes the descending trend of the upper bound u MSR , whereas the red line indicates the ascending trend of the lower bound l MSR . Intuitively, after a few iterations, the upper bound (i.e., minimum distance to an adversarial example) is 2.84 wrt the L 2 metric, and the absolute safety (i.e., lower bound) is within radius 0.012 from the original image. The right-hand side of Figure 9 includes images produced by intermediate iterations, with adversarial images generated by MCTS shown in the two top rows, and safe images computed by Admissible A* in the bottom rows. Similarly, Figure 10 displays the converging upper and lower bounds of MSR in a cooperative game on a GTSRB image (index 19).
As for the computation time, each MCTS iteration updates the upper bound u MSR and typically takes minutes; each Admissible A* iteration further expands the game tree and updates the lower bound l MSR whenever applicable. The running times for the iterations of the Admissible A* vary: initially it takes minutes but this can increase to hours when the tree is larger.
Convergence of FR Λ in a Competitive Game. Next we demonstrate the convergence of FR Λ in a competitive game on the CIFAR10 and GTSRB datasets. Each iteration of MCTS or Alpha-Beta Pruning updates their respective bound with respect to a certain feature. Note that, in each MCTS iteration, upper bounds u MSR of all the features are improved and therefore the maximum among them, i.e., u FRΛ of the image, is updated, whereas Alpha-Beta Pruning calculates l MSR of a feature in each iteration, and then compares and updates l FRΛ with the computation progressing until all the features are processed.
For the CIFAR10 image in Figure 12, the green line denotes the upper bound u FRΛ and the red line denotes the lower bound l FRΛ . The "ship" image is partitioned into 10 features (see Figure 11a) utilising the grey-box extraction method. We observe that this saliency-guided image segmentation procedure captures the features well, as in Figure 11a the most influential features (in blue) resemble the (a) CIFAR10 "ship" image.
(b) GTSRB "speed limit 70" image. silhouette of the "ship". After 3 iterations, the algorithm indicates that, at L 2 distance of more than 1.75, all features are fragile, and if the L 2 distance is 0.48 there exists at least one robust feature. The right-hand side of Figure 12 shows several intermediate images produced, along with the converging u FRΛ and l FRΛ . The top row exhibits the original image as well as the manipulated images with decreasing u FR . For instance, after the 1st iteration, MCTS finds an adversary perturbed in Feature4 with L 2 distance 2.38, which means by far the most robust feature of this "ship" image is Feature4. (FeatureID is retrieved from the number in each cell of the image segmentation in Figure 11a.) When the computation proceeds, the 2nd iteration updates u FRΛ from 2.38 to 1.94, and explores the current most robust Feature8, which is again replaced by Feature9 after the 3rd iteration with lower distance 1.75. The bottom row displays the original image together with perturbations in each feature while l FRΛ is increasing. It can be seen that Feature1, Feature2, and Feature3 need only one dimension change to cause image misclassification, and the lower bound Feature4 increases from 0.42 to 0.56 after three iterations.
For the feature robustness (FR Λ ) problem, i.e., when Player I and Player II are competing against each other, apart from the previous CIFAR10 case where Player II wins the game by generating an adversarial example with atomic manipulations in each feature, there is a chance that Player I wins, i.e., at least one robust feature exists. Figure 13 illustrates this scenario on the GTSRB dataset. Here Player I defeats Player II through finding at least one robust feature by MCTS, and thus the convergence trend of the upper bound u FRΛ is not shown. As for the lower bound l FRΛ , Alpha-Beta Pruning enables Player II to manipulate a single pixel in Feature1 -Feature5 (see Figure 11b) so that adversarial examples are found. For instance, with L 1 distance above 0.79,  Feature1 turns out to be fragile.
Here, each iteration of MCTS or Alpha-Beta Pruning is dependent on the size of feature partitions -for smaller partitions it takes seconds to minutes, whilst for larger partitions it can take hours. The running times are also dependent on the norm ball radius d. If the radius d is small, the computation can always terminate in minutes.
Scalability wrt Number of Input Dimensions. We now investigate how the increase in the number of dimensions affects the convergence of the lower and upper bounds. From the complexity analysis of the problems in Section 4.3, we know that the theoretical complexity is in PTIME with respect to the size of the game model, which is exponential with respect to the number of input

dimensions.
We utilise the example in Figure 9, where the convergence of the upper bound u MSR and the lower bound l MSR in a cooperative game is exhibited on all the dimensions (pixels) of the MNIST image (index 67). We partition the image into 10 disjoint features using the grey-box extraction method, and gradually manipulate features, starting from those with fewer dimensions, to observe how the corresponding bound values u MSR , l MSR are affected if we fix a time budget. To ensure fair comparison, we run the same number of expansions of the game tree, i.e., 10 iterations of MCTS, and 1000 iterations of Admissible A*, and plot the bound values u MSR , l MSR thus obtained. Figure 14 shows the widening upper and lower bounds based on the L 2 norm with respect to 2 to 10 features of the image. It is straightforward to see that the conclusion also holds for the feature robustness problem.

Comparison with Existing Approaches for Generating Adversarial Exam-
ples When the game is cooperative, i.e., for the maximum safe radius problem, we can have adversarial examples as by-products. In this regard, both MCTS and A* algorithm can be applied to generate adversarial examples. Note that, for the latter, we can take Inadmissible A* (i.e., the heuristic function can be inadmissible), as the goal is not to ensure the lower bound but to find adversarial examples. By proportionally enlarging the heuristic distance heuristic(α ) with a constant, we ask the algorithm to explore those tree nodes where an adversarial example is more likely to be found. Figure 15 displays some adversarial MNIST, CIFAR10 and GTSRB images generated by DeepGame after manipulating a few pixels. More examples can be found in Figures A.17, A.18, and A.19 in the Appendix. Figure 15: Examples of adversarial MNIST, CIFAR10 and GTSRB images with slight perturbations based on the L 2 -norm. Top: "9" misclassified into "8"; "1" misclassified into "3". Middle: "frog" misclassified into "dog"; "dog" misclassified into "cat". Bottom: "speed limit 80" misclassified into "speed limit 60"; "danger" misclassified into "pedestrian crossing".
We compare our tool DeepGame with several state-of-the-art approaches to search for adversarial examples: CW [11], L0-TRE [17], DLV [13], SafeCV [23], and JSMA [10]. More specifically, we train neural networks on two benchmark datasets, MNIST and CIFAR10, and calculate the distance between the adversarial image and the original image based on the L 0 -norm. The original images, preprocessed to be within the bound [0, 1], are the first 1000 images of each testing set. Apart from a ten-minute time constraint, we evaluate on correctly classified images and their corresponding adversarial examples. This is because some tools regard misclassified images as adversarial examples and record zero-value distance while other tools do not, which would result in unfair comparison. The hardware environment is a Linux server with NVIDIA GeForce GTX TITAN Black GPUs, and the operating system is Ubuntu 14.04.3 LTS. Table 1 demonstrates the statistics. Figure A.17 and Figure A.18 in the Appendix include adversarial examples found by these tools. Model architectures, descriptions of the datasets and baseline methods, together with the parameter settings for these tools, can be found in Appendix A.

Evaluating Safety-Critical Networks
We explore the possibility of applying our game-based approach to support real-time decision making and testing, for which the algorithm needs to be highly efficient, requiring only seconds to execute a task.
We apply our method to a network used for classifying traffic light images collected from dashboard cameras. The Nexar traffic light challenge [22] made over eighteen thousand dashboard camera images publicly available. Each image We test the winner of the challenge which scored an accuracy above 90% [35]. Despite each input being 37632-dimensional (112 × 112 × 3), our algorithm reports that the manipulation of an average of 4.85 dimensions changes the network classification. We illustrate the results of our analysis of the network in Figure 16. Although the images are easy for humans to classify, only one pixel change causes the network to make potentially disastrous decisions, particularly for the case of red light misclassified as green.
To explore this particular situation in greater depth, we use a targeted safety MCTS procedure on the same 1000 images, aiming to manipulate images into green. We do not consider images which are already classified as green. Of the remaining 500 images, our algorithm is able to change all image classifications to green with worryingly low distances, namely an average L 0 of 3.23.

Related Work
In this section we review works related to safety and robustness verification for neural networks, Lipschitz constant estimation and feature extraction.

White-box Heuristic Approaches
In [8], Szegedy et. al. find a targeted adversarial example by running the L-BFGS algorithm, which minimises the L 2 distance between the images while maintaining the misclassification. Fast Gradient Sign Method (FGSM) [9], a refinement of L-BFGS, takes as inputs the parameters θ of the model, the input α to the model, and the target label y, and computes a linearized version of the cost function with respect to θ to obtain a manipulation direction. After the manipulation direction is fixed, a small constant value τ is taken as the magnitude of the manipulation. Carlini and Wagner [11] adapt the optimisation problem proposed in [8] to obtain a set of optimisation problems for L 0 , L 2 , and L ∞ attacks. They claim better performance than FGSM and Jacobianbased Saliency Map Attack (JSMA) with their L 2 attack, in which for every pixel x i a new real-valued variable w i is introduced and then the optimisation is conducted by letting x i move along the gradient direction of tanh(w i ). Instead of optimisation, JSMA [10] uses a loss function to create a "saliency map" of the image, which indicates the importance of each pixel on the network's decision. A greedy algorithm is used to gradually modify the most important pixels. In [36], an iterative application of an optimisation approach (such as [8]) is conducted on a set of images one by one to get an accumulated manipulation, which is expected to make a number of inputs misclassified. [37] replaces the softmax layer in a deep network with a multiclass SVM and then finds adversarial examples by performing a gradient computation.

White-box Verification Approaches
Compared to heuristic search for adversarial examples, verification approaches aim to provide guarantees on the safety of DNNs. An early verification approach [38] encodes the entire network as a set of constraints. The constraints can then be solved with a SAT solver. [12] improves on [38] by handling the ReLU activation functions. The Simplex method for linear programming is extended to work with the piecewise linear ReLU functions that cannot be expressed using linear programming. The approach can scale up to networks with 300 ReLU nodes. In recent work [39] the input vector space is partitioned using clustering and then the method of [12] is used to check the individual partitions. DLV [13] uses multi-path search and layer-by-layer refinement to exhaustively explore a finite region of the vector spaces associated with the input layer or the hidden layers, and scales to work with state-of-the-art networks such as VGG16. [16] shows that most known layers of DNNs are Lipschitz continuous and presents a verification approach based on global optimisation. DiffAI [40] is a method for training robust neural networks based on abstract interpretation, but is unable to calculate the maximum safe radius MSR.

Lipschitz Continuity
The idea of using Lipschitz continuity to provide guarantees on output behaviour of neural networks has been known for some time. Early work [14,15] focused on small neural networks (few neurons and layers) that only contain differentiable activation functions such as the sigmoid. These works are mainly concerned with the computation of a Lipschitz constant based on strong assumptions that the network has a number of non-zero derivatives and a finite order Taylor series expansion can be found at each vertex. In contrast, our approach assumes knowledge of a (not necessarily tight) Lipschtz constant and focuses on developing verification algorithms for realistically-sized modern networks that use ReLU activation functions, which are non-differentiable.

Lipschitz Constant Estimation
There has been a resurgence of interest in Lipschitz constant estimation for neural networks. The approaches of FastLin/FastLip [33] and Crown [34] aim to estimate the Lipschitz constant by considering the analytical form of the DNN layers. They are able to compute the bounds, but, in contrast to our approach, which gradually improves the bounds, are not able to improve them. Moreover, their algorithms require access to complete information (e.g., architecture, parameters, etc) about the DNN, while our approach is mainly "black-box" with a (not necessarily tight) Lipschitz constant. We remark that a loose Lipschitz constant can be computed quite easily, noting that a tighter constant can improve computational performance.
Although estimation of the Lipschitz constant has not been the focus of this paper, knowledge of the Lipschitz constant is important in safety verification of DNNs (i.e., estimation of MSR). The recent tool DeepGO [16] develops a dynamic Lipschitz constant estimation method for DNNs by taking advantage of advances in Lipschitzian optimisation, through which we can construct both lower and upper bounds for MSR with the guarantee of anytime convergence.

Maximum Safe Radius Computation
Recent approaches to verification for neural networks can also be used to compute bounds on the maximum safety radius directly for, say, L ∞ , by gradually enlarging the region. These works can be classified into two categories. The first concentrates on estimation of the lower bound of MSR using various techniques. For example, FastLin/FastLip [33] and Crown [34] employ layer-bylayer analysis to obtain a tight lower bound by linearly bounding the ReLU (i.e., FastLin/FastLip) or non-linear activation functions (i.e., Crown). Kolter&Wong [41,42], on the other hand, calculates the lower bound of MSR by taking advantage of robust optimisation. The second category aims to adapt abstract interpretation techniques to prove safety. For example, DeepZ and DeepPoly [43] (also including AI 2 ) adapt abstract interpretation to perform layer-by-layer analysis to over-approximate the outputs for a set of inputs, so that some safety properties can be verified, but are unable to prove absence of safety. A fundamental advantage of DeepGame compared to those works is that it can perform anytime estimation of MSR by improving both lower and upper bounds monotonically, even with a loose Lipschitz constant. Moreover, DeepGame provides a theoretical guarantee that it can reach the exact value of MSR.
Maximal radius computation for DNNs has been addressed directly in [44,45], where the entire DNN is encoded as a set of constraints, which are then solved by searching for valid solutions to the corresponding satisfiability or optimality problem. The approach of [44] searches for a bound on the maximal safety radius by utilising Reluplex and performing binary search, and [45] instead considers an MILP-based approach. In contrast, our approach utilises a Lipschitz constant to perform search over the input space. Further, our approach only needs to know the Lipschitz constant, whereas [44,45] need access to the DNN architecture and the trained parameters.

Black-box Algorithms
The methods in [46] evaluate a network by generating a synthetic data set, training a surrogate model, and then applying white box detection techniques on the model. [47] randomly searches the vector space around the input image for changes which will cause a misclassification. It shows that in some instances this method is efficient and able to indicate where salient areas of the image exist. [17] and this paper are black-box, except that grey-box feature extraction techniques are also considered in this paper to partition the input dimensions. L0-TRE [17] quantifies the global robustness of a DNN, where global robustness is the expectation of the maximum safe radius over a testing dataset, through iteratively generating lower and upper bounds on the network's robustness.

Feature Extraction Techniques
Feature extraction is an active area of research in machine learning, where the training data are usually sampled from real world problems and high dimensional. Feature extraction techniques reduce the dimensionality of the training data by using a set of features to represent an input sample. In this paper, feature extraction is used not for reducing dimensionality, but rather to partition the input dimensions into a small set of features. Feature extraction methods can be classified into those that are specific to the problem, such as the SIFT [18], SURF [48] and superpixels [32], which are specific to the object detection, and general methods, such as the techniques for computing for every input dimension its significance to the output [28]. The significance values can be visualised as a saliency map, as done in e.g., [10,17], but can also be utilised as in this paper to partition the input dimensions.

Conclusion
In this work, we present a two-player turn-based game framework for the verification of deep neural networks with provable guarantees. We tackle two problems, maximum safe radius and feature robustness, which essentially correspond to the absolute (pixel-level) and relative (feature-level) safety of a network against adversarial manipulations. Our framework can deploy various feature extraction or image segmentation approaches, including the saliencyguided grey-box mechanism, and the feature-guided black-box procedure. We develop a software tool DeepGame, and demonstrate its applicability on state-ofthe-art networks and dataset benchmarks. Our experiments exhibit converging upper and lower bounds, and are competitive compared to existing approaches to search for adversarial examples. Moreover, our framework can be utilised to evaluate robustness of networks in safety-critical applications such as traffic sign recognition in self-driving cars.

Appendix A.3. Baseline Methods
We choose a few well-established baseline methods that can perform stateof-the-art L 0 adversarial attacks. Their codes are all available on GitHub.
• CW 6 : a state-of-the-art adversarial attacking method, which models the attacking problem as an unconstrained optimization problem that is solvable by Adam optimizer in TensorFlow.
• L0-TRE 7 : a tensor-based robustness evaluation tool for the L0-norm, and its competitive L0 attack function is compared in this work.
• DLV 8 : an untargeted DNN verification method based on exhaustive search and MCTS.
• SafeCV 9 : a feature-guided safety verification work based on SIFT features, game theory, and MCTS.
• JSMA 10 : a targeted attack based on L 0 -norm, so we perform this attack in a sense that the adversarial examples are misclassified into all classes except the correct one.

Appendix A.4. Parameter Setting
MNIST and CIFAR-10 use the same settings, unless separately specified.