深度神经网络的属性推理_深度神经网络的属性推理有哪些

引用

D. Gopinath, H. Converse, C. Pasareanu and A. Taly, "Property Inference for Deep Neural Networks," 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), San Diego, CA, USA, 2019, pp. 797-809, doi: 10.1109/ASE.2019.00079.

摘要

我们提出了自动推断前馈神经网络的形式属性的技术。据我们观察，前馈神经网络的逻辑有很大一部分是通过其神经元的激活状态来捕获的。我们提出了基于神经元决策的模式提取模式，通过将这些神经元的决策作为前提条件，来推理某些输出属性，例如，最终的预测类别。我们提出了提取输入属性的技术，在输入空间上编码来标记给定的输出属性和层属性的谓词，代表在隐藏层中捕获的网络属性，最终推理期望的输出结果。我们将我们的技术应用在 MNIST 和 ACASXU 上的网络。我们的实验强调了推理属性在各种任务中的应用，如解释预测、提供鲁棒性保证、简化证明和网络提炼等。

1 介绍

深度神经网络(DNNs)已经成为解决复杂计算任务的强大机制，在执行这些任务时取得了较为满意的效果，有时甚至超过了人类的能力。然而，DNNs 的使用越来越多的同时，也带来了一些安全和可靠性方面的问题。造成这种结果的有诸多因素，其中包括缺乏鲁棒性。众所周知，包括经过高度训练的 DNNs 在内的网络，很容易受到对抗性扰动的影响。对输入的微小（几乎是不可感知的）变化会导致错误分类。如果在自动驾驶的感知模块中使用这样的分类器，网络受对抗性图像的干扰所导致的错误决策会产生灾难性的后果。DNNs 还存在着缺乏可解释性的问题：人们不太了解网络为什么会做出某种预测，这阻碍了 DNNs 在安全关键领域的应用，如司法、银行、医学等。最后，在设计神经网络时，神经网络只从实例中学习，往往没有高层次的需求规范，这阻碍了神经网络具有严格的逻辑推理。在设计更传统的安全攸关系统时，这种逻辑性是必要的。

在本文中，我们提出了自动推断前馈神经网络的形式属性的技术，这些属性的形式为 Pre ? Post。Post 是一个后置条件，说明所期望的输出行为，例如，网络的预测结果是某一具体的类别。本文基于输入属性开展了研究。它编码了输入空间中的谓词，暗示了给定的输出属性。此外，本文还进一步研究了层属性，它将在中间层观察到的具有共同特征的输入进行分组，最终影响了网络的输出行为。

设置网络属性是构建网络的必要前置过程，该行为会导致诸多结果。在本文中，我们推断出 DNN 中神经元的决策模式所对应的属性。这种模式规定了不同层中哪些神经元处于激活或未激活状态。对于实现 ReLU 激活函数的神经元，这相当于神经元的输出是大于零（激活）还是等于零（未激活）。对于其他更复杂的特性（例如，使用一个正阈值而不是零的激活函数，在神经元值上使用线性组合），这些都是留待以后的工作中研究。

我们定义了基于模式的输入属性，这些模式约束了直到中间层的所有神经元的激活状态（激活或未激活）。这样的模式在输入空间中形成了凸状谓词。使用凸函数的特性在此处是很有必要的，因为它使推断出的属性很容易被可视化且具有较强的解释性。此外，凸型谓词可以用现有的线性编程求解器有效地求解。类似地，我们基于约束中间层激活状态的模式来定义层属性。层属性的模式定义了中间层值上的凸区域，可以表示为输入空间中的凸区域的联合。

研究决策模式的另一个动机是这类似于程序分析中的路径约束。不同的神经元决策模式也能捕捉到不同的 DNN 行为。我们认为，根据决策模式提取出简洁的输入输出属性是可行的。这些属性共同解释了网络的行为，可以作为网络的形式化规范。我们提出了两种提取网络属性的技术。我们的第一种技术是基于迭代的决策模式，同时利用现有的决策程序。我们使用了决策程序 Reluplex，旨在证明前馈式 ReLU 网络的属性，但也可以使用其他决策过程。我们的第二种技术使用决策树学习直接从数据中学习层属性的模式。学习到的模式可以使用决策程序进行最终检验。为了代替最终检验，我们可以在一个数据集上对学习到的结果进行实证验证，以验证其准确性。

我们认为这项工作是研究 DNNs 形式属性的第一步。作为一个概念的证明，我们提出了几个不同的应用。我们学习了 MNIST 网络的输入属性和层属性，并展示了它们在保证鲁棒性、解释网络的决策和调试网络的错误分类方面的用途。我们还研究了将中间层的模式作为插值器，用于证明给定的输入-输出属性的网络模型，即无人机控制的安全关键系统（ACAS XU）。这些学习到的模式有助于分解证明，从而使其在计算上更有效率。最后，我们讨论了一个略带争议的应用，即提炼 DNNs 的行为中学习到的模式。关键的想法是将可靠性高的模式作为提炼规则，直接决定网络的预测，而不需要评估整个网络。这样做的结果是在不损失太多精度的情况下大幅提高了速度。

2 网络属性

如果一个隐藏层中的所有神经元都馈入下一层的所有神经元，那么一个前馈网络就被称为完全连接的网络；图 1 中的网络就是这样一个网络。卷积神经网络（Convolutional Neural Networks，CNNs）类似于 ReLU 网络，但除了全连接层之外，它们还可能包含卷积层，这些卷积层用不同的滤波器计算出输入的多个卷积，然后应用 ReLU 激活函数。为了简单起见，我们将讨论的重点放在 ReLU 网络上，但我们的工作适用于所有的片状线性网络，包括 ReLU 和 CNN。

我们的目标是提取网络行为的简洁的输入-输出特征，可以作为网络的正式规范。网络本身提供了一个输入-输出映射。理想的情况下，我们应该将导致相同输出的输入组合在一起，并以简洁的数学形式表达出来。输入属性是对输入空间的一个谓词，所有满足它的输入都会得到满足该属性 P 的输出。以一个分类网络的输出属性为例，假设理想的预测类别是 c，那么 P(Y)::=argmax(Y)=c。

在本文中，我们推断出输入属性，这些输入的特征是由网络以相同的方式处理的输入，也就是说，它们遵循相同的激活模式，并在输入空间中定义了凸区域。对于一个特定的输出属性（例如一个特定的预测），可能有许多这样的凸区域。在实际应用中，精确计算这些区域的联合代价较高，但我们最终证明了，即使是计算这些区域的子集也能满足许多场景下的应用。

我们进一步研究了层属性，在中间层编码共同的属性，这些属性预示着了所需的输出结果。神经网络的工作原理是通过在输入数据上采用若干个隐藏层，提取数据的重要特征，然后根据这些特征做出决策。因此，层属性可以潜在地捕捉到提取的特征上的共同特征，使我们能够洞察到网络的内在工作原理。与输入属性类似，我们试图通过研究网络的激活模式来推断层属性。与输入属性不同的是，层属性并不映射到输入空间中的凸区域，而是映射到凸输入区域的联合。

2.1 输入属性

为了构建输入属性，我们对输入属性进行推测，这些输入属性是输入空间中的凸谓词，暗示着给定的后置条件。考虑到前馈 ReLU 网络编码属于高度非凸函数，输入属性的存在本身就值得研究。为了识别输入属性，我们考虑决策模式，其中对于模式中的每个神经元 N，所有馈入 N 的神经元也包括在该模式中。我们称这种模式为闭合。我们表明，闭合模式捕获了输入空间中的凸谓词。

2.2 层属性

虽然推断的输入属性可能很容易解释，但它们往往支持的范围很小。例如，一个基于输入 X 的激活特征定义的属性可能只被 X 和可能是语法上接近 X 的其他几个输入所满足。为此，我们将注意力集中在中间层的决策模式上，以捕捉高级特征。

注意，图层属性在该层的值空间中是凸的，但在输入空间中不是凸的。然而，将图层属性表示为输入前提条件的解结是较为容易的。这是通过将一个图层模式与所有可能的模式扩展到（直接或间接）馈入该图层的神经元上的所有可能的模式来实现的。每个这样的扩展模式都是闭合的，因此是凸的。

2.3 解释和使用推断网络属性

鲁棒性保证和对抗样本。我们为证明正确的输入属性和层属性定义了预测后置条件。在输入空间中，网络保证对相同标签对应相同的区域，此时网络是鲁棒性的。从模式候选者的反例中产生的输入，由于它们（在欧几里得空间中）接近于分类不同的输入（区域），因此代表了潜在的对抗样本。

解释网络的预测依据。神经网络因是复杂的黑箱而一直以来备受质疑。解释神经网络的一个重要难题是：理解为什么网络会对一个输入进行某种预测。我们对于预测属性的研究（确保预测是某一类的）可以用来获得这样的解释。但是，只有当这些属性本身是可以理解的时候，这些属性才是有用的解释。当输入空间是低维的时候，这样的区域很容易解释。

对于具有高维输入的网络（例如，图像分类网络），输入属性可能难以解释或可视化。这里的传统方法是通过给每个输入特征分配一个重要性权重（称为属性）来解释预测。归因法可以被可视化为一个热图叠加在输入的可视化上。在此基础之上，我们提出了两种不同的方法来从输入属性中获得类似的可视化。我们注意到，与归因法相比，我们提出的输入属性有助于解释单个输入的预测，而我们提出的输入属性有助于解释输入空间的区域预测。

3 计算网络属性

现在我们介绍两种技术，从前馈网络中构建输入和层属性的前馈网络 wrt 凸输出属性 P。

3.1 决策模式的迭代

这是一种提取输入属性的技术，它利用了一个现成的神经网络决策程序。在这项工作中，我们使用了 Reluplex，但也可以使用其他的决策程序。

3.2 利用决策树学习挖掘层属性

上一节中描述的贪心算法的计算成本很高，因为它每一步都要调用一个决策过程。我们现在提出一种成交相对较低的技术，它依赖于数据，避免了多次调用决策过程。我们的想法是观察大量输入的激活特征，并学习各种输出属性的决策模式。在本文中，我们使用决策树学习来提取基于层中神经元的激活状态（激活或未激活状态）的紧凑规则。采用决策树是很有必要，因为决策树能够根据各种信息理论的衡量标准得到一个决策模式，并且是紧凑的（因此具有较高的可靠性）。所得到的模式是经过实证验证的层属性，可以通过对决策过程的一次调用来正式检验。

4 应用

在本节中，我们讨论了计算输入属性和层属性的案例研究，并将其用于不同的应用。我们用 Python3.0 和 Tensorflow 实现了我们所有的算法。我们的 Python 笔记本连接到 Python2Google 计算引擎后端，并分配了 12Gb RAM。我们使用 Reluplex 来进行证明，它只限于 ReLU 网络。为了执行决策模式，我们修改了 Reluplex 来约束中间神经元值。随着更多的神经网络的决策程序变得可用，我们计划将其纳入我们的工具中，从而扩展其适用性。Reluplex 的运行是在 Ubuntu v16.04（8 核，64GB RAM）的服务器上完成的。我们使用线性编程求解器 pulp 2.3.1 来求解欠近似框。我们计划在最终版本中提供实现和网络。

4.1 对 ACASXU 的分析

我们首先讨论了 ACAS XU 的分析，ACAS XU 是无人驾驶飞机控制的安全关键型防撞系统。ACAS X 是美国联邦航空局(FAA)正在开发的飞机防撞系统家族。ACAS XU 是针对无人机的版本。作为对标无人机的版本，它接收无人机(机身)和附近任何入侵的无人机的传感器信息，然后发出水平转弯警告，以防止碰撞。输入的传感器数据包括：

(1)Range：自有船与入侵者之间的距离；

(2)θ：入侵者相对于自有船的航向角度；

(3)ψ：入侵者相对于自有船的航向角度；

(4)vown：自有船的速度；

(5)vint：入侵者的速度；

(6)τ：失去垂直分离的时间；

(7)aprev：以前的警告。

FAA 正在探索 ACAS XU 的一个实现，它使用了 45 个深度神经网络的阵列，我们在此选择了一个网络来讨论。五种可能的输出如下：

(0)Clear-of-Conflict(COC)；

(1)Weak Left；

(2)Weak Right；

(3)Strong Left；

(4)Strong Right。

我们分析的网络由 6 个隐藏层组成，每层有 50 个 ReLU 激活节点。我们使用了 384221 个已知标签的输入，ACASXU 网络采用 Reluplex 进行了分析。

4.2 对 MNIST 的分析

我们还基于大量的手写数字集合的数据集，对图像分类网络 MNIST 进行了分析。它有 60,000 个训练输入图像，每个图像的特征是 784 个属性和属于 10 个标签中的一个。我们首先分析了从 Reluplex 分布的简单网络（包含 10 层，每层 10 个 ReLU 节点）对于蒸馏（一种常见的模型压缩方法）实验，我们使用了一个更复杂的 MNIST 网络。

1）属性推理。我们使用迭代放宽法提取输入属性，使用决策树学习法提取层属性，最终证明了我们的方法在图像分类中的可行性。与 ACAS XU 相比，图像分类涉及的输入空间要大得多。

2）解释网络预测。我们进一步计算了推理属性的近似值域，并将其可视化。在图 2 中，我们展示了训练集中三个不同图像对应的输入属性的可视化。第一列显示的是原始图像。第 2 列和第 3 列分别显示了在计算出的欠逼近框中所有像素设置为最小值和最大值的图像。第 4 列、第 5 列和第 6 列分别将每个像素设置为框中的均值、随机选择的均值以下和随机选择的均值以上。

3）误分类。误分类的输入实例较少，并且分布在整个输入空间中，开发人员很难理解其原因，也很难修复其底层问题。

4.3 蒸馏

我们最后的实验是评估层属性在蒸馏网络中的使用。本文的核心想法是将中间层的预测属性作为蒸馏规则。对于满足该属性的输入，我们节省了从中间层开始评估网络的推理成本。我们用一个比较复杂的 MNIST 网络对这个想法进行了初步评估，该网络有 8 个隐藏层；两个卷积层、一个最大池化层、两个卷积层、一个最大池化层和两个全连接层。我们使用决策树算法获得层模式，然后对其进行实证验证(使用 5000 张图像的验证集)，选出精度高于阈值 τ 的层。选择的属性被用作满足这些属性的输入的提炼规则。我们使用一个保留的测试数据集，测量不同值 τ 的混合设置的总体精度和推理时间。

图 3 显示了由 4608 个神经元组成的第一个最大池化层的蒸馏结果。X 轴显示的是用于选择属性的经验验证阈值。极右点（阈值>1）对应的是没有选择属性，因此没有触发蒸馏。图中显示了当阈值 τ 在 0.9 到 1.0 之间变化时，整体精度和推理时间的趋势。观察到，在阈值 τ=0.98 的情况下，推理时间可以节省 22%，而精度从 0.9943 下降到 0.9903，这是相当有希望的。正如预期的那样，降低阈值进一步考虑了更多的属性，从而减少了推理时间和精度。

5 结论

本文提出了提取神经网络输入输出属性的技术，并讨论了它们在解释神经网络、保证神经网络鲁棒性、简化证明和提炼网络方面的应用。随着神经网络的决策程序越来越多，我们计划将其纳入我们的工具中，从而扩展其适用性和可扩展性。我们还计划利用这些决策模式来获得神经网络的并行验证技术，并研究推理属性的其他应用，如可靠性和安全攸关系统的信任建模、对抗性检测等。

致谢

本文由南京大学软件学院 2019 级硕士刘佳玮转述