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

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

算格局未终止时, 它维护线性等式、ReLU 关系、数值边界和所有变量的当前赋值. 形式化地, Reluplex 计算格局
可以定义如下.
定义 2 (Reluplex 计算格局). 在给定变量集 X 上的 Reluplex 计算格局 C 是 SAT, UNSAT, 或一个六元组
(B,T,R,l,u,α), 其中,
● B ⊆ X 是基础变量 (basic variable) 的集合;
∑
● T 是解表 (tableau), 对于每个 x i ∈ B, 存储一个形式为 x i = a i j x j 的约束;
x j <B
● R ⊆ X×X 是 ReLU 对的集合;
● l,u : X → R 分别是每个变量的下界和上界;
● α : X → R 是每个变量的赋值.
[6]
给定性质 ( f,X,P), 我们引入松弛变量来建立解表, 并调用 DeepPoly 计算变量的数值边界来初始化计算格局.
DeepPoly 是一种基于抽象解释计算神经元在给定输入约束下的上下界的高效算法. 该算法对每个神经元维护一组
线性的符号上下界和数值上下界. 其中符号上下界是通过对神经元进行抽象 (三角形松弛) 得到的神经元输出范围的
线性边界; 数值上下界由符号上下界具体化得到. 具体化是一个迭代过程, 需要不断将当前符号上下界表达式中的变
量替换为前一层的变量, 直到得到当前符号上下界关于输入的表达式, 并带入输入的上下界得到数值上下界.
当求解过程处于计算格局 (B,T,R,l,u,α) 时, Reluplex 会通过不断调整变量的赋值 α 以匹配解表 T 和 ReLU 关
系 R 进行局部搜索. 如果当前计算格局 (B,T,R,l,u,α) 中的赋值能够使所有约束被满足, 即:
∑ ∑
● 对于解表 T 中的任何线性等式 x i = x j <B a i j x j , 都有 α(x i ) = x j <B a i j α(x j );
(x i , x j ) ∈ R α(x j ) = ReLU(α(x i ));
,
● 对于任何对
x l(x) ⩽ α(x) ⩽ u(x);
● 对于 X 中的任何 ,
则意味着已经找到一个反例, Reluplex 算法返回 SAT.
∑
如果存在解表 T 中的线性等式 x i = 满足以下之一:
a ij x j
x j <B
∑ ∑
l(x i ) > max(a ij ,0)·u(x j )+ min(a ij ,0)·l(x j ),
x j <B x j <B
∑ ∑
u(x i ) < max(a ij ,0)·l(x j )+ min(a ij ,0)·u(x j ),
x j <B x j <B
则在此计算格局中不可能有可以满足约束的赋值, 我们为此计算格局的相应分支标记 UNSAT.
如果经过一定数量的局部搜索后可能仍无法确定当前计算格局究竟是 SAT 还是 UNSAT, 我们需要停止局部搜

索, 并选择一个不确定的神经元 x j , 将其数值边界分割为 [0,u(x j )] 和 [l(x j ),0]. 随后向当前计算格局中添加断言, 即添
加形式为 x j ⩾ 0 或 x j ⩽ 0 的约束, 并进行新的局部搜索. 当所有分支都被标记为 UNSAT 时, Reluplex 返回 UNSAT.
我们用图 1 中的小型神经网络来说明 Reluplex 算法, 该网络的输入层包括两个神经元 x 1 和 , 输出为 y ∈ R.
x 2
,
,
该网络的行为可以表示为仿射变换 x 3 = 0.2x 1 −0.7x 2 −0.1 x 4 = 0.8x 1 −0.8x 2 y = 0.4x 5 +0.6x 6 与 ReLU 关系 x 5 =
ReLU(x 3 ) x 6 = ReLU(x 4 ) 的组合.
,

0.2 ReLU(x 3 )
x 1 x 3 x 5
0.4
0.8 Bias −0.1
−0.7 0.6 y
−0.8 ReLU(x 4 )
x 2 x 4 x 6
图 1 小型神经网络 f

P = {y | y < 0.3}. 编码约束时需
考虑对性质 ( f,X,P) 进行约束求解, 其中输入约束为 X = [−1,1]×[−1,1], 性质
要将输入约束 ( −1 ⩽ x 1 ⩽ 1 −1 ⩽ x 2 ⩽ 1), 性质 P 的否定 ( y ⩾ 0.3) 以及神经网络 f 的行为合取.
,
求解上述约束时, 首先初始化其 Reluplex 计算格局. 神经网络 f 在 X 上的 DeepPoly 抽象如图 2 所示.