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

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

到初始计算格局 C 0 的方式维护 Assert(v) 中涉及的不确定神经元的所有行为. 另一个重要的特征是计算格局 L(v) ↓
v 是一个 UNSAT (L(v) ↓) 表示在数值边界上存在矛盾的线性等
∗
中的基础变量的集合, 特别是当 叶节点时. 我们用
式. UNSAT 的推理严重依赖于 (L(v) ↓) , 而线性等式 (L(v) ↓) 来源于当前基础变量集下的线性等式解表. 因此, 可
∗
∗
∗
以根据这组基础变量集合在 f 的计算格局中模拟线性等式 (L(v) ↓) .
′
在 f 的验证过程中, 继承旧验证过程中的 UNSAT 叶节点 v 的关键特征并形成模拟计算格局后, 我们不难观
(L(v) ↓) 中变量的数值边界的精度与 UNSAT 证明的有效性高度相关. 数值边界越精确, 推断出 UNSAT 的可
∗
察到
能性就越大. 注意, L(v) 中的计算格局的语义等同于初始计算格局 C 0 和断言 Assert(v) 的合取, 因此我们直接通过
′ L(v) 中的计算格局.
f 的行为和 Assert(v) 计算数值边界, 而不是通过
如果旧的验证结果是 UNSAT, 我们增量地检查每个 UNSAT 叶节点上旧的 UNSAT 推理是否仍然适用于 f .
′
对于无法立即证明的叶节点 v, 我们将计算格局设置为 L(v) ↓ 并使用 Reluplex 继续求解. 如果旧的验证结果是 SAT,
我们首先定位在 SAT 叶节点, 并检查这个分支中是否有反例. 如果没有反例, 则按从最近到最远的顺序遍历标记
为 ε 的叶节点. 若仍没有反例, 则按照上述对 UNSAT 叶节点的处理方式对剩余的 UNSAT 叶节点进行增量验证.
算法 1 展示的是增量验证的主算法, 其中输入是安全性质 ( f,X,P) 的 Reluplex 求解过程 T = (V,E,r,L) 和修改
′
′ f 的计算格局并计算该初始计算格局的数值上下界 . 计算上下界时通常会调用可
后的神经网络 f . 首先初始化 U
靠 (sound) 但不完备 (complete) 的方法, 在本工作中我们选择抽象解释方法 DeepPoly. 由于 DeepPoly 是可靠的, 如
果 DeepPoly 成功验证出性质, 算法可以直接返回 UNSAT.
算法 1. 适用于深度神经网络验证的增量 SMT 求解算法.

f
′
输入: Reluplex 对于安全性质 ( f,X,P) 的求解过程 T = (V,E,r,L) 和修改后的深度神经网络 ;
′
输出: 如果安全性质 ( f ,X,P) 不成立, 返回 SAT; 否则返回 UNSAT.
1. function Verify( f ,X,P,T )
′
2. U ← DeepPoly( f ,X)
′
3. if U ∧¬P = ⊥ then
4. return UNSAT
5. C 0 ← Initialize( f ,X,P,U)
′
6. for e ∈ E do
7. if L(e)∪U = ∅ then
8. T ← T \{e}
9. if 存在 SAT 叶节点 v SAT ∈ V then

10. for 叶节点 v 的标记为 SAT 或 ε do
11. C ← L(v) ↓ ▷ C = (B,T,R,l,u,α)
12. l,u ← DeepPoly( f ,X ∧Assert(v))
′
13. T ← GaussElimination(C 0 ,B)
14. if Reluplex(C) = SAT then
15. return SAT
16. for UNSAT 叶节点 v ∈ V do
′
17. if Solve( f ,T ,v) = SAT then
18. return SAT
19. return UNSAT

初始化计算格局后, 我们能推断出 T 中的一些边是否可以被剪枝. 如果一个边 e ∈ E 的标签 L(e) 与 DeepPoly
′
e
计算的结果矛盾, 即 L(e)∩DeepPoly( f ,X) = ∅, 则从 T 中删除边 及其下的子树, 我们用 T \{e} 表示该剪枝过程.