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

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

3 实验评估

本节将对增量 SMT 求解器 DeepInc 进行实验评估. 所有实验均在配备 AMD R9 5900HS@3.00 GHz (8 核心)
和 16 GB RAM 的 Ubuntu 20.04 笔记本电脑上进行, 最多同时使用 16 个子进程.
● 网络: 我们使用 ACAS Xu 数据集和 MNIST 数据集上训练出的网络进行评估. ACAS Xu 是无人机空中碰撞
避免系统 [2] 的缩写, 该系统使用神经网络为飞机做出决策以避免飞机在空中发生碰撞. 我们使用的网络包含 6 个
隐藏层, 每层有 50 个神经元, 并且所有隐藏神经元都使用 ReLU 激活函数. MNIST 数据集包含 60 000 张训练图像和
10 000 张测试图像, 每张图像均为 28×28 像素的手写数字. 我们从 MNIST 数据集训练出的网络中选择 2×256,
4×256, 6×256 这 3 种类型的全连接网络进行测试.
● 性质: 对于 ACAS Xu 数据集训练出的网络, 我们选择文献 [2] 的附录 VI 中提供的前 4 个安全性质, 即性质
φ 1 、 φ 2 、 φ 3 和 φ 4 . 另外我们还生成了 3 个局部鲁棒性性质, 其 L ∞ 半径分别为 0.05、0.075 和 0.01. 除这些性质外,
我们还通过在原始神经网络上进行二分搜索找到最大鲁棒性半径, 生成了 24 个接近鲁棒边界的局部鲁棒性性质,
验证这些性质非常具有挑战性. 我们基于这些性质来比较 DeepInc、α, β-CROWN 和 IVAN 的验证效率. 由于这 3
种方法都是可靠且完备的, 因此验证这些困难性质的性能真实地显示了各个工具的极限能力. 对 MNIST 上训练出
的网络, 我们从测试集选择一些图片, 并将图片分别在 0.05 和 0.1 的扰动下鲁棒作为性质.
● 网络参数的扰动: 我们对神经网络权重的采用两种随机修改方法. 第 1 种修改方法对所有权重进行修改. 且
I(w,γ) = [(1−γ)w,(1+γ)w] 中的一个数字. 修改后
所有权重在变化率 γ 内变化. 具体而言, 权重 w 可以修改为区间
的权重是根据权重变化率 γ 在 I(w,γ) 上进行均匀分布的随机采样获得的. 在我们的实验中, 权重变化率 γ 设置为
0.001、0.01、0.03 和 0.05. 第 2 种修改方法是部分权重修改, 即只修改原始神经网络的部分权重. 在我们的实验
中, 改变的权重百分比设为 10%、30% 和 50%, 并且随机选择要改变的权重. 在部分修改中, 我们还对改变的权重
施加了权重变化率的限制, 实验中为 0.01、0.03 和 0.05. 对于实际的修改, 我们使用神经网络修复工具 CARE [16] 、
PRDNN [24] 和 VeRe [25] 来修复 ACAS Xu 网络中 Marabou 发现的不安全行为. 这里我们不仅考虑了不同程度和不同
形式随机生成的扰动, 还考虑了修复产生的扰动, 这能体现出我们的工具在各种扰动下的性能.
我们将 DeepInc 与 Marabou 进行比较, 以展示我们的增量验证算法的有效性和效率, 此外还将 DeepInc 与
α, β-CROWN 和 IVAN 进行比较, 以对比这些工具在增量验证场景下的性能.

3.1 总体效率
我们在随机修改后的神经网络上运行 Marabou 和 DeepInc, 其中 DeepInc 还有 Marabou 给出的原始神经网络
的验证过程作为输入. 各个工具验证单个问题的超时时间 (timeout, TO) 设置为 20 000 s. 实验结果显示在图 7、图 8
和图 9 中, 每个子图都对比了两种工具在不同权重扰动下验证对应数据集全部安全性质/局部鲁棒性性质的运行
时间, 验证时间为超时或少于 1 s 的情况未在图中显示. 在所有验证问题中, 原始神经网络及其所有修改后的神经
网络的对于同一性质的验证结果都是相同的.
总体效率方面, 在 ACAS Xu 数据集上, DeepInc 在 81% 的 ACAS Xu 验证问题中胜过 Marabou, Marabou 的总
运行时间是 DeepInc 的 2.003 倍. DeepInc 和 Marabou 在同一个验证问题上都有一个超时结果. 从图 7 中可以看出,
在 4 个安全性质上 DeepInc 显示出更多的效率优势, 有 11 个验证问题比 Marabou 快 100 倍以上, 但它们在局部鲁
棒性验证上的表现相对接近. 这可能是因为安全性质输入范围更大, 分支数更多, 能够继承的验证信息更多, 有利
于我们的算法发挥作用. 从图 7 中可以看到, 在权重变化率在 0.01 和 0.05 时, DeepInc 在绝大多数问题上都有明显
的加速. 在权重变化率为较大的 0.05 时, 多数验证任务性能相当, 但仍有少数验证任务 (x 轴上的验证任务) 有着极
大的加速. 在 UNSAT 验证问题 (验证结果为 UNSAT 的验证问题) 和 SAT 验证问题 (验证结果为 SAT 的验证问
题) 上分别加速 0.61 倍和 41.01 倍, 表明 DeepInc 在增量搜索反例方面表现突出, 这是由于权重变化不明显时, 修
改后的网络的反例往往存在于原始网络反例所在分支的附近, 我们的方法因此能够快速找到反例. 具体来说, 当权
重变化率为 0.001、0.01、0.03 和 0.05 时, DeepInc 的加速比分别为 1.25、0.6、0.51 和 0.11, 这表明随着修改的增
大, 增量求解的优势有所下降. 这种现象与我们的增量验证算法设计直觉一致.