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