随着神经网络技术的快速发展, 其在自动驾驶、智能制造、医疗诊断等安全攸关领域得到了广泛应用, 神经网络的可信保障变得至关重要. 然而, 由于神经网络具有脆弱性, 轻微的扰动经常会导致错误的结果, 因此采用形式化验证的手段来保障神经网络安全可信是非常重要的. 目前神经网络的验证方法主要关注分析的精度, 而易忽略运行效率. 在验证一些复杂网络的安全性质时, 较大规模的状态空间可能会导致验证方法不可行或者无法求解等问题. 为了减少神经网络的状态空间, 提高验证效率, 提出一种基于过近似误差分治的神经网络形式化验证方法. 该方法利用可达性分析技术计算非线性节点的上下界, 并采用一种改进的符号线性松弛方法减少了非线性节点边界计算过程中的过近似误差. 通过计算节点过近似误差的直接和间接影响, 将节点的约束进行细化, 从而将原始验证问题划分为一组子问题, 其混合整数规划(MILP)公式具有较少的约束数量. 所提方法已实现为工具NNVerifier, 并通过实验在经典的3个数据集上训练的4个基于ReLU的全连接基准网络进行性质验证和评估. 实验结果表明, NNVerifier的验证效率比现有的完备验证技术提高了37.18%.

With the rapid development of neural network technology, neural networks have been widely applied in safety-critical fields such as autonomous driving, intelligent manufacturing, and medical diagnosis. Thus, it is crucial to ensure the trustworthiness of neural networks. However, due to the vulnerability of neural networks, slight perturbation often leads to wrong results. Therefore, it is vital to use formal verification methods to ensure the safety and trustworthiness of neural networks. Current verification methods for neural networks are mainly concerned with the accuracy of the analysis, while apt to ignore operational efficiency. When verifying the safety properties of complex networks, the large-scale state space may lead to problems such as infeasibility or unsolvability. To reduce the state space of neural networks and improve the verification efficiency, this study presents a formal verification method for neural networks based on divide and conquer considering over-approximation errors. The method uses the reachability analysis technique to calculate the upper and lower bounds of nonlinear nodes and uses an improved symbolic linear relaxation method to reduce over-approximation errors during the boundary calculation of nonlinear nodes. The constraints of nodes are refined by calculating the direct and indirect effects of their over-approximation errors. Thereby, the original verification problem is split into a set of sub-problems whose mixed integer linear programming (MILP) formulation has a smaller number of constraints. The method is implemented as a tool named NNVerifier, whose properties are verified and evaluated through experiments on four ReLU-based fully-connected benchmark networks trained on three classic datasets. The experimental results show that the verification efficiency of the NNVerifier is 37.18% higher than that of the existing complete verification methods.

国家重点研发计划(2018AAA0103202);国家自然科学基金(62192734,62172322)