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

3446 软件学报 2025 年第 36 卷第 8 期

量的数值边界是检查修改后的神经网络中旧 UNSAT 证明是否依然适用的关键, 因此我们采用线性规划并使用线
性抽象技术编码不确定的 ReLU 关系 [22] , 这使我们能够得到更紧的数值边界并加速被修改神经网络的证明. 针对
旧求解过程中找到反例的情况, 我们启发式地搜索对应的分支及其附近分支, 以在修改后的神经网络中快速找到
反例. 通过利用这些技术, 我们的方法能够在增量场景中高效, 准确地验证神经网络的性质.
本工作的主要贡献可以总结如下.
(1) 我们在神经网络验证问题中引入增量约束求解的概念, 并提出基于 Reluplex 框架的增量 SMT 算法. 该算
法在扰动后的神经网络上模拟旧验证过程中的搜索树上叶子结点处的关键证明, 利用单纯形法的机制快速检查模
拟的证明是否能复用, 从而在神经网络权重被更改但结构保持不变时进行高效地增量验证.
(2) 我们实现增量 SMT 求解器 DeepInc, 该求解器基于 SMT 验证工具 Marabou. 实验表明, 在 ACAS Xu 和
MNIST 网络上, DeepInc 分别在 81% 和 57.3% 的验证任务中优于 Marabou. 增量验证求解器 DeepInc 的性能与神
经网络的扰动幅度有很大关系, 在扰动幅度不大 (权重值变化不超过 5%) 时, 我们的方法有显著的效率提升. 同时
我们分析了增量求解效率较低的情况, 并通过实验表明即使是微小的修改也可能从根本改变原始神经网络的行
为, 从而增加增量 SMT 求解的难度.
(3) 我们将 DeepInc 与目前最先进的工具 α, β-CROWN 在困难的验证任务上进行比较. 在寻找反例方面,
DeepInc 的性能优于 α, β-CROWN, 表现出强劲的竞争力. 此外, 与同期工作 IVAN [23] 的相比, DeepInc 在困难性质
上的表现始终优于 IVAN. 这些结果表明, 基于 SMT 的 DeepInc 在求解具有挑战性的验证问题上具有潜在优势.

1 基础知识

在本节中, 我们将回顾深度神经网络验证的基础定义.
深度神经网络由一系列层组成, 从输入层开始, 经过若干隐藏层, 最终到达输出层. 每一层中都存在若干神经
元, 每个神经元代表一个实数变量. 除输入层外, 神经元的值是通过前一层的神经元的函数变换获得的. 我们将神
f : R → R , 该函数是层与层之间函数的复合. 这些函数包括仿射函数和非线性激活函数. 仿射
n
m
经网络建模为函数
函数的形式为 y = Wx+b, 其中 W 和 b 分别是常数实数矩阵和向量, 称为权重和偏置. 在本工作中, 我们只考虑 ReLU
激活函数 ReLU(x) = max(0, x), 其中 x ∈ R. 对于 ReLU 关系 x j = ReLU(x i ), 如果 x i 的所有可能的取值均为非负/非
正, 我们称神经元 x i 被确定激活/非激活. 如果 x i 既不能被确定激活也不是被确定非激活, 我们称其为不确定状态.
在形式验证中, 安全性质意味着不发生任何不期望的事件. 在神经网络验证的背景下, 安全性质通常要求神经
网络对给定区域内的所有输入都应表现出正确的行为. 我们可以对安全性在进行如下定义.
定义 1 (神经网络的安全性质). 神经网络的安全性质是一个三元组 ( f,X,P), 其中 f : R → R 是神经网络,
n
m
m n
X ⊆ R 和 P ⊆ R 分别是输入和输出的集合. 当且仅当对所有 x ∈ X, 有 f(x) ∈ P 时, 性质 ( f,X,P) 成立. 违反性质 P
∗ ∗
的输入 x ∈ X 满足 f(x ) < P, 被称为性质 ( f,X,P) 的反例. 神经网络验证问题是判断给定的性质 ( f,X,P) 是否成立.
m n
局部鲁棒性也是安全性质的一种. 对于分类神经网络 f : R → R , 定义 C f (x) = argmax 1⩽i⩽n f(x) i 为 f 的分类.
如果对于输入 x 0 的邻域 B(x 0 ) 中的所有 x, 都有 C f (x) = C f (x 0 ), 则称分类神经网络 f 在给定邻域中是局部鲁棒的.
n
该性质可以写成安全性质 ( f,X,P), 其中 X = B(x 0 ) 且 P = {y ∈ R | argmax i y i = C f (x 0 )}.
X
约束求解是神经网络验证的基本方式. 给定一个安全性质 ( f,X,P), 我们将输入集合 , 构成神经网络 f 的所
P 的否定编码为等式或不等式, 并确定这些约束的合取是否可以被满足. 如果这些约束的合取可
有函数, 以及性质
以被满足, 则必定存在违反该性质的反例; 否则, 该安全性质成立.

2 适用于神经网络验证的增量可满足模理论
在本节中, 我们将介绍神经网络验证的增量 SMT 求解问题, 并通过一个示例展示我们的算法.

2.1 Reluplex 算法
[2]
Reluplex 是一个基于 SMT 的神经网络验证算法. Reluplex 求解过程中, 会对当前的计算格局进行管理. 当计