A Game-Based Approximate Verification of Deep Neural Networks with Provable Guarantees

1. Introduction

• The maximum safe radius measures distance to the nearest adversarial example, while feature robustness measures whether perturbations restricted to selected features can control adversarial-example crafting.These correspond to absolute and relative safety radii, respectively.Source: §1 · p. 3
• Lipschitz continuity lets the authors reduce verification to finite optimisation over uniformly sampled inputs with an error bounded by the distance between samples.The approach covers modern networks with potentially non-differentiable layers such as ReLU.Source: §1 · p. 3
• Two-player turn-based games model feature selection and perturbation; the first player is cooperative for maximum safe radius and competitive for feature robustness.An anytime approach tightens upper and lower bounds, using Monte Carlo tree search for upper bounds and Admissible A* and Alpha-Beta Pruning for lower bounds.Source: §1 · p. 3
• The framework supports feature extraction methods including saliency-guided grey-box and SIFT-based black-box approaches.It is implemented in DeepGame2, with experiments reporting convergence of upper and lower bounds.Source: §1 · pp. 3–4
• The maximum-safe-radius upper-bound method is competitive with state-of-the-art heuristic methods on MNIST, CIFAR10, and GTSRB networks.The compared heuristic methods use white-box saliency matrices or sophisticated optimisation procedures and lack provable guarantees.Source: §1 · p. 4
• This paper extends from cooperative games and maximum-safe-radius upper bounds to feature robustness, competitive games, lower bounds, and detailed guarantees.The earlier evaluation used SIFT feature extraction.Source: §1 · p. 4

2. Preliminaries

• Inputs are vectors of dimensions normalized to [0, 1], with image dimensions corresponding to pixels and channels.For images, the domain is represented using width, height, and channel dimensions.Source: §2 · p. 4

2.1. Distance Metric and Lipschitz Continuity

• The framework measures perturbations with L_k metrics and defines a d-neighbourhood as inputs within distance d; its results extend to any metric but not L0.The authors focus on L1, L2, and L∞, and assume Lipschitz continuity, which holds for the bounded-input networks they consider.Source: §2.1 · p. 5

2.2. Input Manipulations

• Input manipulation operations alter selected dimensions by a specified magnitude and instruction, and any such operation can be implemented as a finite sequence of atomic single-dimension manipulations.Mapping one input to another through manipulation may incur an error bound because inputs are bounded real-valued vectors.Source: §2.2 · p. 6

2.3. Feature-Based Partitioning

• A feature extraction function partitions all input dimensions into disjoint feature sets; the framework can use suitable partitions beyond image classification.The experiments use saliency-guided grey-box and feature-guided black-box approaches for image classification.Source: §2.3 · p. 7

3. Problem Statement

• Pointwise robustness means a network’s classification remains invariant near a given input, making local safety the absence of nearby adversarial examples.The paper uses this notion to quantify the safety of a classification decision for a specific input.Source: §3 · p. 7

3.1. The Maximum Safe Radius Problem

• The maximum safe radius is the minimum distance from an input to an adversarial example, or equivalently the radius of its largest safe norm ball.The paper approximates this quantity using finite input manipulations because the adversarial-example search space may be infinite.Source: §3.1 · pp. 8–9
• Under Lipschitz continuity, a finite τ-grid yields an MSR estimate with error at most 1/2 d(k, τ), provided the grid satisfies a confidence-margin condition.The condition bounds grid spacing using the class confidence margin and the relevant Lipschitz constants.Source: §3.1 · pp. 9, 12, 13

3.2. The Feature Robustness Problem

• Feature robustness alternates between selecting features to maximize robustness and minimizing over perturbations within each selected feature; it is a relative radius for controlling adversarial-example existence.The paper also reduces this problem to finite optimisation using input manipulations.Source: §3.2 · pp. 14–15
• The relation between FRΛ, MSR, and the distance budget determines whether feature restrictions prevent, permit, or control adversarial examples.In the simpler FR′Λ example, d=10 and d′=4 yield FR′Λ=5, so restricting perturbations to Grass makes adversary existence controllable.Source: §3.2 · pp. 14–15
• When all τ-grid inputs are misclassification aggregators with respect to 1/2 d(k,τ), FRΛ(k, d, α, c) is at least FFRΛ(τ, k, d, α, c) − 1/2 d(k,τ).Source: §3.2 · p. 16
• 1/2 d(k,τ) bounds the error when FFRΛ(τ, k, d, α, c) estimates FRΛ(k, d, α, c), provided the stated grid condition holds.The condition requires d(k,τ) ≤ 2g(α′,N(α′)) max over competing classes c′ of (ℏN(α′)+ℏc′) for every τ-grid input α′. The bound depends linearly on grid-input prediction confidence and inversely on the network Lipschitz constants.Source: §3.2 · p. 17

4.1. Problem Solving as a Two-Player Turn-Based Game

• Player I selects a feature before Player II applies an atomic manipulation; Player I cooperates for maximum safe radius but competes for feature robustness.Player II minimizes distance to an adversarial example in both games.Source: Figure 6 · p. 18, §4.1 · p. 20

4.2. Safety Guarantees via Optimal Strategy

• The game value equals the corresponding finite optimisation value for both maximum safe radius and feature robustness.The resulting approximation has error bound 1/2 d(k, τ) when the stated condition on τ holds.Source: §4.2 · pp. 20–21
• The game value can be achieved with deterministic, memoryless strategies for Player I in both objectives.Source: §4.2 · p. 21

4.3. Complexity of the Problem

• Solving the game takes time polynomial in d/τ but exponential in the number of input dimensions n.Source: §4.3 · p. 22

5.1. Upper Bounds: Monte Carlo Tree Search (MCTS)

• MCTS estimates upper bounds for both games by expanding a partial game tree and simulating plays until termination.Its bounds improve monotonically, and the search converges when the finite tree is fully explored.Source: §5.1 · pp. 23–24, §5.4 · pp. 28–29

5.2. Lower Bounds: Admissible A* in a Cooperative Game

• Admissible A* computes lower bounds for the cooperative maximum safe radius game using a heuristic that does not overestimate the cost to a terminal state.The heuristic is derived from the minimum confidence margin and Lipschitz constants.Source: §5.2 · p. 25

5.3. Lower Bounds: Alpha-Beta Pruning in a Competitive Game

• Alpha-Beta Pruning computes lower bounds for the competitive feature robustness game by tracking Player I's maximum and Player II's minimum rewards.It prunes remaining Player II strategies when the current bounds show they cannot affect the result.Source: §5.3 · pp. 27–28

5.4. Anytime Convergence

• The approach can terminate MCTS after a chosen number of iterations without improvement or when a time limit is reached.Full expansion guarantees convergence but may take prohibitively long.Source: §5.4 · p. 28
• Lower bounds improve monotonically as the algorithms expand the game tree to greater depths.Source: §5.4 · pp. 28–29

6.1. Feature-Based Partitioning

• The experiments illustrate saliency-based partitioning, SIFT, and K-means superpixels; saliency ranks pixel sensitivities into disjoint sets.The approach can use varied feature partitioning methods.Source: Figure 8 · p. 30, §6.1 · pp. 30–31

6.2. Lipschitz Constant Estimation

• Verification assumes a known Lipschitz constant, whose size affects computational performance through the grid-point and error-bound trade-off.Even with the constant known, high-dimensional, highly nonlinear networks remain nontrivial to verify.Source: §6.2 · p. 31

6.3. Convergence Analysis of the Upper and Lower Bounds

• On MNIST, MCTS found an adversarial example at L2 distance 2.84, while Admissible A* established safety within radius 0.012.The bounds descend and ascend, respectively, as the cooperative-game search proceeds.Source: §6.3 · pp. 31–32, Figure 9 · p. 31
• On CIFAR10, after three iterations all features were fragile above L2 distance 1.75, while at 0.48 at least one feature was robust.The upper bound successively improved from 2.38 to 1.94 to 1.75 as MCTS explored different features.Source: §6.3 · p. 33, Figure 12 · p. 34
• On GTSRB, Alpha-Beta Pruning found that manipulating one pixel in Features 1–5 yields adversarial examples; Feature1 is fragile above L1 distance 0.79.The competitive-game example has a robust feature, so the upper-bound convergence trend is not shown.Source: §6.3 · pp. 33–34, Figure 13 · p. 34
• With a fixed search budget, the L2 upper and lower bounds widened as feature count increased from 2 to 10; larger partitions can take hours per iteration.Smaller partitions take seconds to minutes, and small norm-ball radii can permit termination within minutes.Source: §6.3 · pp. 34–35, Figure 14 · p. 35

6.4. Comparison with Existing Approaches for Generating Adversarial Examples

• The adversarial-search comparison evaluates DeepGame against CW, L0-TRE, DLV, SafeCV, and JSMA on MNIST and CIFAR10 using L0 distance and a ten-minute limit.The supplied passages describe the comparison setup but do not report its outcome values.Source: §6.4 · p. 36, Table 1 · p. 37

6.5. Evaluating Safety-Critical Networks

• On Nexar traffic-light images, changing an average of 4.85 dimensions altered classifications; targeted search changed all 500 non-green images to green at average L0 3.23.The authors also report one-pixel changes causing potentially disastrous red-to-green misclassifications.Source: §6.5 · p. 37

7.1. White-box Heuristic Approaches

• White-box heuristic attacks use gradients, saliency maps, or optimization; Carlini–Wagner adapts L-BFGS for L0, L2, and L∞ attacks, while JSMA greedily changes salient pixels.These methods search for adversarial examples rather than providing verification guarantees.Source: §7.1 · pp. 37–38

7.2. White-box Verification Approaches

• White-box verification encodes networks as constraints or analyzes layer outputs; cited methods include SAT, ReLU-aware solving, DLV, and abstract interpretation.DiffAI trains robust networks but cannot calculate maximum safe radius.Source: §7.2 · pp. 38–39

7.3. Lipschitz Continuity

• Earlier Lipschitz verification work focused on small differentiable networks under assumptions about nonzero derivatives and finite Taylor expansions; this paper instead considers modern ReLU networks.Its approach assumes a Lipschitz constant rather than requiring differentiable activations.Source: §7.3 · p. 39

7.4. Lipschitz Constant Estimation

• FastLin/FastLip and Crown estimate Lipschitz constants from network layers, whereas DeepGame assumes a possibly loose constant and incrementally improves bounds.The cited estimators require complete network information; DeepGame is described as mainly black-box.Source: §7.4 · p. 39

7.5. Maximum Safe Radius Computation

• For maximum safe radius, DeepGame monotonically improves upper and lower bounds and has a theoretical guarantee of reaching the exact value.Other cited approaches use layer bounds, robust optimization, abstract interpretation, or constraint-solving search.Source: §7.5 · pp. 39–40

7.6. Black-box Algorithms

• Black-box approaches include surrogate-model detection, random local search, and L0-TRE, which estimates dataset-level robustness from bounds on maximum safe radius.The paper also considers grey-box feature extraction to partition input dimensions.Source: §7.6 · p. 40

7.7. Feature Extraction Techniques

• Here, feature extraction partitions input dimensions into features rather than reducing training-data dimensionality; methods include SIFT, superpixels, and significance-based saliency maps.The paper uses the resulting partitions in robustness analysis.Source: §7.7 · p. 40

8. Conclusion

• DeepGame addresses absolute pixel-level safety through maximum safe radius and relative feature-level safety through feature robustness.The framework supports saliency-guided grey-box and feature-guided black-box procedures.Source: §8 · p. 41
• Experiments on benchmark datasets show converging upper and lower bounds, and adversarial-example search competitive with existing approaches.Source: §8 · p. 41
• The framework is applicable to evaluating network robustness in safety-critical settings such as traffic-sign recognition in self-driving cars.Source: §8 · p. 41

Appendix A.1. Model Architectures

• Table A.2 lists architectures for the MNIST, CIFAR-10, and GTSRB models.Source: Table A.2 · p. 46
• The appendix reports MNIST at 99.99% on 60,000 images and CIFAR-10 at 99.83% on 50,000 images.Source: Appendix A.1 · p. 46
• A second reported set gives MNIST at 99.36% on 10,000 images and CIFAR-10 at 78.30% on 10,000 images.Source: Appendix A.1 · p. 46

• The experiments compare methods on MNIST and CIFAR-10, benchmark datasets widely used by the baselines.Source: Appendix A.2 · p. 46
• MNIST has 60,000 training and 10,000 test images of size-normalised, centred handwritten digits.Source: Appendix A.2 · p. 46
• CIFAR-10 contains 60,000 colour images across 10 classes, split into 50,000 training and 10,000 test images.The images are 32×32 pixels.Source: Appendix A.2 · p. 46

• The selected baselines are established methods for state-of-the-art L0 adversarial attacks, with code available on GitHub.Source: Appendix A.3 · p. 47
• CW models adversarial attack generation as unconstrained optimization solved with the Adam optimizer in TensorFlow.Source: Appendix A.3 · p. 47
• L0-TRE is a tensor-based L0 robustness evaluation tool, and its competitive L0 attack function is compared.Source: Appendix A.3 · p. 47
• DLV is an untargeted DNN verification method based on exhaustive search and Monte Carlo tree search.Source: Appendix A.3 · p. 47
• SafeCV is a feature-guided safety verification method using SIFT features, game theory, and Monte Carlo tree search.Source: Appendix A.3 · p. 47
• JSMA is a targeted L0 attack evaluated by seeking adversarial examples misclassified into every class except the correct one.Source: Appendix A.3 · p. 47

• MNIST and CIFAR-10 use the same settings unless otherwise specified.Source: Appendix A.4 · p. 47
• The game is cooperative with an upper-bound objective, A* algorithm, L0 radius 30, and τ = 1.Source: Appendix A.4 · p. 47
• The attack is untargeted, with learning rate 0.1 and a maximum of 100 iterations.Source: Appendix A.4 · p. 47
• The SIFT two-player MCTS uses 150 one-dimensional features and time limits of 30 seconds per level and 120 seconds overall.It uses 5 multi-samples for MNIST and 3 for CIFAR-10.Source: Appendix A.4 · p. 48
• Manipulation uses max manip on MNIST and white manipulation on CIFAR-10, with simulation cutoffs of 75 and 100, respectively.The visit and backtracking constants are both 1, and small image is enabled.Source: Appendix A.4 · p. 48

Appendix A.5. Platforms

• The listed platforms include an NVIDIA GeForce GTX TITAN Black GPU and an Intel Core i5-4690S CPU, running Ubuntu 14.04.3 or Fedora 26.The software list also names Anaconda and PyCharm.Source: Appendix A.5 · p. 48

Appendix A.6. Adversarial Images

• The MNIST and CIFAR-10 figures compare original images with outputs from DeepGame, CW, L0-TRE, DLV, SafeCV, and JSMA.Source: Figure A.17 · p. 49, Figure A.18 · p. 50
• A separate figure presents adversarial GTSRB images generated by DeepGame.Source: Figure A.19 · p. 51