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

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

x 6 交换, 并调整其赋值为 0.3. 类似地, 我们可
现在 y 的赋值仍然违反其数值边界, 因此我们选择与非基础变量
以得到基础变量集 B 2 = {x 3 , x 4 , x 5 , x 6 , x 8 }、表 T 2 和相应的赋值 (如表 3).


 x 3 = 0.2x 1 −0.7x 2 − x 9






 x 4 = 0.8x 1 −0.8x 2 − x 10




 x 5 = 0.2x 1 −0.7x 2 + x 7 − x 9 + x 12 .





 x 6 = −0.13x 1 +0.47x 2 +1.67y−0.67x 7 +0.4x 7 −0.67x 9 +1.67x 11 −0.67x 12





x 8 = −0.93x 1 +1.27x 2 +1.67y−0.67x 7 +0.67x 9 + x 10 +1.67x 11 −0.67x 12 − x 13

表 3 修改 x 6 后的边界与赋值

边界与赋值 x 1 x 2 x 3 x 4 x 5 x 6 y x 7 x 8 x 9 x 10 x 11 x 12 x 13
l −1 −1 −1 −1.6 0 0 0.3 0 0 0.1 0 0 0 0
u 1 1 0.8 1.6 0.8 1.6 1.28 1 1.6 0.1 0 0 0 0
α −1 −1 0.4 0 0.4 0.233 0.3 0 0.233 0.1 0 0 0 0

T 2 中所有线性等式都被满足, 但 ReLU x 6 = ReLU(x 4 ) 被违反. 如果在
这组赋值不违反任何数值边界, 且 关系
,
这一步我们用 y 替换 , 我们将再次获得 B 1 T 1 和上一步相同的冲突赋值. 假设现在达到局部搜索的阈值, 我们必
x 6
须选择一个不确定的 ReLU 神经元进行分割. 这里一个启发式的选择是分割 x 4 , 因为在 x 4 的局部搜索中已有一次
冲突, 但 x 3 没发生过冲突. 在断言 x 4 ⩽ 0 的非激活分支中, 我们首先将 x 4 的上界重置为 0, 并在这一断言下再次运
行 DeepPoly, 以获得新的数值边界和赋值 (如表 4).

表 4 分割 ReLU 节点后的边界与赋值

边界与赋值 x 1 x 2 x 3 x 4 x 5 x 6 y x 7 x 8 x 9 x 10 x 11 x 12 x 13
l −1 −1 −1 −1.6 0 0 0.3 0 0 0.1 0 0 0 0
u 1 1 0.8 0 0.8 0 0.32 1 1.6 0.1 0 0 0 0
α −1 −1 0.4 0 0.4 0 0.16 0 0 0.1 0 0 0 0

y 再次违反其数值边界, 我们将其与一个非基础变量交换. 经过多步局部搜索后, 我们无法找到满足
现在变量
所有约束的赋值, 因此必须再次进行分割, 断言 x 3 ⩽ 0 或 x 3 ⩾ 0. 在这两个分支中, 问题都简化为一个线性规划问
x 4 ⩾ 0 进行 DeepPoly
题, 并且这两个分支都是不可行的. 我们仍然有未求解的分支 x 4 ⩾ 0. 我们以类似的方式对断言
算界, 检查赋值是否有效, 并在违反约束的基础变量中进行交换. 经过多步局部搜索后, 我们再次需要对 x 3 进行分
T
割. 在 x 3 ⩽ 0 的分支中, 我们找到一个满足所有约束的赋值, 其中的反例是 (0.675,0.05) , 其输出是 y = 0.3. 这意味
着该组输入违反了性质 P : y < 0.3. 由于已找到一个真实的反例, Reluplex 立即输出 SAT, 最后 x 3 ⩾ 0 对应的分支不
会 被 探 索 . 上 述 求 解 过 程 对 应 的 搜 索 树 T = (V,E,r,L) 如 图 3 所 示 , 其 中 V = {r,v 1 ,v 2 ,v 3 ,v 4 ,v 5 ,v 6 } , 且 r 是 根 ;

;
E = {(r,v 1 ),(r,v 2 ),(v 1 ,v 3 ),(v 1 ,v 4 ),(v 2 ,v 5 ),(v 2 ,v 6 )} V ∪ E 上的标记函数 L 在图 3 中标出. 在这一求解过程中, 叶节点 v 3
和 v 4 是 UNSAT 叶节点, v 5 是 SAT 叶节点, v 6 是一个标记为空序列 ε 的叶节点. 在节点 , 我们已找到一个真正的
v 5
反例, 因此最后的叶节点 v 6 在求解过程中不会被求解, 其标签应为 ε.

r C 0 C 1 C 2
x 4 ≤0 x 4 ≥0
C 3 C 4 C 5 v 1 v 2 C 8 C 9 C 10
x 3 ≤0 x 3 ≥0 x 3 ≤0 x 3 ≥0
v 3 v 4 v 5 v 6
ε
C 6 UNSAT C 7 UNSAT C 11 C 12 SAT
图 3 性质 ( f,X,P) 的求解过程

2.2 增量 SMT 求解问题
如前文所述, Reluplex 求解实际上是通过添加断言来将不确定 ReLU 神经元行为限定为绝对激活或非激活来
进行深度优先搜索, 因此, 我们可以将 Reluplex 求解过程形式化为一个带标记的二叉树, 并称其为搜索树.