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

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

f 的验证结果是 SAT, 则有唯一的 SAT ε 的叶节点, 因为 SAT 意味着找到了
如果 叶节点并且可能有一些标记为
一组对应反例的赋值, 一旦找到这样一组赋值, 验证会立即终止, 所以可能有一些分支未被验证. 在这种情况下, 我
们总是首先对 SAT 叶节点尝实验证, 然后是标记为 ε 的叶节点 (直接调用 Reluplex 求解), 最后是 UNSAT 叶节点.
这是因为叶节点的验证结果多数情况下不会因为权重的微小修改而改变, 所以旧 UNSAT 叶节点存在反例的可能
性也不会比未探索过的叶节点大.
ε 的叶节点, 我们认为即使原始 SAT f 中的求解结果是 UNSAT, 靠近 SAT
′
对于标记为 叶节点对应的计算格局在
Assert(v ) 的基
′
叶节点的叶节点也比其他叶节点在 T 中更有可能存在反例, 具体来说, 我们通过对称差集 Assert(v) 和
′ ε 的叶节点之前, 我们计算 叶节点与它们
数来衡量标记二叉树 T 中两个节点 v 和 v 之间的距离. 在处理标记为 SAT
之间的距离, 并按照这个距离从最小到最大的顺序排序作为求解顺序. 对于 UNSAT 节点 v, 我们通过检查 T 中的
′
UNSAT 证明是否仍然适用于修改后的神经网络 f 进行增量求解, 算法 2 的 Solve( f ,T ,v) 对该过程进行了详细描述.
′
算法 2. 针对 UNSAT 节点 v 的函数 Solve( f ,T ,v).
′
输入: Reluplex 对于安全性质 ( f,X,P) 的求解过程 T = (V,E,r,L), 修改后的深度神经网络 f 和 ′ UNSAT 节点 v ∈ V;
( f ,X ∧Assert(v),P) 不成立, 返回 SAT; 否则返回 UNSAT.
′
输出: 如果安全性质
1. function Solve( f ,T ,v)
′
2. C ← L(v) ↓ ▷ C = (B,T,R,l,u,α)
′
3. l,u ← DeepPoly( f ,X ∧Assert(v))
4. if LP( f ∧ X ∧¬P∧Assert(v)) 不可满足 then
′
5. return UNSAT
6. for x i ∈ Var((L(v) ↓) ) do
∗
7. (l i ,u i ) ← LP( f ∧ X ∧¬P∧Assert(v), x i )
′
8. T ← T \{e}
9. T ← GaussElimination(C 0 ,B)
10. if ((L(v) ↓) (T),l,u) 推断出 UNSAT then
∗
11. return UNSAT
12. else return Reluplex(C)
算法 2 中, 首先获取 T 中推断出 UNSAT 的计算格局 L(v) ↓. 根据该计算格局中的基础变量, 我们可以使用高
′ C 0 的表转换为具有相同基础变量的形式. 如前文所述, 对于旧求解过程中推断出
斯消元法将 f 的初始计算格局
∗
UNSAT 的线性等式 (L(v) ↓) , 如果其中的变量的数值边界越紧, 那么立即推断出 UNSAT 的可能性就越大. 但在 f ′
(L(v) ↓) 时, 由 DeepPoly 得到的数值边界往往不够紧, 因为 Assert(v) 中的
∗
中模拟 DeepPoly 不允许反向分析导致
断言 x j ⩾ 0 (或 x j ⩽ 0) 不能细化同一层或前一层神经元的边界. 为了获得更紧的数值上下界, 我们调用非迭代版本的
DeepSRGR [22] , 该版本结合线性规划和线性近似来收紧边界. 我们首先优化 min x i 或 max x i 以获取 x i ∈ Var((L(v) ↓) )
∗
∗
∗ ∗ (L(v) ↓) 产生的方程
更紧的边界, 这里 Var((L(v) ↓) ) 表示出现在 (L(v) ↓) 的变量集合. 随后检查当前解表 T 中模拟
在当前的数值界下是否能推断出 UNSAT. 如果不能证明 UNSAT, 我们基于当前的数值边界对 v 调用 Reluplex 求解.
接下来我们展示如何使用 DeepInc 增量验证修改后的神经网络. 在图 5 和图 6 中, 我们分别展示了从原始神
f 在图 1 ′ ′′ ′ f 的求解程序
经网络 的基础上修改得到的两个神经网络 f 和 f . 我们首先增量验证性质 ( f ,X,P). 由于
中有 SAT 节点 v 5 , 所以首先在 f 中对 v 5 进行增量求解. 我们采用 v 5 在第 1 次验证中的断言 Assert(v 5 ) = x 4 ⩾ 0∧ x 3 ⩽ 0
′
T
′ (0.714,0.204) , 所以算法返回 SAT. 由
并初始化 f 在此约束下的计算格局. 经过一次交换操作后, 找到了一个反例
′ f 仅略有不同, 增量 f 的反例. 两个反例的计算格局中断言的神经元激活
′
于 f 与 SMT 求解使我们能够快速找到
模式完全相同, 从而避免了对其他节点的大量局部搜索.