引用

Baluta T, Chua Z L, Meel K S, et al. Scalable quantitative verification for deep neural networks[C]//2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE). IEEE, 2021: 312-323.

摘要

尽管近年来深度神经网络（DNNs）的应用取得了巨大成功，但其可信度仍然是一个挑战。为了应对这一挑战，人们提出了测试和验证技术。但是，这些现有的技术要么提供对大型网络的可扩展性，要么提供形式上的保证，而不是两者都有。在本文中，我们为深度神经网络提出了一个可扩展的定量验证框架，即一个测试驱动的方法，该方法带有形式保证，即所需的概率属性得到满足。我们的技术执行足够多的测试，直到形式上的概率属性的合理性可以被证明。它可以用来证明确定性和随机性的 DNN 的属性。我们在一个叫做 PROVERO 的工具中实现了我们的方法，并将其应用于认证 DNN 的对抗性稳健性的背景中。在这种情况下，我们首先展示了一种新的攻击诊断性的鲁棒性措施，它提供了一种替代目前报告的完全基于攻击的鲁棒性评估方法。其次，PROVERO 为大型 DNN 提供了鲁棒性证明，而现有的最先进的验证工具无法产生此类结论性的结果。我们的工作为验证真实世界的深度神经网络所捕获的分布属性铺平了道路，即使测试人员只有对神经网络的黑盒访问权，也能获得该证明的保证。

1.介绍

在过去的几年里，深度神经网络（DNNs）在自动驾驶、无人机或机器人等领域的应用越来越多，错误的预测会带来严重的后果。稳健性、隐私性和公平性已经成为安全采用 DNN 所需要解决的核心问题。因此，人们越来越关注对神经网络的测试和验证。

深度神经网络环境中最早的形式验证方法专注于定性验证，即系统是否满足给定的规范。这类方法存在三个不足：

1) 它们需要对模型的白盒访问和专门的程序来将 DNN 转换为规范，从而限制了它们的通用性。

2) 底层可行性求解器的性能随着非线性约束的使用而严重下降，导致分析无法扩展到更大的模型。

3) 现有技术仅限于确定性神经网络，而广泛的研究工作已投入到随机 DNN 中，尤其是为了增强鲁棒性。

我们的工作包括以下：

·提出了一种新的神经网络定量验证算法。该框架相当通用：它只假设对被验证模型的黑盒访问，并且只假设能够从属性被断言的输入分布中进行采样。

·实现了一个工具 PROVERO 并在工具中实施了我们的方法，该工具将对抗性鲁棒性的量化验证扩展到大型真实世界 DNN，包括确定性和随机性。

·在证明对抗性鲁棒性的背景下，我们的实证评估提出了一种新的攻击不可知的鲁棒性衡量标准，并表明 PROVERO 可以在现有最先进的定性验证无法提供结论性结果的情况下生成具有高置信度的证明。

2.应用：对抗性稳健性

2.1.采样

给定一个可采样输入空间 I 和神经网络 f 上的属性 ψ，我们的方法通过独立于 I 进行采样 N 次来工作。我们测试每个样本作为输入。令 Xi 是一个 0-1 随机变量，表示对样本 i 的试验结果，其中 Xi=1，如果 ψ(x,f,Φ)为真，否则 Xi=0。设 X 是随机变量，表示在 X1,X2,...,XN 中的性质为真的试验次数。

在此基础上我们提出了一个定理：

应用 Lemma4.1 的唯一假设是，所有样本都是独立的。如果神经网络在一次试验（或在一个样本下的执行）中不计算信息并在另一次试验中使用它，正如我们研究的所有神经网络的情况一样，试验将是独立的。概率取决于神经网络和输入分布，p=Ex∼D[ψ(x,f,Φ)]，其中 D 是 I 上的分布。使用基于采样和切尔诺夫界线的框架具有相当大的普遍性。应用该定理的唯一假设是所有样本都是独立的。如果神经网络在一次试验（或在一个样本下执行）不计算信息并在另一次试验中使用它，试验将是独立的。对于随机 DNN，我们可以认为第 i 次试验是在给定的样本上评估一个可能不同的神经网络（从一些函数分布中取样）。在这里，由于神经网络本身使用的随机化，输出随机变量可能不是相同分布的。然而，即使对于非同分布的试验但独立的试验，Lemma4.1 仍然可以使用。

我们接下来讨论一种基于估计的策略，它以一种直接的方式应用切尔诺夫界线。这样的解决方案对于对抗性稳健性的定量验证具有很高的样本复杂性。然后，我们提出了基于假设的解决方案，这种解决方案是合理的，对于现实世界的 DNN 来说，具有更好的经验样本复杂性。我们提出的算法仍然只依赖切尔诺夫式的界限，但经过精心设计，在内部改变参数（对其调用切尔诺夫界限），以减少调度断言属性所需的样本数。

2.2一个基于估计的解决方案

通过抽样定量验证属性的一种方法是直接将切尔诺夫界限应用于 N 次试验中均值的经验估计，这是一种常见的评估方法。通过我们提出的定理，可以证明 p 的均值在 p 的误差范围内，并且置信度高于。在这种解决方法中，样本数量随着的减少而增加，即使对于像 BranchyNet 这样的优化架构来说，ResNet（152 层）的每个样本的平均推理时间为 70.9 毫秒，估计方法也需要超过 1083 个 GPU 计算小时,这个成本是非常高的。

我们的工作提供了新的算法，平均利用更少的样本。在 BranchyNet 的例子中，如果真实的概率 p 是 0.3，我们的方法需要 4246 个样本来返回一个信心大于 0.99 的'No'答案。估算算法的主要问题是，它在决定所需的样本数量时没有利用给定的 θ 的知识。

2.3我们的方法

我们提出了新算法，其关键思想是使用更简单的（样本复杂性）假设检验来尽早决定“是”或“否”。给定阈值 θ 和误差 η，高级思想是在 θ 的左侧和 θ+η 的右侧提出替代假设。我们选择假设和抽样程序，以便如果 θ 左侧的任何假设为真，那么我们可以返回“是”。类似地，如果 θ+η 右侧的任何假设为真，那么我们可以返回“否”。因此，当真实概率 p 离阈值 θ 更远时，我们可能会更快地返回。

3.算法

我们为定量认证提供了一种自适应算法，它缩小了证明搜索中的区间大小，类似于二元搜索策略。

3.1BINPCERTIFY 算法

我们提出了一种算法 BinPCertify，其并非预先固定间隔，而是通过将间隔减半来缩小搜索范围。BinPCertify 的用户指定输入参数是阈值 θ、误差界限 η 和置信度参数 δ。然后，BinPCertify 算法在内部调用过程 CreateInterval 来创建证明区间和反驳区间。请注意，对于反驳区间，我们保持左侧固定，θi=θ+η，对于证明区间，我们保持右侧固定，即 θ2=θ。对于 BinPCertify 的每次迭代，我们使用的策略是通过将最外面的阈值移近 θ 来将间隔减半。对于这些中间假设，Tester 检查它是否可以证明或反驳断言 p<θ。它继续交替证明和反驳假设，直到两个区间的大小都小于误差界限 η。如果仅在阈值的一侧 CreateInterval 返回大小为 a>η 的区间，BinPCertify 将检查这些假设。如果 CreateInterval 返回的证明和反驳区间的大小为 η，则直接在(θ,θ+η)上调用最终检查并返回给用户。

3.2. TESTER 原语

测试器将两个阈值 θ1,θ2 作为输入，使得 θ1<θ2 和置信度参数，当 θ1<θ2 置信度高于 δ 时返回“是”，当 p<θ2 置信度高于 δ 时返回“否”.如果 p∈(θ1,θ2]，则测试器没有保证返回。

引理 5.2：给定阈值(θ1,θ2)和置信度参数 δ，测试者具有以下健全性保证：

我们在图 3 进行说明：它分别显示了(t,ηi,η2)和 p=θi 和 p=θ2 时 p 的两个概率分布。p<θi 情况的分布将进一步向左移动，而 p>θ2 情况的分布将进一步向右移动；所以这些是要考虑的极值分布。

图 3：测试人员考虑允许区分 p<θi 或 p>θ2 的边界 t=θi+ηi=θ2-η2

取最大值可确保 p<θi 和 p>θ2 这两个假设的概率同时处于上限。我们将详细分析留给补充材料。

4.评估

实验的数据集和模型如下表所示：

表 I：我们评估中使用的神经网络架构。

我们将从可扩展性、攻击评估中的效用、是否适用于随机模型和性能这四个方面来进行评估。

4.1攻击评估中的效用

PROVERO 提供了一种新功能：我们可以在给定测试输入 x 的指定扰动范围内测量对抗样本的比率。我们在这个实验中的主要结果是 ϵHard 与 ϵmin 密切相关。图 4 和图 5 直观地显示了两种模型的相关性：它表明这两种单独攻击发现的扰动边界不同，但都与 PROVERO 产生的认证实例的对抗性程度相关。对于比较白盒攻击成功的所有案例，所有模型的 Pearson 相关性在表 II 中报告。PGD、ϵPGD 和 ϵHard 在所有模型中发现的扰动之间的平均 Pearson 相关系数为 0.858，而 C&W、ϵC&W 和 ϵHard 发现的扰动之间的平均 Pearson 相关系数为 0.8438。我们为每个模型拍摄 25 张图像来计算相关性。显著性水平很高（所有情况的 p 值都低于 0.01）。

PROVERO 是合理的，因此对抗程度 ϵHard 的估计值以高概率(99%)接近真实情况。该指标是一种与攻击不可知的指标，通过统一采样计算，无需对模型进行白盒访问。强相关性表明 PGD 和 C&W 攻击发现较小的 ϵmin 用于更容易的认证实例，而较大的 ϵmin 用于较难的实例。这表明，在比较两种模型的鲁棒性时，可以将对抗程度视为一种有用的攻击不可知指标，补充对特定攻击的评估。

4.2可扩展性

我们发现 PROVERO 对于 BM2 小于 2%的输入案例和 BM1 小于 5%的输入案例返回“无”，即 PROVERO 无法最终证明小于或大于查询的阈值。对于所有其他情况，PROVERO 提供“是”或“否”结果。

作为比较，我们选取了现有的工具 ERAN。我们在 BM1 上成功运行了 ERAN。ERAN 中共有 4 个分析。分别是 DeepZono、DeepPolydomains、RefineZono 和 RefinePoly 我们选取这 4 种分析中最具扩展性的进行比较，即 DeepZono。

图 6 显示验证模型减少了更高的扰动。这与 ERAN 论文中的发现一致：对于非鲁棒模型和更高的值，ERAN 要么需要更长的时间，要么更不精确。在 ERAN 不确定的所有情况下，PROVERO 在所有 35431 个测试图像和 ϵ 的值的 600 秒内成功完成。在超过 95%的情况下，PROVERO 会产生高可信度的“是”或“否”结果。

4.3是否适用于随机模型

到目前为止，在我们的评估中专注于确定性 DNN，但是，PROVERO 可以证明随机 DNN 的鲁棒性。为了证明这种普遍性，我们采用了一个通过称为 PixelDP 的训练过程获得的模型，该模型添加了不同的私有噪声以使神经网络更加稳健。PixelDP 网络的推理阶段使用随机化：它不是选择具有最大概率的标签，而是从噪声层采样并计算输出值的期望。PixelDP 还产生经过认证的扰动边界，它保证模型对于给定的输入图像是健壮的。诸如 ERAN 之类的定性验证工具需要白盒访问并使用确定性模型，因此它们无法验证随机 PixelDPDNN 的鲁棒性。我们在这个实验中的发现是，PROVERO 可以证明比 PixelDP 产生的定性证明大得多的扰动边界的低对抗密度。

4.4性能

我们发现对于 η=0.01、θ=0.01，估计方法需要比 PROOVERO 多 27 倍的样本，对于 BM1 的 η=0.001、θ=0.0001 估计方法需要多 687 倍的样本。对于 BM2 中较大的模型和值 η=0.001,θ=0.001，估计方法和 η=0.01,θ=0.01 需要比 PROVERO 多 74 倍的样本。

表 II：使用 Pearson 系数(p)的 BM1 和 BM2 模型的 PGD 和 C&W 攻击的攻击相关性。统计显着性 p<0.01。

5.结论

PROVERO 介绍了一种验证神经网络定量属性的算法，只假设黑盒访问，并且测试样本复杂度比比较基线要好得多。我们的算法特别提供了一种强大的、与攻击无关的新方法来评估深度神经网络的对抗性稳健性。

鸣谢

本文由南京大学软件学院 2021 级硕士林聚翻译转述，肖媛审核。