1 introduction

在过去的几年中，神经网络的重大进步导致它们在关键领域（包括医疗保健，自动驾驶汽车和安全性）的部署不断增加。但是，最近的工作表明，尽管神经网络取得了巨大的成功，但它们经常会犯下危险的错误，尤其是对于罕见的极端情况输入。例如，大多数先进的神经网络已经显示出可以通过向常规输入中添加人类难以察觉的微扰来专门设计的对抗输入产生不正确的输出[36、14]。类似地，最新技术的神经网络已显示出照明或输入图像方向上看似微小的变化会引起严重的错误预测[29，30，37]。这样的错误可能造成灾难性的后果，甚至可能导致致命的后果。例如，特斯拉在自动驾驶模式下的汽车最近造成了致命的车祸，因为它未能在明亮的天空中检测到一辆白色的卡车，上面有白云[3]。

最小化此类错误的原则方法是确保神经网络满足简单的安全性/安全性，例如在给定图像的特定L范数内不存在对抗性输入，或者对同一对象的图像的网络预测不变性在不同的照明条件下。理想情况下，给定一个神经网络和一个安全属性，自动检查器应保证网络可以满足该属性，或者应找到表明违反安全属性的具体反例。这种自动检查器的有效性取决于他们可以多么准确地估计网络的决策边界。

但是，严格估计具有分段线性激活函数（例如ReLU）的神经网络的决策边界是一个难题。虽然每个ReLU节点的线性片段可以划分为两个线性约束并有效地进行单独检查，但是线性片段的总数与网络中节点的数量成指数增长[25，27]。因此，对于任何现代网络，这些部件的所有组合的详尽枚举极其昂贵。同样，基于采样的推理技术（例如黑盒蒙特卡洛采样）可能需要大量数据才能在决策边界上生成严格的准确边界[11]。

在本文中，我们提出了一种新的有效方法来严格检查神经网络的不同安全属性，该方法明显优于现有方法多个数量级。具体来说，我们介绍两种关键技术。首先，我们使用符号线性松弛，将符号区间分析和线性松弛相结合，通过在区间传播过程中跟踪输入之间的松弛依存关系（当实际依存关系变得太复杂而无法跟踪时），来计算网络输出上的更严格边界。其次，我们引入了一种称为定向约束细化的新技术，以迭代地最小化在松弛过程中引入的错误，直到满足安全属性或找到反例为止。为了使优化过程高效，我们确定可能被高估的节点，即在松弛期间引入的不准确性可能会影响对给定安全性检查的节点，并使用现成的求解器仅关注那些节点以进一步提高缩小输出范围。

我们将我们的技术作为Neurify的一部分实施，该系统用于严格检查神经网络的各种安全属性集，该安全属性比现有技术可以处理的神经网络大10倍。我们使用Neurify来检查在五个不同数据集上训练的九个不同网络的六种不同类型的安全属性。我们的实验结果表明，平均Neurify比Reluplex [17]快5000倍，比ReluVal [39]快20倍。

除了对安全特性的形式分析外，我们认为我们用于有效估计网络的紧缩和严格输出范围的方法也将有助于指导鲁棒网络的训练过程[42，32]和提高神经网络做出的决策的可解释性[ 34，20，23]。

2 Background

我们基于区间分析[10]和线性松弛[39]这两项先前技术来分析神经网络。我们简要地介绍了它们，并向感兴趣的读者推荐[10,39]以了解更多细节。

2.1 Symbolic interval analysis

区间算术[33]是一种灵活高效的方法，可以通过计算和传播函数中每个操作的输出间隔来严格估计给定输入范围的函数的输出范围。 但是，幼稚的间隔分析会遭受较大的高估误差，因为它会忽略间隔传播期间的输入依存关系。 为了最大程度地减少此类错误，Wang等人。 [39]使用符号间隔来跟踪相关性，方法是维护每个ReLU的上下限线性方程式，仅具体化那些在给定输入间隔内表现出非线性行为的ReLU。

区间算术 = 区间算法 = 区间分析
符号传播 = 符号区间分析
符号传播是区间算术的升级版

Wang的论文中提到，将仅在第三种情况下具体化该节点的输出区间，因为这种情况下的输出不能用单个线性方程表示。

2.2 Bisection of input features.二分输入特征

略

2.3 Linear relaxation

Ehlers等人[10]使用ReLU节点的线性松弛来严格过分逼近每个ReLU引入的非线性约束。 然后，可以使用线性求解器有效地求解生成的线性约束，以获取给定输入范围内神经网络输出的界限。 考虑简单的ReLU节点，该节点获取输入z’分别具有上限和下限u和l，并产生输出z，如图1所示。

不幸的是，Ehlers等人 [10]使用朴素区间传播来估计u和l，造成了很大的过度逼近误差。 此外，他们的方法不能有效地精细化近似的边界，因此不能从增加的计算能力中受益。

3 Approach

在本文中，我们做出了两个主要贡献，以将形式安全性分析扩展到比先前工作[17,10,42,39]中评估的网络大得多的网络。首先，我们以一种新颖的方式将符号间隔分析和线性松弛（在第2节中进行了描述）结合起来，以创建一种效率更高的传播方法-符号线性松弛-可以实现更为严格的估计（在第4节中进行了评估）。其次，我们提出了一种在符号线性松弛过程中识别被高估的中间节点（即其输出被高估的节点）的技术，并提出了定向约束细化以迭代地细化这些节点的输出范围。在第4节中，我们还显示了该方法减轻了输入二分法的局限性[39]，并可以扩展到更大的网络。

图2说明了Neurify的高级工作流程。 Neurify接受一定范围的输入，然后使用线性求解器确定由符号线性松弛产生的输出估计是否满足安全性要求。如果求解器发现松弛约束不满足，则证明该属性是安全的。否则，求解器将返回潜在的反例。请注意，由于松弛过程引入的不准确性，求解器发现的返回反例可能是误报。因此，Neurify将检查反例是否为假阳性。如果是这样，Neurify将使用由符号线性松弛引导的定向约束细化来获得更严格的输出界限，并使用求解器重新检查属性。

3.1 符号线性松弛

每个ReLU z = Relu（z’）的输出的符号线性弛豫均利用z’，Eq low和Eq up（Eqlow≤Eq∗（x）≤Equp）的界限。 这里的Eq ∗表示z’的闭合形式。具体地，等式1显示了符号线性松弛，其中→表示“相对于”。 另外，[llow，ulow]和[lup，uup]分别表示Eqlow和Equp的具体下限和上限。 在补充材料的第1.2节中，我们提供了详细的证据，表明这种松弛是最紧密的，因为它与Eq ∗的最大距离最小。 在下面的讨论中，我们将Eqlow和Equp简化为Eq，并将相应的上下限简化为[l，u]。 图3显示了我们的符号松弛过程和Wang等人使用的天真具体化之间的区别。 [39]。更详细的讨论可以在补充材料第2节中找到。

后面全是公式，暂略