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

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

x 1 ≥−1 x 3 ≥0.2x 1 −0.7x 2 −0.1 x 5 ≥0

x 1 ≤1 x 3 ≤0.2x 1 −0.7x 2 −0.1 x 5 ≤0.445x 3 +0.445
l 1 =−1 l 3 =−1 l 5 =0
u 1 =1 u 3 =0.8 u 5 =0.8 y≥0.4x 5 +0.6x 6
y≤0.4x 5 +0.6x 6
0.2 ReLU(x 3 ) l 7 =0
x 1 x 3 x 5 0.4
0.8 u 7 =1.28
−0.7 Bias −0.1 0.6 y
−0.8 ReLU(x 4 )
x 2 x 4 x 6
x 2 ≥−1 x 4 ≥0.8x 1 −0.8x 2 x 6 >0
x 2 ≤1 x 4 ≤0.8x 1 −0.8x 2 x 6 ≤0.5x 4 +0.8
l 2 =−1 l 4 =−1.6 l 6 =0
u 2 =1 u 4 =1.6 u 6 =1.6
f 的 DeepPoly 抽象
图 2 神经网络

图 2 中, ReLU 关系集为 R = {(x 3 , x 5 ),(x 4 , x 6 )}. 初始解表根据 f 中的仿射函数 (即 x 3 = 0.2x 1 −0.7x 2 −0.1 x 4 =
,
y = 0.4x 5 +0.6x 6 ), 以及来自 ReLU 关系的不等式 x 6 ⩾ x 4 ) 构建. 首先为两个不等式引入
0.8x 1 −0.8x 2 和 (即 x 5 ⩾ x 3 和
两个松弛变量 x 7 和 , 即 x 5 − x 3 − x 7 = 0 和 x 6 − x 4 − x 8 = 0. 从 DeepPoly 抽象中可以得到 x 7 和 x 8 的数值边界分别是
x 8
[0, 1] 和 [0, 1.6]. 然后为其他 5 个线性等式分别添加一个松弛变量来替代常量, x 9 = −x 3 +0.2x 1 −0.7x 2 x 10 = 0.8x 1 −
,
,
,
0.8x 2 − x 4 x 11 = 0.4x 5 +0.6x 6 −y x 12 = x 5 − x 3 − x 7 , 和 x 13 = x 6 − x 4 − x 8 , 其中 x 9 = 0.1 和 x 10 , x 11 , x 12 , x 13 = 0. 对于以上
每个方程, 我们启发式地选择一个变量作为基础变量, 并获得初始基础变量集 B 0 = {x 3 , x 4 ,y, x 7 , x 8 }. 初始表 T 0 如下:


 x 3 = 0.2x 1 −0.7x 2 − x 9





 x 4 = 0.8x 1 −0.8x 2 − x 10





 y = 0.4x 5 +0.6x 6 − x 11 .





 x 7 = x 5 − x 3 − x 12 = −0.2x 1 +0.7x 2 + x 5 + x 9 − x 12





x 8 = x 6 − x 4 − x 13 = −0.8x 1 +0.8x 2 + x 6 + x 10 − x 13
初始数值边界和赋值如表 1, 加粗的赋值表示其不满足数值边界或 ReLU 关系.

表 1 初始数值边界和赋值

边界与赋值 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 0 −0.4 0 0.1 0 0 0 0

注意, y 和 x 7 的赋值不满足其数值边界, 并且它们都是当前的基础变量. 我们选择其中一个 (如 x 7 ), 进行交换
(pivot). 此时 x 7 的当前赋值小于其下界约束, 而对 x 5 的赋值进行修改可能修复这一冲突, 因为 x 5 并且未达到其上
界. 交换 x 7 和 x 5 后可以得到 x 5 = 0.2x 1 −0.7x 2 + x 7 − x 9 + x 12 . 随后将其他方程中出现的 x 5 替换为当前的表达式 0.2x 1 −
0.7x 2 + x 7 − x 9 + x 12 . 此时基础变量集变为 B 1 = {x 3 , x 4 , x 5 ,y, x 8 }, 解表变为 T 1 :


 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 .





y = 0.08x 1 −0.28x 2 +0.6x 6 +0.4x 7 −0.4x 9 − x 11 +0.4x 12





x 8 = −0.8x 1 +0.8x 2 + x 6 + x 10 − x 13
y
此时 x 7 是非基础变量, 我们将其赋值更改为 0 以满足其数值边界, 同时基础变量 x 5 和 的赋值根据 T 1 进行相
应地变化. 上述操作完成后当前赋值如表 2.

表 2 修改 x 7 后的边界与赋值

边界与赋值 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 0.16 0 0 0.1 0 0 0 0