Towards Proving the Adversarial Robustness of Deep Neural Networks
Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer
TL;DR
The paper addresses proving adversarial robustness for deep neural networks used as controllers in autonomous vehicles, proposing Reluplex as a scalable verification tool that handles ReLU constraints alongside linear relations. It explores local and global robustness definitions, reports initial results on the ACAS Xu network family, and analyzes scalability challenges. The authors advocate a practical hybrid local robustness notion and outline parallelization and future integration with reachability analysis to extend verification to larger, real-world networks. This work lays groundwork for certifying safety-critical DNN controllers by combining specialized verification techniques with parallel computation and system-level analysis.
Abstract
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.