Iteratively Enhanced Semidefinite Relaxations for Efficient Neural Network Verification
Iteratively Enhanced Semidefinite Relaxations for Efficient Neural Network Verification
复制标题
DOI：
10.1609/aaai.v37i12.26744
复制
发表时间：
2023-06
期刊：
影响因子：
--
通讯作者：
Jianglin Lan;Yang Zheng;A. Lomuscio
中科院分区：
文献类型：
--
作者：
Jianglin Lan;Yang Zheng;A. Lomuscio
我们提出了一种增强型半定程序(SDP)松弛算法，以实现对神经网络(NNS)的紧密而有效的验证。紧密性的改善是通过在先前提出的用于神经网络验证的现有SDP松弛中引入非线性约束来实现的。该方案的效率源于所提出算法的迭代性质，它通过递归地求解辅助凸层SDP问题来求解所得到的非凸SDP。我们形式化地证明了我们的算法生成的解比最新的基于SDP的解更紧凑。我们还证明了解序列收敛于非凸增强SDP松弛的最优解。在该领域的标准基准测试上的实验结果表明，我们的算法在保持可接受的计算代价的同时达到了最先进的性能。
We propose an enhanced semidefinite program (SDP) relaxation to enable the tight and efficient verification of neural networks (NNs). The tightness improvement is achieved by introducing a nonlinear constraint to existing SDP relaxations previously proposed for NN verification. The efficiency of the proposal stems from the iterative nature of the proposed algorithm in that it solves the resulting non-convex SDP by recursively solving auxiliary convex layer-based SDP problems. We show formally that the solution generated by our algorithm is tighter than state-of-the-art SDP-based solutions for the problem. We also show that the solution sequence converges to the optimal solution of the non-convex enhanced SDP relaxation. The experimental results on standard benchmarks in the area show that our algorithm achieves the state-of-the-art performance whilst maintaining an acceptable computational cost.