基于多路径回溯的神经网络验证方法  

Multi-path Back-propagation Method for Neural Network Verification

作　　者：郑烨 施晓牧 刘嘉祥 ZHENG Ye;SHI Xiao-Mu;LIU Jia-Xiang(College of Computer Science and Software Engineering,Shenzhen University,Shenzhen 518060,China)

机构地区：[1]深圳大学计算机与软件学院,广东深圳518060

出　　处：《软件学报》2022年第7期2464-2481,共18页Journal of Software

基　　金：深圳市高等院校稳定支持计划(20200810045225001);国家自然科学基金(62002228);深圳市科创委基础研究项目(JCYJ20210324094202008)

摘　　要：基于线性抽象的符号传播方法在神经网络验证中具有重要地位.针对这类方法,提出了多路径回溯的概念.现有方法可看作仅使用单条回溯路径计算每个神经网络节点的上下界,是这一概念的特例.使用多条回溯路径,可以有效地改善这类方法的精度.在数据集ACAS Xu,MNIST和CIFAR10上,将多路径回溯方法与使用单条回溯路径的Deep Poly进行定量比较,结果表明,多路径回溯方法能够获得明显的精度提升,而仅引入较小的额外时间代价.此外,在数据集MNIST上,将多路径回溯方法与使用全局优化的Optimized LiRPA比较,结果表明,该方法仍然具有精度优势.Symbolic propagation methods based on linear abstraction play a significant role in neural network verification.This study proposes the notion of multi-path back-propagation for these methods.Existing methods are viewed as using only a single back-propagation path to calculate the upper and lower bounds of each node in a given neural network,being specific instances of the proposed notion.Leveraging multiple back-propagation paths effectively improves the accuracy of this kind of method.For evaluation,the proposed method is quantitatively compared using multiple back-propagation paths with the state-of-the-art tool DeepPoly on benchmarks ACAS Xu,MNIST,and CIFAR10.The experiment results show that the proposed method achieves significant accuracy improvement while introducing only a low extra time cost.In addition,the multi-path back-propagation method is compared with the Optimized LiRPA based on global optimization,on the dataset MNIST.The results show that the proposed method still has an accuracy advantage.

关 键 词：神经网络验证 符号传播 抽象解释 多路径回溯 

分 类 号：TP183[自动化与计算机技术—控制理论与控制工程]