引用

Teodora Baluta, Shiqi Shen, Shweta Shinde, Kuldeep S. Meel, Prateek Saxena , et al. Quantitative Verification of Neural Networks

and Its Security Applications[J]. 2019.

摘要

神经网络越来越多地应用于安全关键领域。这引起了人们对验证或证明神经网络的逻辑编码特性的兴趣。之前的工作主要集中于检查存在属性，其中的目标是检查是否存在任何违反给定兴趣属性的输入。然而，神经网络训练是一个随机过程，其分析中出现的许多问题需要概率和定量推理，也就是说估算满足给定属性的输入数量。为此，作者提出了一个新的、有原则的框架来定量验证神经网络的逻辑特性。作者的框架是第一个提供 PAC 式稳健性保证的框架，因为其定量估计值与真实计数的误差在可控和有界范围内。作者通过构建一个名为 NPAQ 的原型工具来实例化作者的算法框架，该工具能够检查二值化神经网络的丰富属性。作者展示了新兴的安全分析如何在 3 个应用中利用作者的框架：量化对抗性输入的鲁棒性、特洛伊木马攻击的有效性以及给定神经网络的公平性/偏差。

1 引言

神经网络正在被广泛采用，包括在可能对人类社会产生长期影响的领域。这些领域的例子包括刑事判决、毒品发现[、自动驾驶汽车、飞机防撞系统、机器人和无人机。虽然神经网络在诸如图像识别和机器翻译等一些具有挑战性的任务中达到了人类水平的精确度，但研究表明，这些系统在野外可能表现出不稳定的行为。

因此，人们对设计验证和测试神经网络的方法感兴趣。早期的工作集中于定性验证，其中，给定神经网络 N 和属性 P，人们关注的是确定是否存在违反 P 的输入 I 到 N。虽然此类可证明技术提供了价值，例如证明存在对抗性示例，但值得回顾的是，基于神经网络系统的设计者通常会对其行为做出统计声明，即一个给定的系统被声称以高概率满足兴趣属性，但并不总是如此。因此，许多神经网络分析需要定量推理，这决定了有多少输入满足 P。

本文的主要贡献是建立了一个新的分析框架，该框架将给定的神经网络 N 和 P 建模为逻辑约束集 φ，使得量化 N 满足 P 的频率的问题简化为 φ 上的模型计数。然后作者证明了定量验证是#P-hard 的。鉴于#P 的计算难度，作者寻求计算严格的估计，并引入近似定量验证的概念：给定规定的公差系数 ε 和置信参数 δ，作者估计 P 满足 PAC 式保证的频率，即计算结果在基础真值的乘法（1+ε）因子范围内，置信度至少为 1−δ。

作者的方法是将神经网络编码成合取范式（CNF）的逻辑公式。实现可靠性保证的关键是作者新的等基数概念，它定义了一种将神经网络编码为 CNF 公式 F 的原则性方法，从而使定量验证减少计算投影到 F 支持子集的 F 的满意赋值。然后，作者使用计算 F 的近似模型，在为 F 计数提供 PAC 式保证的实用工具中，这一技术得到了快速发展。最终结果是为神经网络提供了一个具有可靠性和精度保证的定量验证程序。

虽然作者的框架更为通用，但作者用称为二值化神经网络（或 BNN）的神经网络子类来实例化作者的分析框架。BNN 是具有+/-1 权重和阶跃激活函数的多层感知器。它们已被证明可在各种应用中实现高精度。由于它们的内存占用量小，推理时间快，它们已被部署在受限环境中，如嵌入式设备。作者观察到，BNN 的特定现有编码遵循作者的等基数概念，并在名为 NPAQ 的新工具中实现这些编码，并提供了通用方法以及特定编码的关键正确性和可组合性的证明。

2 方法和工具

2.1 方法及框架

定量验证使神经网络在安全分析（及以上）中有了许多应用。作者提供了 3 个应用程序，其中可以定量回答以下分析问题：

•稳健性：给定的神经网络有多少对抗性样本？与另一个神经网络相比，一个神经网络是否具有更多的对抗性输入？

•特洛伊木马攻击：可以训练神经网络，将具有“特洛伊木马触发”模式的特定输入分类到所需标签。特洛伊木马模型的中毒程度如何？即攻击成功针对多少个此类特洛伊木马输入？

•公平性：当存在某些输入特征时（例如，当输入记录的性别属性设置为“女性”与“男性”）神经网络是否会显著改变其预测？

等基数框架：作者的关键技术进步是一个新的算法框架，该框架使用可证明可靠的编码过程将（ϵ，δ）-NQV 减少为 CNF 计数。该过程将 N 和 P 编码为 φ，使得 φ 上的模型计数以某种方式计数 N∧P。这不是直截了当的。为了说明，考虑在布尔电路上计数的情况，而不是神经网络。为了避免编码中的指数膨胀，通常采用经典的等满意度编码，该编码保留了可满意度，但在编码过程中引入了新的变量。相等可满足性意味着原始公式是可满足的，当且仅当编码公式也是可满足的。然而，请注意，这种等满意度的概念不足以用于模型计数-编码公式可能是等满意度的，但可能比原始公式有更多的可满意度。

作者观察到一个更强的概念，作者称之为等基数，提供了一种原则性的方法来构造保留计数的编码。高级别的等基数编码可确保原始公式的模型计数可以通过对结果公式中的变量子集进行模型计数来计算。作者严格地定义了这个等基数关系，该模型对约束的计数相当于对其等基数编码的计数。在逻辑连接下，等基数关系是封闭的。这意味着约束的连接上的模型计数等同于其等基数编码的连接上的计数。因此，等基数 CNF 编码可以由布尔连接组成，同时在生成的公式中保留等基数。

根据这一关键观察，作者的程序还有两个子步骤。首先，作者展示了每个神经网络的等基数编码，并将其性质转化为单个等基数 CNF 公式。这意味着 ψ，φ 中共轭的等基数 CNF 编码的结合，保留了 φ 的原始模型计数。其次，作者展示了如何利用现有的具有（ϵ，δ）保证的 CNF 近似模型计数器来计算 ψ 中的变量投影子集。通过构造，最终结果保证作者对模型计数的最终估计具有有界误差，由 ε 参数化，置信度至少为 1−δ。

形式化：作者使用布尔逻辑的符号标准将上述概念形式化。赋值 σ 在变量 t 子集上的投影，表示为 σ| t，是将 t 赋值给 σ 中的值（忽略 σ 中除 t 以外的变量）。作者说公式 φ：t→ {0,1}是公式 ψ：u 的等基数 → {0,1}其中 t⊆ u、 如果：

引理 1（计数保存）。如果 ψ 与 φ 相等，则| R（ψ）↓ t |=| R（φ）|

引理 2（CNF 可组合性）。考虑 φi：Ti→ {0,1}与 ψi:ui→ {0,1}，使得 φi 等于 ψi，对于 i∈ {1,2}. 如果 u1∩u2=t，其中 t=t1∪t2，然后 φ1∧φ2 与 ψ1∧ψ2 相等。

最后计数估计数：利用 CNF 可组合引理，作者将神经网络 N 和性质 P 的连接上的计数问题分解为它们各自的等基数编码的连接上的计数问题。等基数编码保留计数，取其连词保留计数。接下来将展示如何将 N 编码为布尔 CNF 公式，从而使编码是等基数的。由于编码准确地保留了最初需要的计数，作者可以使用具有（ϵ，δ）保证的现成近似 CNF 计数器。因此，通过构造，最终计数保证是可靠的估计。

2.2 NPAQ 工具设计

作者的工具以一组经过训练的二值化神经网络 N 和一个属性 P 作为输入，并输出具有（ϵ，δ）保证的 P 保持 N 的“频率”。作者展示了从二值化神经网络到 CNF 的两步构造。作者坚持的主要原则是，在每一步中，作者正式证明作者获得了等基数公式。首先，作者使用基数约束来表示 BNN。第二步，作者选择使用基于排序的编码将基数约束编码为 CNF 作者证明了 NPAQ 在定理 4 中保持了等基数。最后，作者使用了一个近似模型计数器，它可以直接处理 CNF 公式的投影变量子集上的模型计数。

定理 5：NPAQ 是（ϵ，δ）-NQV

将不同的 BNN（f、f1、f2）编码为一组基数约束上的连词的示例。攻击者操纵 f 的目的是增加分类为 y=0 的触发器 x3=1 的输入。具体地说，为了获得 F1，将 f 的 x1、x2、x3 在 v2、v3、v4 的约束中的权重设置为 0（在下面用虚线突出显示）。为了获得 f2，作者将 w21 设置为 0。特洛伊属性 P=（y=0）∧（x3=1) 对于 f，一个输入（左）满足，而对于 F2，作者发现两个输入（右）满足。

图 1

表 1

作者可以将 BNN 中的每个块表示为基数约束的连接。基数约束是来自形式 x1+...+xn△c 的布尔变量 x1....xn。满足 △ ∈ {=,≤,≥}. 更具体地说，通过应用 Cardblk 规则（如下表），作者获得了输出块的基数约束的类似连接。获得 BNN 布尔公式表示的最后一步是将基数约束编码为 CNF。

表 2

3 实验

实施：作者在大约 5000 LOC 的 Python 和 C 中实现了 NPAQ。作者使用 Pytork（v1.0.1.post2）深度学习平台来训练和测试二值化神经网络。为了将 BNN 编码为 CNF，作者使用 PBLib 库构建了作者自己的工具，用于将基数约束编码为 CNF。生成的 CNF 公式用投影集进行注释，NPAQ 调用近似模型计数器 ApproxMC3 来计算解决方案的数量。作者配置了一个容许误差 ϵ=0.8 和置信参数 δ=0。2 作为整个评估过程中的默认值。

模型：作者的基准由 BNN 组成，作者在 BNN 上测试了 2.1 中概述的 3 个应用程序的属性。对于每个应用程序，作者使用以下 4 种不同的体系结构培训 BNN：

• ARCH1- BLK1(100)

• ARCH2- BLK1(50), BLK2(20)

• ARCH3- BLK1(100), BLK2(50)

• ARCH4- BLK1(200), BLK2(100), BLK3(100)

数据集：作者在 2 个标准数据集上训练模型。具体而言，作者量化了 MNIST 数据集上的健壮性和特洛伊攻击有效性，并估计了 UCI 成人数据集上的公平性查询。作者选择它们作为之前使用这些数据集的工作。

3.1量化鲁棒性

作者量化了模型的鲁棒性和防御的有效性，用于对抗性训练的模型强化。

结果是，总共有 480 个公式对应于经过对抗训练（强化）的模型。表 3 显示了对抗性样本和 PS（adv）的数量。观察 NPAQ 的声音估计，可以确认，对于 11/16 模型，普通 BNN 比硬化 BNN 更稳健，正如先前工作中所建议的那样。此外，安全分析师可以比较这两种防御。对于这两个时间点，Defense1 和 Defense2 仅分别对 2/8 和 3/8 型号执行普通 BNN。因此，对于作者训练的模型，防御 1 和防御 2 之间没有显著差异。人们可以使用 NPAQ 估计来选择一个对良性样本和较少对抗性样本都具有高精度的模型。例如，在 epoch 1 使用 Defense2 训练的 Arch4 模型具有最高的准确性（88.85%）和 549 个对抗性样本。

表 3

3.2量化特洛伊木马攻击的有效性

特洛伊木马攻击的有效性通常在选定的测试集上进行评估，该测试集取自具有嵌入式特洛伊木马触发器的特定图像分布。给定一个特洛伊木马模型，人们可能会对评估该特定测试发行版之外的特洛伊木马的有效性感兴趣。具体而言，NPAQ 可用于计算在所有可能的图像空间中，有多少带有特洛伊木马触发器的图像被分类到所需的目标标签。如表 4 显示特洛伊木马攻击的有效性。TC 表示攻击的目标类别。所选历元报告历元编号，其中模型具有每个体系结构和目标类的最高 PS（tr），x 表示超时。

表 4

木马程序可以任意不同于作者的程序；使用 NPAQ 进行验证并不以任何方式依赖于它。作者的程序改编自 Liu 等人的程序，该程序适用于具有实值权重的模型。对于一个给定的模型，它选择与前一层连接最强的神经元，即基于权重的大小，然后生成触发器，使所选神经元的输出值最大化。这种启发式不适用于 BNN，因为它们已经{−1,1}权重。在作者的自适应中，作者从内部层随机选择神经元，其中输出值通过梯度下降最大化。这种策略背后的直觉是，这些选定的神经元将在特洛伊木马输入下激活，产生所需的目标类。对于此过程，作者需要一组特洛伊木马和良性样本。在作者的程序中，作者假设作者可以访问 10000 张良性图像，这与 Liu 等人的工作不同。Liu 等人的工作是从模型本身生成的。与前面的工作一样，使用这两个集合，作者重新训练模型以输出特洛伊木马输入所需的类，同时预测良性样本的正确类。

3.3量化公平模型

作者使用 NPAQ 来估计给定神经网络处理相似输入的频率，即单个特征值不同的输入也不同。

量化偏差的方向：对于敏感特征的变化导致预测变化的输入集，可以进一步量化变化是否“偏向”敏感特征的特定值。例如，使用 NPAQ，作者发现在作者所有的模型中，从“已婚”到“离婚”的变化会导致预测收入从低到高的变化。对于 ARCH1，当所有其他特征相同时，性别为“男性”的个体（9.13%）比“女性”（2.07%）更有可能被预测拥有更高的收入。然而，对于 ARCH4，从“女性”到“男性”的变化更可能导致分类器输出从高到低的变化（10.19%）。同样，对于种族特征，不同的模型表现出不同的偏向“方向”。例如，从“白色”到“黑色”的变化与正变化相关，即从低收入到高收入，例如 ARCH2。其他 3 个模型，ARCH1、ARCH2 和 ARCH4 将预测，如果种族属性设置为“黑色”，则具有相同特征（敏感特征除外）的个体可能收入较低。

表 5

使用 NPAQ，作者可以区分模型对敏感特征的不公平程度。可以对其他公平性属性进行编码，例如定义个体之间的相似性度量，其中非敏感特征在一定距离内，类似于个体公平性。NPAQ 对于此类公平性公式是有帮助的。

4 结论

作者提出了一种新的算法框架，用于形式 PAC 式神经网络可靠性的近似定量验证。该框架定义了将神经网络等基数编码为 CNF 公式的概念。这种编码保留计数，并确保逻辑连接下的可组合性。作者为二值化神经网络实例化了这个框架，构建了一个名为 NPAQ 的原型工具。作者用三个具体的安全应用程序中出现的几个属性来展示它的实用性。

致谢

本文由南京大学软件学院 2021 级硕士赵辰熹翻译转述。