Page 22 - 《软件学报》2025年第8期

刘宗鑫 等: 神经网络的增量验证 3445

can be applied to prove the correctness of the modified DNN. Experimental results demonstrate that DeepInc outperforms Marabou in
terms of efficiency in most cases. Moreover, for cases where the safety property is violated both before and after modification, DeepInc
achieves significantly faster performance, even when compared to the state-of-the-art verifier α, β-CROWN.
Key words: satisfiability module theory; deep neural network (DNN); incremental constraint solving; local robustness; formal verification
过去几年间, 神经网络在计算机视觉, 自然语言处理等多个领域取得了革命性的进展. 然而, 神经网络在安全
攸关领域的应用仍受到其可靠性的限制. 特别是, 神经网络面临对抗攻击时极为脆弱, 攻击者可以对输入数据进行
微小的修改致使模型做出错误的决策 [1] . 这种脆弱性引起了人们对于在自动驾驶, 医疗诊断等安全攸关领域中应
用神经网络的担忧.
形式化验证使用数学方法严格证明系统或程序的正确性与可靠性. 在本工作中, 我们聚焦于验证神经网络的
安全性质, 即确定在给定输入约束下神经网络的输出是否满足预定义的安全行为. 为实现这一目标, 我们采用约束
求解技术, 这是一种在神经网络验证领域中被广泛使用的基础技术. 在进行约束求解时, 神经网络的行为和安全性
质的否定被编码成约束. 这些约束通常以实数变量不等式的形式出现. 随后, 使用约束求解器来确定是否存在一组
对这些变量的赋值能够满足这些约束. 如果找到了满足约束的赋值, 求解器将返回 SAT, 表示存在违反安全性质
的反例 (性质不成立). 反之, 如果没有找到满足约束的赋值, 求解器将返回 UNSAT, 表示不存在违反安全性质的赋
值 (性质成立). 2017 年, 针对以线性整流函数 (rectified linear unit, ReLU) 作为激活函数的神经网络, Katz 等人 [2] 和
[3]
Ehlers 分别提出了的基于可满足性模理论 (satisfiability modulo theories, SMT) 的求解器 Reluplex 和 Planet. 此后,
[6]
[4]
Marabou 作为 Reluplex 的优化版本推出, 展示了更佳的实验性能. 基于抽象解释的方法, 如 AI 2 [5] 和 DeepPoly 等,
能够有效地提供约束求解问题语义的上近似, 因此在进行约束求解时常被用于初始化变量的边界.
增量约束求解是在约束发生微小变化时可以高效求解其可满足性问题的技术. 增量约束求解的核心思想是利
用旧求解过程的信息, 即确定在旧求解过程中所做的推断是否可以应用于求解新的约束. 由于约束的变化相对较
小, 可以快速检查旧求解过程中的推断是否能够保留. 通常情况下大部分推断能够应用于新的求解过程. 与从头开
始解决整个问题相比, 这种方法显著降低了计算开销. 增量约束求解已广泛应用于各种形式方法中, 例如有界模型
检验中的增量 SAT 求解 [7−9] 和组合等效性检查 [10] . 该技术还被用于线性规划的敏感性分析 [11−15] . 增量约束求解可
以有效处理约束的变化, 并提高约束求解算法的整体性能.
神经网络的权重或结构的微小变化催生了对神经网络进行增量验证的需求. 增量验证的一个典型的应用场景
是验证神经网络修复 [16] 后的网络. 神经网络修复的目标是纠正神经网络非预期的行为, 通常情况下, 这需要对神
经网络的权重或结构进行微小改动. 在利用现有的验证工具来评估修复效果时, 需要对被微调过的网络进行验证,
因此采用增量约束求解技术显得尤为适宜. 增量约束求解另一个可能的应用是用于神经网络验证中的反例引导的
抽象细化 (counterexample-guided abstraction refinement, CEGAR) 框架 [17−19] , 该框架首先创建神经网络的抽象, 并
对抽象后的网络进行验证. 如果验证过程发现假反例, 则迭代地精化抽象. 每个精化步骤都涉及对神经网络的结构
和权重进行微小的更改. 例如, Elboher 等人 [18] 通过合并神经元与其对应权重进行抽象, 通过拆分合并的神经元进
行精化. 在这种情况下, 网络的结构和权重都发生改变, 因此可以使用增量约束求解高效的地验证精化后的神经网
络. 此外, 增量情况也可能适用于对抗性训练 [20] 和后门攻击 [21] 等场景.
本文专注于神经网络验证中的增量约束求解问题. 与传统的增量 SAT 求解或线性规划的灵敏度分析不同, 神
经网络增量验证问题中的变化主要涉及权重的定量变化. 换言之, 虽然神经网络增量验证问题中发生变化的约束
数量可能很大, 甚至所有约束都可能受到微小扰动的影响, 但权重变化的绝对值之和仍然微小. 这一根本差异使得
神经网络的增量验证问题与传统增量约束求解问题存在本质的区别.
鉴于这些挑战, 我们基于 Reluplex 框架提出一种针对神经网络增量验证需求的增量约束求解方法. 我们的算
法考虑了神经网络权重的定量变化, 并能够高效地处理大量变化的约束. 具体来说, 我们仅考虑神经网络在权重上
进行修改, 而结构保持不变的情况. 该情况下, 原始神经网络和修改后的神经网络之间存在一一对应的关系, 这使
我们能在修改后的神经网络中模拟旧验证过程中直接得出某一分支验证结果的计算格局. 在模拟中, 我们提取原
始计算格局中的关键特征, 包括分支断言, 基础变量集和直接推断出 UNSAT 结果的线性等式的位置. 通过计算断
言的合取并利用修改后的神经网络的语义, 我们可以有效地引导搜索树来模拟这些断言. 加强关键线性等式中变