一句话：提出结合浮点多面体与区间的抽象域 DeepPoly，实现对深度神经网络可扩展且精确的认证。
该论文研究深度神经网络的可扩展、精确认证问题。其核心贡献是提出一种新的抽象域，将浮点多面体与区间相结合，并针对神经网络场景定制抽象变换器，具体包括仿射变换、ReLU、sigmoid、tanh 与 maxpool 的变换器。作者在名为 DeepPoly 的系统中实现了该方法，并在多个数据集、网络架构（含防御网络）和规范上进行了广泛评估。实验表明，DeepPoly 比先前工作更精确，同时能扩展到大型网络。论文还展示了如何将 DeepPoly 与基于 trace partitioning 的抽象精化相结合，从而首次证明网络在输入图像经受旋转等采用线性插值的复杂扰动时仍具有鲁棒性。
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.
@article{paperbot646,
title = {An abstract domain for certifying neural networks},
author = {Gagandeep Singh and Timon Gehr and Markus Püschel and Martin Vechev},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290354}
}