关键词：
深度神经网络
鲁棒性
形式化方法
剪枝
近似验证
摘要：
近年来,深度神经网络(Deep Neural Networks,简称DNN)技术广泛应用于智能驾驶、医疗诊断、航空航天和军事装备等安全攸关领域。于此同时,深度神经网络也被证明容易受到对抗样本等漏洞攻击手段的威胁,鲁棒性面临极大挑战。由于形式化验证可以对鲁棒性属性给出是否成立的确定性保证,因此,在深度神经网络鲁棒性保障研究方面受到了极大的关注。
目前,深度神经网络鲁棒性形式化验证研究仍然存在巨大挑战。一方面,验证方法的计算复杂度伴随着深度神经网络规模的增大而激增,导致难以验证大规模网络。另一方面,由于深度神经网络非线性的特征,验证方法很难实现对神经网络属性的精确计算。
针对当前研究中存在的问题,本文从两个角度提出鲁棒性验证优化方法。一是针对可验证神经网络规模提升,设计神经网络剪枝和重构方法,缩减待验证神经网络规模,提升验证方法可拓展性。二是针对验证方法计算精度提升,通过构建更加严格约束模型,实现了更加精确的神经网络近似验证方法。具体工作如下:
(1)提出了基于单样本剪枝和聚类的形式化精确验证方法优化。剪枝算法首先结合神经元覆盖率和符号边界传播方法来筛选深度神经网络对单样本进行识别时存在的冗余神经元,然后将此类神经元从待验证的神经网络中移除,得到剪枝后的子网络,最后通过验证此子网络的鲁棒性得到原网络在此样本下的鲁棒性。实验数据表明此方法可以有效缩减神经网络规模,并在误差极小的情况下提高验证算法的验证效率。此外,为解决存在大量待验证样本时需要剪枝大量子网络的问题,提出了对应的样本聚类算法。此算法通过不同样本间神经元覆盖率的相似性对样本进行聚类,聚类后的同类别样本可以使用相同的子网络进行鲁棒性验证。实验数据表明,根据同类别样本剪枝出的子网络规模得到了有效缩减。
(2)提出了基于双重神经元松弛的深度神经网络近似验证算法。该算法首先使用线性松弛方法构建深度神经网络的线性规划模型,然后向此模型中添加双神经元联合约束,来捕获同一隐藏层中不同神经元之间的依赖关系,实现更精确的神经元边界计算。此外,此工作设计了最大数量联合约束模型和最小数量联合约束模型两种验证方案,可以在计算精度和计算效率之间得到有效平衡。实验数据表明,此算法可以得到更精确的计算效果和鲁棒性验证能力。
欢迎来到三峡大学图书馆！
