Towards Proving the Adversarial Robustness of Deep Neural Networks

By Guy Katz, Clark W. Barrett, David L. Dill, Kyle D. Julian, Mykel J. Kochenderfer. 2017

128 citations recorded by the source corpus.

Autonomous vehicles are highly complex systems, required to function reliably in a wide variety of situations. Manually crafting software controllers for these vehicles is difficult, but there has been some success in using deep neural networks generated using machine-learning. However, deep neural networks are opaque to human engineers, rendering their correctness very difficult to prove manually; and existing automated techniques, which were not designed to operate on neural networks, fail to scale to large systems. This paper focuses on proving the adversarial robustness of deep neural networks, i.e. proving that small perturbations to a correctly-classified input to the network cannot cause it to be misclassified. We describe some of our recent and ongoing work on verifying the adversarial robustness of networks, and discuss some of the open questions we have encountered and how they might be addressed.

Subfields: Artificial Intelligence, Emergency Medicine, Safety, Robustness & Interpretability

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Emergency Medicine

In Safety, Robustness & Interpretability

Citations in the corpus

Efficient Formal Safety Analysis of Neural Networks (2018, background): “Several researchers have tried to extend and customize Satisfiability Modulo Theory (SMT) solvers, which have been very successful at verifying different properties of traditional software, for estimating decision boundaries with strong guarantees [13, 14, 11, 7, 25].”
Certified Defenses against Adversarial Examples (2018, methodology): “Another approach is to compute the worst-case perturbation exactly using discrete optimization (Katz et al., 2017a; Carlini (a) (b) Figure 1: Illustration of the margin function f ( x ) for a simple two-layer network.”
Lipschitz-Margin Training: Scalable Certification of Perturbation Invariance for Deep Neural Networks (2018, methodology): “[14, 13] reduced the problem to Satisfiability Modulo Theory, and Raghunathan et al.”
Ground-Truth Adversarial Examples (2017, background): “Veriﬁcation techniques can be used to ﬁnd adversarial examples for a given input point and some allowed amount of distortion, but they tend to be signiﬁcantly slower than gradient-based techniques [11, 12, 18].”
AI Safety Gridworlds (2017, background): “, 2017), formal verification (Seshia et al., 2016; Huang et al., 2017b; Katz et al., 2017), scalable oversight and reward learning problems (Amodei et al.”
Semidefinite relaxations for certifying robustness to adversarial examples (2018, methodology): “The second category draws techniques from formal verification such as SMT [16, 17, 7, 14], which aim to provide tight certificates for any network using discrete optimization.”
Transformers in Medical Imaging: A Survey (2022, background): “Furthermore, theoretical understanding to provide guarantees about the performance and robustness of ViTs, like CNNs [417], can be of significant interest to medical imaging researchers.”
Review of Artificial Intelligence Adversarial Attack and Defense Technologies (2019, methodology): “In the articles [31,32], they replaced DNN in MalGAN with RNN.”
DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks (2017, methodology): “2 is checked independently for every l′, these queries can also be performed in parallel — expediting the process even further [12].”
Provably Minimally-Distorted Adversarial Examples (2017, methodology): “Veriﬁcation techniques can be used to ﬁnd adversarial examples for a given input point and some allowed amount of distortion, but they tend to be sig-niﬁcantly slower than gradient-based techniques (Katz et al., 2017b; Pulina and Tacchella, 2012; Katz et al., 2017a).”
Towards Robust CNN-based Object Detection through Augmentation with Synthetic Rain Variations (2019, background): “of robustness is currently impossible for larger networks [4].”
Certifiable Distributional Robustness with Principled Adversarial Training (2017, background): “On the other hand, verification of deep networks using SMT solvers [24, 25, 22] provides formal guarantees on robustness but is NP-hard in general; this approach requires prohibitive computational expense even on small networks.”
Benchmarking Neural Network Robustness to Common Corruptions and Surface Variations (2018, background): “In efforts to ground adversarial robustness research, several competing robustness measures have been introduced [3, 8, 9, 44, 33].”
The Marabou Framework for Verification and Analysis of Deep Neural Networks (2019, methodology): “The Marabou project builds upon our previous work on the Reluplex project [2,7,12,13,15,17], which focused on applying SMT-based techniques to the veriﬁcation of DNNs. Marabou follows the Reluplex spirit in that it applies an SMT-based, lazy search technique: it iteratively searches for an…”