Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encoding

Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encoding
复制标题

DOI:
10.48550/arxiv.2203.14141
复制
发表时间:
2022-03
期刊:
2022 Design, Automation & Test in Europe Conference & Exhibition (DATE)
影响因子:
--
通讯作者:
Zhilu Wang;Chao Huang;Qi Zhu
Zhilu Wang;Chao Huang;Qi Zhu
中科院分区:
其他
文献类型:
--
作者:
Zhilu Wang;Chao Huang;Qi Zhu

文献摘要

被引文献

相似文献

深度神经网络的鲁棒性最近引起了人们的极大兴趣,特别是在部署在安全关键系统中时,因为分析模型输出在输入扰动下的敏感程度非常重要。虽然之前的大多数工作都集中在输入样本周围的局部鲁棒性,但仍然缺乏对全局鲁棒性的研究,该鲁棒性限制了整个输入空间扰动下的最大输出变化。在这项工作中,我们将具有 ReLU 激活函数的神经网络的全局鲁棒性证明制定为混合整数线性规划 (MILP) 问题,并提出了一种有效的方法来解决它。我们的方法包括一种新颖的交错双网络编码方案,其中神经网络的两个副本并排编码,并在它们之间添加额外的交错依赖性,以及利用松弛和细化技术来降低复杂性的过近似算法。实验证明了与之前的全局鲁棒性认证方法相比,我们工作的计时效率以及我们的过度近似的严格性。进行了闭环控制安全验证的案例研究,并证明了我们的方法在验证安全关键系统中神经网络的全局鲁棒性方面的重要性和实用性。
The robustness of deep neural networks has received significant interest recently, especially when being deployed in safety-critical systems, as it is important to analyze how sensitive the model output is under input perturbations. While most previous works focused on the local robustness property around an input sample, the studies of the global robustness property, which bounds the maximum output change under perturbations over the entire input space, are still lacking. In this work, we formulate the global robustness certification for neural networks with ReLU activation functions as a mixed-integer linear programming (MILP) problem, and present an efficient approach to address it. Our approach includes a novel interleaving twin-network encoding scheme, where two copies of the neural network are encoded side-by-side with extra interleaving dependencies added between them, and an over-approximation algorithm leveraging relaxation and refinement techniques to reduce complexity. Experiments demonstrate the timing efficiency of our work when compared with previous global robustness certification methods and the tightness of our over-approximation. A case study of closed-loop control safety verification is conducted, and demonstrates the importance and practicality of our approach for certifying the global robustness of neural networks in safety-critical systems.