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

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

0.34 ReLU(x 3 )
x 1 x 3 x 5
0.2 ReLU(x 3 ) 0.4
x 1 x 3 x 5 0.16
0.4 Bias −0.05
0.9 −1.34 0.6 y
−0.7 0.6 y −0.69 ReLU(x 4 )
−0.7 ReLU(x 4 ) x 2 x 4 x 6
Bias −0.33
x 2 x 4 x 6
图 5 修改后的神经网络 f ′ 图 6 修改后的神经网络 f ′′
f ′′ f 差异很大. 以类似方式, 我们增量求解 SAT v 5 . 但在该网络中,
神经网络 的权重与原始神经网络 叶节点
v 5 的求解结果变为 UNSAT, 因此我们必须探索其他节点. 首先处理标签为空的节点 v 6 , 检查是否有反例. 这里启
v 6 而不是两个 UNSAT ε 的叶节点更有可能找到修改后神经
发式地首先处理 叶节点 v 3 和 , 因为我们认为标记为
v 5
网络的反例. 在这个示例中, v 6 的 Reluplex 求解结果依然为 UNSAT, 所以我们必须返回到 UNSAT 叶节点 v 3 和 .
v 5
对于 UNSAT 叶节点的增量求解是不同的, 因为我们可以利用旧的 UNSAT 证明. 对于这里的 UNSAT 叶节点 v 3 ,
我们有一个证明 C 6 → UNSAT. 接下来通过 f ′′ 在 Assert(v 3 ) 限制下的计算格局来模拟 C 6 . 我们提取 C 6 中基础变量
∗
的集合 B 6 , 并将 f ′′ 的初始表转换为以 B 6 为基础变量的形式. 此外, C 6 → UNSAT 源于表中的一个线性等式 C , 因
6
此我们关注当前表中的这个线性等式. 注意, 更紧的数值边界有助于证明这个 UNSAT, 因此我们求解一个以此线
性等式中的变量为优化对象的线性规划. 通过紧化边界, UNSAT 立即从 C 推断出来. 类似的程序也在 UNSAT 叶
∗
6
节点 v 4 上进行, 并且它也有一个立即的 UNSAT 证明. 现在树 T 中的所有叶节点都有验证为 UNSAT, 因此我们的
增量 SMT 求解返回 UNSAT, 即性质 ( f ,X,P) 成立. 当修改较小时, 我们可以可能继承旧求解程序中相应叶节点
′′
的验证结果, 从而避免大量的局部搜索和不必要的 UNSAT 叶节点的求解. 然而, 当修改很大, 以至于本质上改变
了神经网络的行为时, 许多验证结果可能无法继承, 可能还需要更多的局部搜索. 直观上, 我们的增量 SMT 求解是
否更有效取决于修改的大小以及修改是否从本质上改变神经网络的行为.
我们在定理 1 中总结了算法 1 的可靠性和完备性.
定理 1. 算法 1 是可靠且完备的, 即算法 1 返回 UNSAT 当且仅当性质 ( f ,X,P) 成立.
′
证明: 首先证明对于 UNSAT 叶节点 v, 函数 Solve( f ,T ,v) 返回 UNSAT 当且仅当 ( f ,X ∧Assert(v),P) 成立. 在
′
′
算法 2 的第 8 行中, 当前计算格局 C 的语义恰好是 f ∧ X ∧Assert(v)∧¬P, 因为 , Assert(v) 已在 L(v)
′
X ¬P 以及断言
中编码, 第 8 行的解表编码了 f 中的仿射变换且 ReLU 关系 R 保持不变. 数值边界 和 u 是 f ∧ X ∧Assert(v)∧¬P
l
′
′
的上近似, 因此它们不违反此语义. 如果在算法 2 的第 10 行, Solve( f ,T ,v) 返回 UNSAT, 则 C 得到一个 UNSAT
′
( f ,X ∧Assert(v),P) 成立. 如果在算法 2 的第 11 行, Solve( f ,T ,v) 返回 UNSAT, 由于 Reluplex
′
′
证明, 这意味着性质
′
′ ( f ,X ∧Assert(v),P) 成立, 则无论是在第 行
是完备的且可靠的, 性质 ( f ,X ∧Assert(v),P) 也成立. 现在我们假设 10
迅速给出证明, 还是在第 11 行通过 Reluplex 求解, Solve( f ,T ,v) 必然输出 UNSAT. 对于那些非 UNSAT 的叶节点
′
v, 同样在算法 1 的第 10 行, 当前计算格局 C 的语义是 f ∧ X ∧Assert(v)∧¬P Reluplex(C) 返回 UNSAT 当且仅当
.
′
( f ,X ∧Assert(v),P) 成立. 因此, 我们得出算法 1 返回 UNSAT 当且仅当对所有叶节点 , ′
′
v ( f ,X ∧Assert(v),P) 成立.
′
根据求解过程建, 自然地有 ∨ v是叶节点 Assert(v) = ⊤, 因此对所有叶节点 , ′ ( f ,X,P)
v ( f ,X ∧Assert(v),P) 成立当且仅当
成立.
算法 1 也适用于输入约束 X 和性质 P 被修改的情况. 这在我们使用基于 SMT 的验证工具通过二分搜索计算
最大鲁棒性半径时非常有用.
值得注意的是, 我们的算法与 IVAN [23] 所采用的技术从不同角度对神经网络增量验证问题进行了优化. 我们
增量验证算法的关键是在 SMT 求解器角度快速重用首次验证过程的信息验证修改后的神经网络, 为增量验证提
取关键信息和在叶节点计算数值边界是该方法最大的挑战; IVAN 则专注于启发式地构建增量求解的最优搜索策
略; 此外, IVAN 中虽然提到对叶子节点的重用, 但其对叶子节点的利用更加直接, 即直接添加验证中的分支信息
后调用现成的求解器. 相比之下, 我们的方法从 SMT 求解器的角度, 更细粒度的利用 UNSAT 的验证格局 (即基础
变量表, 导致冲突的变量等) 进一步地加速 UNSAT 的证明.