PEREGRiNN：惩罚松弛贪婪神经网络验证器

神经网络（NNs）在实际应用中的普及使其安全影响日益显著：无论是非预期的还是对抗性的误分类都可能导致致命后果。因此，形式化验证技术已被认为是安全神经网络设计与部署的关键。本文提出一种新方法，用于形式化验证 ReLU 神经网络最常考虑的安全规范——即网络输入与输出的多胞形规范。与其他一些方法类似， ours 使用松弛凸规划来缓解问题的组合复杂性。然而，我们方法的独特之处在于将凸求解器不仅用作线性可行性检查器，还用作惩罚解中允许松弛程度的手段。具体而言，我们用通常的线性约束对每个 ReLU 进行编码，并将其与惩罚每个神经元输出与其松弛之间差异的凸目标函数相结合。该凸函数被进一步构造为迫使最大松弛出现在最靠近输入层的位置；这带来了额外好处，即在逐层条件化时，最具问题的神经元尽可能早地被条件化。该范式可用于创建一种验证算法，其不仅总体上快于竞争方法，还能验证相当更多的安全性质；我们在标准 MNIST 鲁棒性验证套件上评估了 PEREGRiNN 以证实这些主张。