完备神经网络验证加速技术综述  

Survey on Acceleration Techniques for Complete Neural Network Verification

作　　者：刘宗鑫 杨鹏飞 张立军 吴志林[1,2] 黄小炜 LIU Zong-Xin;YANG Peng-Fei;ZHANG Li-Jun;WU Zhi-Lin;HUANG Xiao-Wei(State Key Laboratory of Computer Science(Institute of Software,Chinese Academy of Sciences),Beijing 100190,China;University of Chinese Academy of Sciences,Beijing 100049,China;University of Liverpool,Liverpool L693BX,UK)

机构地区：[1]计算机科学国家重点实验室(中国科学院软件研究所),北京100190 [2]中国科学院大学,北京100049 [3]University of Liverpool,Liverpool L693BX,UK

出　　处：《软件学报》2024年第9期4038-4068,共31页Journal of Software

基　　金：中国科学院基础领域研究青年团队计划(CASYSBR-040);中国科学院软件研究所新培育方向项目(ISCAS-PYFX-202201)。

摘　　要：人工智能技术已被广泛应用于生活中的各个领域.然而,神经网络作为人工智能的主要实现手段,在面对训练数据之外的输入或对抗攻击时,可能表现出意料之外的行为.在自动驾驶、智能医疗等安全攸关领域,这些未定义行为可能会对生命安全造成重大威胁.因此,使用完备验证方法证明神经网络的性质,保障其行为的正确性显得尤为重要.为了提高验证效率,各种完备神经网络验证工具均提出各自的优化方法,但并未充分探索这些方法真正起到的作用,后来的研究者难以从中找出最有效的优化方向.介绍神经网络验证领域的通用技术,并提出一个完备神经网络验证的通用框架.在此框架中,重点讨论目前最先进的工具在约束求解、分支选择与边界计算这3个核心部分上的所采用的优化方法.针对各个工具本身的性能和核心加速方法,设计一系列实验,旨在探究各种加速方式对于工具性能的贡献,并尝试寻找最有效的加速策略和更具潜力的优化方向,为研究者提供有价值的参考.Artificial intelligence(AI)has been widely applied to various aspects of lives.However,as the primary technique of realizing AI,neural networks can exhibit undefined behavior when faced with inputs outside of their training data or under adversarial attacks.In safety-critical fields such as autonomous driving and intelligent healthcare,undefined behavior can pose significant threats to human safety.Therefore,it is particularly crucial to employ complete verification methods to verify the properties of neural networks and ensure the correctness of the behavior.To enhance the verification efficiency,various complete neural network verification tools have proposed their optimization methods.However,the true influence of these methods has not been thoroughly explored,making it challenging for researchers to identify the most effective optimization directions.This paper introduces the common techniques in neural network verification and presents a universal framework for complete neural network verification.Within this framework,it focuses on discussing the optimization methods employed by state-of-the-art tools for constraint solving,branch selection,and boundary computation.Meanwhile,a series of experiments are designed to investigate the contributions of various acceleration techniques to the performance of each tool and to explore the most effective acceleration strategies and more promising optimization directions.Finally,valuable references can be provided for researchers in this field.

关 键 词：完备验证 可满足性模理论 人工智能安全 形式化方法 鲁棒性 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]