Towards Proving the Adversarial Robustness of Deep Neural Networks
Guy Katz Stanford University Clark Barrett Stanford University David L. Dill Stanford University Kyle Julian and Mykel J. Kochenderfer Stanford University {guyk, clarkbarrett, dill, kjulian3,
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.
中文速览
自动驾驶系统越来越多地依赖深度神经网络（DNN）来做决策，但这类网络像"黑盒子"一样难以被人工审查，而且一旦输入被微小扰动就可能产生错误分类——即所谓对抗样本（adversarial examples）——这对安全至关重要的场景构成严重威胁。作者团队提出并扩展了一种名为 Reluplex 的验证算法，通过将神经网络的线性方程组与 ReLU 非线性约束联合求解，能够形式化地证明或证伪网络的对抗鲁棒性（adversarial robustness），即在给定扰动范围内网络的分类结果不会发生改变。他们将这一方法应用于美国联邦航空局正在研发的机载防撞系统 ACAS Xu 的 45 个神经网络模型，给出了局部鲁棒性和全局鲁棒性两类属性的初步验证结果，其中全局鲁棒性因需同时搜索两个自由输入点而难度显著更高。这项工作填补了神经网络形式化验证在规模和精确性上的空白，为高安全性自动驾驶系统的认证提供了可落地的技术路径。
原文 arXiv:1709.02802;中英对照 + 大白话阅读 https://aha.fim.ai/paper/1709.02802v1