通过交错孪生网络编码实现神经网络高效全局鲁棒性认证

深度神经网络的鲁棒性近来受到极大关注，尤其在部署于安全关键系统时，因为分析模型输出在输入扰动下的敏感度十分重要。尽管多数先前工作聚焦于输入样本周围的局部鲁棒性属性，对全局鲁棒性属性（其在整个输入空间上界定扰动下的最大输出变化）的研究仍然匮乏。本文中，我们将带 ReLU 激活函数的神经网络全局鲁棒性认证表述为混合整数线性规划（MILP）问题，并给出一种高效求解方法。我们的方法包含一种新颖的交错孪生网络编码方案，其中神经网络的两份副本被并排编码并加入额外的交错依赖，以及一种利用松弛与精化技术降低复杂度的过近似算法。实验证明了相较先前全局鲁棒性认证方法的时序效率以及我们过近似的紧致性。我们进行了闭环控制安全验证的案例研究，并展示了我们的方法在安全关键系统中认证神经网络全局鲁棒性的重要性与实用性。