Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming
Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming
复制标题
DOI：
10.1109/tac.2020.3046193
复制
发表时间：
2022-01-01
影响因子：
6.8
通讯作者：
Pappas, George J.
中科院分区：
文献类型：
--
作者：
Fazlyab, Mahyar;Morari, Manfred;Pappas, George J.
证明神经网络对输入不确定性和对抗性攻击的安全性或鲁棒性是安全机器学习和控制领域的一个新兴挑战。为了提供这样的保证，当神经网络的输入在有界集合内变化时，必须能够约束神经网络的输出。在这篇文章中，我们提出了一个半定规划（SDP）框架来解决这个问题的前馈神经网络与一般的激活函数和输入不确定性集。我们的主要思想是抽象激活函数的各种属性（例如，单调性、有界斜率、有界值和跨层重复）与二次约束的形式主义。然后，我们通过S-过程和SDP分析抽象网络的安全性。我们的框架跨越保守性和计算效率之间的权衡，并适用于安全验证以外的问题。我们通过各种大小的数值问题实例来评估我们的方法的性能。
Certifying the safety or robustness of neural networks against input uncertainties and adversarial attacks is an emerging challenge in the area of safe machine learning and control. To provide such a guarantee, one must be able to bound the output of neural networks when their input changes within a bounded set. In this article, we propose a semidefinite programming (SDP) framework to address this problem for feed-forward neural networks with general activation functions and input uncertainty sets. Our main idea is to abstract various properties of activation functions (e.g., monotonicity, bounded slope, bounded values, and repetition across layers) with the formalism of quadratic constraints. We then analyze the safety properties of the abstracted network via the S-procedure and SDP. Our framework spans the tradeoff between conservatism and computational efficiency and applies to problems beyond safety verification. We evaluate the performance of our approach via numerical problem instances of various sizes.