软件学报

作者：刘宗鑫，迟智名，赵梦宇，黄承超，黄小炜，蔡少伟，张立军，杨鹏飞

单位：刘宗鑫，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004911,迟智名，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004902,赵梦宇，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004903,黄承超，中国科学院大学南京学院, 江苏 南京 21113504,黄小炜，University of Liverpool, Liverpool L69 3BX, UK05,蔡少伟，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004906,张立军，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004907,杨鹏飞，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 10019008

关键词：可满足性模理论;深度神经网络;增量约束求解;局部鲁棒;形式化验证

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

约束求解是验证神经网络的基础方法. 在人工智能安全领域, 为了修复或攻击等目的, 常需要对神经网络的结构和参数进行修改. 面对此类需求, 提出神经网络的增量验证问题, 旨在判断修改后的神经网络是否仍保持安全性质. 针对这类问题, 基于Reluplex框架提出了一种增量可满足性模理论算法DeepInc. 该算法利用旧求解过程中关键计算格局的特征, 启发式地检查关键计算格局是否适用于证明修改后的神经网络. 实验结果显示, DeepInc的效率在大多数情况下都优于Marabou. 此外, 即使与最先进的验证工具α, β-CROWN相比, 对于修改前后均未满足预设安全性质的网络, DeepInc也实现了显著的加速.

来源：2025年第8期

《软件学报》期刊编辑部

查看软件学报杂志2025年第8期