An Abstract Domain for Certifying Neural Networks
An Abstract Domain for Certifying Neural Networks
复制标题
DOI：
10.1145/3290354
复制
发表时间：
2019-01-01
影响因子：
1.8
通讯作者：
Vechev, Martin
中科院分区：
文献类型：
--
作者：
Singh, Gagandeep;Gehr, Timon;Vechev, Martin
我们提出了一种新的可伸缩的、精确的深度神经网络验证方法。我们方法背后的关键技术见解是一个新的抽象域，它结合了浮点多面体和区间，并配备了专门为神经网络设置量身定做的抽象转换器。具体地说，我们引入了新的仿射变换、校正线性单元(RELU)、Sigmoid、tanh和MaxPool函数。我们在一个名为DeepPoly的系统中实现了我们的方法，并在一系列数据集、神经体系结构(包括防御网络)和规范上对其进行了广泛的评估。实验结果表明，DeepPoly在扩展到大型网络时比以前的工作更精确，并展示了如何将DeepPoly与一种基于踪迹划分的抽象求精相结合。这使我们能够第一次证明，当输入图像受到复杂的扰动时，网络的稳健性，例如使用线性内插的旋转。
We present a novel method for scalable and precise certification of deep neural networks. The key technical insight behind our approach is a new abstract domain which combines floating point polyhedra with intervals and is equipped with abstract transformers specifically tailored to the setting of neural networks. Concretely, we introduce new transformers for affine transforms, the rectified linear unit (ReLU), sigmoid, tanh, and maxpool functions.We implemented our method in a system called DeepPoly and evaluated it extensively on a range of datasets, neural architectures (including defended networks), and specifications. Our experimental results indicate that DeepPoly is more precise than prior work while scaling to large networks.We also show how to combine DeepPoly with a form of abstraction refinement based on trace partitioning. This enables us to prove, for the first time, the robustness of the network when the input image is subjected to complex perturbations such as rotations that employ linear interpolation.