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

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

定义 3 (搜索树). 搜索树是一个标记的二叉树 T = (V,E,r,L), 可以用来表示 Reluplex 求解过程, 其中,
● V 是节点集;
● E ⊆ V ×V 是边的集合;
● r ∈ V 是根;
● L 是一个标记函数, 它给每个节点 v ∈ V 标记一组有限的计算格局序列, 并给每个边 e ∈ E 标记一组形式为

x j ⩾ 0 或 x j ⩽ 0 的断言, 其中 x j 是一个不确定的神经元.
如果 Reluplex 求解的输出是 UNSAT, 则其搜索树中所有叶节点的标记都有 C 1 ,...,C n , UNSAT 的形式, 我们
将这样的叶节点称为 UNSAT 叶节点. 如果输出是 SAT, 则存在一个其标签形式为 C 1 ,...,C n , SAT 的叶节点, 我们
称之为 SAT 叶节点; 在这种情况下, 其他叶节点要么是 UNSAT 叶节点, 要么被标记为空序列 ε. 对于非空的计算
ℓ
格局序列 ℓ, 我们使用 ℓ ↓ 表示 中最后一个不是 SAT 或 UNSAT 的计算格局. 对于节点 v ∈ V, 我们使用 Assert(v)
v
v
表示从根 r 到节点 的边上的断言集合. 注意节点 的语义是初始计算格局与 Assert(v) 中的断言的合取的交集. 为
∧
Assert(v).
Q 简写为
方便叙述, 我们将约束
Q∈Assert(v)
综上所述, 增量约束求解用于神经网络增量验证的目的是利用原始神经网络 f 的验证过程, 高效地验证修改
f 上的性质. 本工作中基于 Reluplex 框架考虑增量 SMT f 与原
′
′
后的神经网络 求解, 并只针对修改后的神经网络
f 在结构上完全相同, 仅在仿射函数中的权重和偏置上有所不同的情况. 下面我们正式陈述要求解的
始神经网络
神经网络增量验证问题:
定义 4 (神经网络增量验证问题). 给定安全性质 ( f,X,P) 的求解程序 T = (V,E,r,L), 我们确定性质 ( f ,X,P) 是
′
′
否成立, 其中神经网络 f 仅在权重和偏置上与 f 不同.

2.3 整体框架
图 4 为神经网络的增量 SMT 求解框架. 对于神经网络的增量求解问题, 最重要的假定是修改后的神经网络 f ′
′ f 时类似. 这启发我们可
与原始神经网络 f 只存在微小的差异, 因此 f 的验证过程中的大多数分支很可能与验证
T 中叶节点的计算格局, 特别是能够最后一个直接推断出 UNSAT 或 SAT 的计算格局, 并检查该计
以直接定位到
f .
′
算格局中的做出的推断是否仍适用于修改后的神经网络

DeepInc
Search tree
Input X
Path
Path Path
DNN f Marabou
Modification Property P UNSAT UNSAT ε SAT
Locate the old UNSAT proof Marabou
DNN f ′ Tighten the bounds of key variables
Invalid
Restore the configuration UNSAT for this node

Incremental proof checking UNSAT
Valid
图 4 增量 SMT 求解框架

对于 T 中的叶节点 v, 我们尝试提取计算格局 L(v) ↓ 的关键特征, 并将这些特征添加到修改后的神经网络 f ′
v
r
的初始计算格局 C 0 中. 一个关键特征是 Assert(v), 即从 到 的路径上断言的合取. 我们可以通过将 Assert(v) 添加