软件学报

作者：董彦松，刘月浩，董旭乾，赵亮，田聪，于斌，段振华

单位：董彦松，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007111,刘月浩，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007102,董旭乾，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007103,赵亮，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007104,田聪，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007105,于斌，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007106,段振华，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007107

关键词：神经网络;模型抽象;符号传播;线性近似;分治

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

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

来源：2024年第5期

《软件学报》期刊编辑部

查看软件学报杂志2024年第5期