软件学报

作者：刘宗鑫，杨鹏飞，张立军，吴志林，黄小炜

单位：刘宗鑫，计算机科学国家重点实验室 (中国科学院 软件研究所 ), 北京 100190;中国科学院大学, 北京 10004911,杨鹏飞，计算机科学国家重点实验室 (中国科学院 软件研究所 ), 北京 10019002,张立军，计算机科学国家重点实验室 (中国科学院 软件研究所 ), 北京 100190;中国科学院大学, 北京 10004903,吴志林，计算机科学国家重点实验室 (中国科学院 软件研究所 ), 北京 100190;中国科学院大学, 北京 10004904,黄小炜，University of Liverpool, Liverpool L69 3BX, UK05

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

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

人工智能技术已被广泛应用于生活中的各个领域. 然而, 神经网络作为人工智能的主要实现手段, 在面对训练数据之外的输入或对抗攻击时, 可能表现出意料之外的行为. 在自动驾驶、智能医疗等安全攸关领域, 这些未定义行为可能会对生命安全造成重大威胁. 因此, 使用完备验证方法证明神经网络的性质, 保障其行为的正确性显得尤为重要. 为了提高验证效率, 各种完备神经网络验证工具均提出各自的优化方法, 但并未充分探索这些方法真正起到的作用, 后来的研究者难以从中找出最有效的优化方向. 介绍神经网络验证领域的通用技术, 并提出一个完备神经网络验证的通用框架. 在此框架中, 重点讨论目前最先进的工具在约束求解、分支选择与边界计算这3个核心部分上的所采用的优化方法. 针对各个工具本身的性能和核心加速方法, 设计一系列实验, 旨在探究各种加速方式对于工具性能的贡献, 并尝试寻找最有效的加速策略和更具潜力的优化方向, 为研究者提供有价值的参考.

来源：2024年第9期

《软件学报》期刊编辑部

查看软件学报杂志2024年第9期