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

arXiv: https://arxiv.org/abs/1807.03571 · HTML: https://mlsanity.com/paper/1807.03571/

## Key facts

- Cited by 33 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Jul 2018.

## Built on by (most cited first, 30 of 33)

- [A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation](https://mlsanity.com/paper/2305.11391/) (2023)
- [How to Certify Machine Learning Based Safety-critical Systems? A Systematic Literature Review](https://mlsanity.com/paper/2107.12045/) (2021)
- [VeriX: Towards Verified Explainability of Deep Neural Networks](https://mlsanity.com/paper/2212.01051/) (2022)
- [Robust Explanation Constraints for Neural Networks](https://mlsanity.com/paper/2212.08507/) (2022)
- [Convex Bounds on the Softmax Function with Applications to Robustness Verification](https://mlsanity.com/paper/2303.01713/) (2023)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [From Robustness to Explainability and Back Again](https://mlsanity.com/paper/2306.03048/) (2023)
- [The Vulnerability of Semantic Segmentation Networks to Adversarial Attacks in Autonomous Driving: Enhancing Extensive Environment Sensing](https://mlsanity.com/paper/2101.03924/) (2021)
- [Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning](https://mlsanity.com/paper/2101.10102/) (2021)
- [The Feasibility and Inevitability of Stealth Attacks](https://mlsanity.com/paper/2106.13997/) (2021)
- [Sparse Adversarial Video Attacks with Spatial Transformations](https://mlsanity.com/paper/2111.05468/) (2021)
- [Towards Verifying the Geometric Robustness of Large-scale Neural Networks](https://mlsanity.com/paper/2301.12456/) (2023)
- [A Survey on Verification and Validation, Testing and Evaluations of Neurosymbolic Artificial Intelligence](https://mlsanity.com/paper/2401.03188/) (2024)
- [Interpretation of Black Box NLP Models: A Survey](https://mlsanity.com/paper/2203.17081/) (2022)
- [Chess AI: Competing Paradigms for Machine Intelligence](https://mlsanity.com/paper/2109.11602/) (2021)
- [Reachability Analysis of Neural Network Control Systems](https://mlsanity.com/paper/2301.12100/) (2023)
- [Certified Policy Smoothing for Cooperative Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2212.11746/) (2022)
- [Adversarial Robustness Certification for Bayesian Neural Networks](https://mlsanity.com/paper/2306.13614/) (2023)
- [Fooling Object Detectors: Adversarial Attacks by Half-Neighbor Masks](https://mlsanity.com/paper/2101.00989/) (2021)
- [What, Indeed, is an Achievable Provable Guarantee for Learning-Enabled Safety Critical Systems](https://mlsanity.com/paper/2307.11784/) (2023)
- [When to Trust AI: Advances and Challenges for Certification of Neural Networks](https://mlsanity.com/paper/2309.11196/) (2023)
- [Adversarial Robustness of Deep Learning: Theory, Algorithms, and Applications](https://mlsanity.com/paper/2108.10451/) (2021)
- [Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks](https://mlsanity.com/paper/2302.06455/) (2023)
- [Abstraction and Symbolic Execution of Deep Neural Networks with Bayesian Approximation of Hidden Features](https://mlsanity.com/paper/2103.03704/) (2021)
- [The Care Label Concept: A Certification Suite for Trustworthy and Resource-Aware Machine Learning](https://mlsanity.com/paper/2106.00512/) (2021)
- [Model-Agnostic Reachability Analysis on Deep Neural Networks](https://mlsanity.com/paper/2304.00813/) (2023)
- [Perturbation-based Self-supervised Attention for Attention Bias in Text Classification](https://mlsanity.com/paper/2305.15684/) (2023)
- [A Roadmap for Robust End-to-End Alignment](https://mlsanity.com/paper/1809.01036/) (2018)
- [Permutation Invariance of Deep Neural Networks with ReLUs](https://mlsanity.com/paper/2110.09578/) (2021)
- [Patch Synthesis for Property Repair of Deep Neural Networks](https://mlsanity.com/paper/2404.01642/) (2024)

## Abstract (arXiv)

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.