神经网络可信性的形式化验证方法综述  

Review of the Formal Verification Methods for the Credibility of Neural Networks

作　　者：王莉 李晓娟[1,2] 关永[1,3] 王瑞[1,4] 王佳岳 WANG Li;LI Xiao-juan;GUAN Yong;WANG Rui;WANG Jia-yue(School of Information Engineering,Capital Normal University,Beijing 100048,China;High Reliable Embedded System Technology Beijing Engineering Research Center,Capital Normal University,Beijing 100048,China;Beijing Imaging Theory and Technology Advanced Innovation Center,Capital Normal University,Beijing 100048,China;Beijing Key Laboratory of Light Industrial Robot and Safety Verification,Capital Normal University,Beijing 100048,China)

机构地区：[1]首都师范大学信息工程学院,北京100048 [2]首都师范大学高可靠嵌入式系统技术北京市工程研究中心,北京100048 [3]首都师范大学北京成像理论与技术高精尖创新中心,北京100048 [4]首都师范大学轻型工业机器人与安全验证北京市重点实验室,北京100048

出　　处：《小型微型计算机系统》2022年第9期1830-1837,共8页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61977040,61876111)资助;科技创新服务能力建设(20530290073)-首都师范大学交叉研究院项目(19530012005)资助.

摘　　要：随着神经网络技术的不断发展和完善,其应用也随之扩展,如何保证其可信性是在许多应用领域特别是安全攸关应用中部署的关键,目前对神经网络可信性研究主要体现在通过循环优化网络训练等过程和对神经网络进行验证两方面.基于形式化方法可以对网络属性、核心算法进行严格的逻辑和模型表达并进行验证,本文利用形式化的方法对神经网络进行可信性验证的研究现状进行综述,对神经网络可信性问题的抽象、属性表达及形式验证进行阐述,并进一步对基于反例的验证、抽象解释、可满足性求解、输入/输出可达性分析等方法的核心算法、特点进行分类阐述和总结,对未来发展趋势进行展望.With the development and improvement of neural network technology,its applications have also expanded.How to ensure its credibility is the key to deployment in many application fields,especially credibility-critical applications.The current research on neural network credibility mainly reflects in the process of optimizing the network training through loops and verifying the neural network.Based on formal methods,network properties and core algorithms can be expressed and verified in strict logic and model.This paper uses formal methods to review the research status of credibility verification of neural networks,and expounds the abstraction,properties expression and formal verification of credibility problems of neural networks.Furthermore,the core algorithms and characteristics of such methods as verification based on counterexample,abstract interpretation,satisfiability solution and input/output accessibility analysis are classified and summarized,and the future development trend is forecasted.

关 键 词：神经网络 可信性属性 模型抽象 形式化方法 

分 类 号：TP389[自动化与计算机技术—计算机系统结构]