2021/09/16 14:29

干货｜什么是神经网络验证？一文读懂神经网络验证大赛获奖算法α,β-CROWN

在近期举办的国际神经网络验证大赛 VNN-COMP 中，来自卡内基梅隆大学 (CMU)、美国东北大学、哥伦比亚大学、加州大学洛杉矶分校(UCLA) 的成员共同开发的工具α,β-CROWN 获得了第二届国际神经网络验证大赛总分第一。本文将深入解读「α,β-CROWN」的细节。

神经网络常常被视为「黑盒」函数：虽然它们常常可以很好的拟合训练数据集，但我们通常很难精确的刻画神经网络所表达的函数。例如下图中，两个神经网络虽然在有限个点上测试结果都几乎一样，但是 Network 2 在 0 到 1 之间存在一小段小于 0 的输出，这可能是很意外的。在高输入维度的情况下，我们通常很难保证神经网络的行为都符合预期。例如，对抗样本 (adversarial examples) 是神经网络中的一个常见的问题：神经网络常常缺乏对输入的鲁棒性，当其输入在加入少量对抗扰动时，神经网络的输出可能产生很大改变，比如在图像分类任务中将物体识别为不相关的类，或在目标检测任务中无法检测到图片中的物体。这对于把神经网络应用到对安全性、鲁棒性要求较高的应用中提出了很大的挑战，比如安全摄像头、自动驾驶和工业设备控制。

神经网络验证的主要任务是为神经网络的行为提供严格的理论保证。比如，在鲁棒性验证问题中，我们需要验证在某张图片上无论采用何种对抗攻击方法，只要对抗扰动的大小不超过某个阀值，攻击都一定不会成功。和很多对抗样本的防御方法不同，经过严格鲁棒性验证的网络无需担心被更强的对抗攻击攻破。神经网络验证可以用在很多其他的场景中，比如验证正确性、公平性、安全性等。它可以确保神经网络在关键的应用中不会出现意外的输出导致严重的后果。

我们将在下文中介绍神经网络验证问题的基本框架，和在今年国际神经网络验证大赛 (VNN-COMP 2021) 中的获胜算法α,β-CROWN。

什么是神经网络验证问题？

神经网络验证问题通常由一个神经网络 f 、一个输入数据集合 C 和一个待验证属性 P 组成。 P 指定了神经网络在输入任意来自于 C 中的点时，输出需要满足的条件。比如，若我们使用神经网络学习一个一维的函数 f(x)，一个简单的可以验证的属性是保证当 x 在 [0,1] 的集合内时，f(x)>0。如下图所示，满足该属性，而

则不满足。

该验证问题等价于一个非凸优化问题

：如果我们可以找到在 [0,1] 范围内 f(x) 的最小值，且该最小值大于零，我们则可以验证对于任意在 [0,1] 之间的 x，f(x)>0 的属性成立。

一个常见的设定是神经网络的鲁棒性验证：给定一个二分类网络 f ，若假设输入 x_0 为正样本（即f(x_0)>0），我们需要验证在 x_0 附近的

范数球中 (

)， f(x) 均为正数，因此任何的在此范数球中的对抗扰动都无法改变二分类器的输出标签。同样地，我们可以把这个问题转换为一个优化问题

：如果我们可以找到在

范数球内 f(x) 的最小值

且该最小值

，则对抗样本不存在；否则使得 f(x)<0 的点即为对抗样本，此样本会被网络误判为负样本。

由于神经网络通常是一个非线性、非凸的函数，求解极小值一般非常困难。如果随机采样有限个点，我们可能无法发现没有采样到的区域出现了 f(x)<0 的情况，而且对于高维输入的函数（如图片）随机采样可能需要指数数量的采样点。如果使用基于梯度下降的方法来求解这个优化问题，由于问题是非凸的，也无法保证解到最优解。实际上，一般的神经网络验证问题是 NP 完全的，目前不存在多项式时间算法。

为了能够有效地解决神经网络验证问题，很多方法都会寻找

的下界

：若

>0 ，因为

是

的下界，所以

必大于 0，验证成功。若

<0，则

的符号无法确定，无法给出答案。这一类方法被称为非完备验证(incomplete verification)，因为它并不能对所有的验证问题给出答案。反之，若一种方法可以保证解出

，则被称为完备验证 (complete verification)。

神经网络的鲁棒性验证问题和大家更熟悉的对抗攻击问题之间存在紧密联系：它们都在解决同一个优化问题

。在对抗攻击问题中，我们常常采用基于梯度的方法（如 PGD）来解决这个有约束条件的优化问题。由于问题是非凸的，对抗攻击通常无法找到最优解

，但可以找到一个比

大的上界

。若

<0，则我们找到了一个违反待验证属性的反例(即对抗样本)，鲁棒性验证失败；若

，寻找对抗样本失败，但我们无法确定神经网络是否鲁棒，因为

既可以为正也可以为负。更强的对抗攻击算法能找到更小的上界

。类似地，在非完备鲁棒性验证算法中，我们寻找的是

的下界；更强的非完备验证算法能找到更大的下界

。简而言之，攻击算法从上界的方向来逼近

，而验证算法从下界的方向逼近

。

本文将简介获得 VNN-COMP 2021 第一名的验证器α,β-CROWN 中使用的三种高效的验证算法，CROWN，α-CROWN 和β-CROWN（开源代码：http://PaperCode.cc/a-b-CROWN）。

基于限界传播的高效验证算法：CROWN，α-CROWN 和β-CROWN

CROWN [1]是一个非完备 (incomplete) 神经网络验证算法，其主要原理为将网络中的非线性激活函数（如 ReLU，sigmoid，maxpool 等）替换为线性的上下界，然后进行限界传播(Bound Propagation)，拿到神经网络输出对输入的线性下界。

这里主要介绍最常见的 ReLU 激活函数的情况。我们定义网络中第 i 层第 j 个 ReLU 神经元输入为

，输出为

。假定我们知道一个 ReLU 神经元的输入范围是

（假设

和

已知）时，在

和

这两种情况时 ReLU 函数已经变为线性函数（线性上下界为其自身，如下图 Case 1&2）；否则，若

，ReLU 函数为非线性函数（如下图 Case 3 所示）；这种情况下的 ReLU 被称作是非稳定的 (unstable)。

对于非稳定的 ReLU，我们可以使用如下图所示的线性函数（蓝色虚线）作为 ReLU 的上界和下界（注意我们只需要上下界在

和

间成立即可）：

一般地，我们都可以用两个线性函数来为非线性函数找到上下界：

对于多维的非线性函数，也可以类似地使用两个线性的超平面来作为上下界。

利用 ReLU 函数的线性上下界，我们在一个简单的两层网络里展示如何进行 CROWN 算法中的反向限界传播(Bound Propagation)。我们定义一个两层网络

，W 和 v 是网络权重。因输出层维度为 1，因此 v 是一个向量。我们用

和

来分别定义第层激活函数前的数值和激活函数后的数值，如下图所示：

对于输出层，根据定义我们已知：

该等式定义了网络输出 f(x) 和

层之间的线性关系。根据网络的定义

，我们先把该等式传播到

这一层：

该等式定义了网络输出 f(x) 和

层之间的线性关系。下一步我们希望找到 f(x) 和

层的线性关系，但由于

是非线性的，我们需要利用他们之间的线性上下界，来保证 f(x) 和

层之间的线性关系不等式成立：

其中，D 是一个对角矩阵，b 是一个向量；它们代表了 ReLU 的线性下界和上界，定义如下。我们在里元素为正时取 ReLU 的线性下界，元素为负时取线性上界：

可以证明上述的 D ，b 可以使得不等式成立 (参见文献[4] 附录 A)。最终，带入定义

我们可以得到网络输出 f(x) 和输入 x 之间的线性不等式：

为简化符号我们在上式中将线性系数定义为 a 和 c 。至此限界传播算法结束，我们得到了网络输出对输入的线性下界 g(x) 。

为了拿到在

内的函数下界，我们需要解决一个优化问题：

因为 g(x) 和 x 之间关系是线性的，对于常见的

范数输入扰动

，可以直接得到闭式解：

至此我们拿到了非凸优化问题

的一个下界

，实现了非完备验证。

在上面的例子里我们假设

和

是已知的。实际计算时，我们可以将

看作是网络的输出层使用 CROWN 来递归计算出

和

。由于在复杂的神经网络上实现 CROWN 算法较难，我们推荐使用 auto_LiRPA 软件包来进行计算 [3]。

虽然 CROWN 能够在 GPU 上高效实现，但它计算出的下界相对较松，特别是和传统的基于线性规划 (LP) 的算法相比时差距较大。

α-CROWN [2]通过梯度上升来获得更紧的下界。我们观察到在推导 ReLU 函数的线性下界时，每个不稳定的 ReLU 神经元都存在一个自由参数

,对于任意

我们都能拿到一个 ReLU 的线性下界，所以最终得到的线性下界 g(x) 可以是不唯一的，取决于的

设定。因此，我们可以将

可以将看作一个函数，通过优化

来最大化下界：

因为整个的限界传播算法可以使用支持自动微分的框架比如 PyTorch 来实现，我们可以很容易拿到

的梯度来进行优化。[3] 中证明了

对应于基于线性规划 (LP) 的非完备验证算法中的对偶变量，所以优化

可以使得α-CROWN 获得和 LP 一样的下界。此外，因为

和

也是使用 CROWN 来计算的，在计算时也存在相应的

参数。优化所有的

参数可以显著让下界变紧，甚至可以超过基于 LP 的非完备验证算法 [4]。

β-CROWN 在限界传播过程中结合分支定界法，实现了完备的神经网络验证(complete verification)。在分支定界法中，我们需要将网络中的每一个不稳定 ReLU 神经元划分成两种情况考虑：

。针对每一种情况，我们需要求解带分支约束的两个子问题的下界：

和

。可以证明将问题划分为两个子问题后，得到新的下界

会比划分前更好，因为不稳定 ReLU 神经元划分后变成了线性的，无需再使用线性松弛。通过不断划分不稳定 ReLU，可以不断让

变得更紧；当所有的不稳定 ReLU 神经元都被划分过后，我们可以得到问题的精确解

，实现完备神经网络验证（实际上，通常在所有不稳定 ReLU 神经元被划分前，已经可以证明

完成验证）。

β-CROWN 使用额外的拉格朗日乘子来保证分支约束条件，比如，在上面介绍 CROWN 的例子里，假设我们有额外的分支约束

，我们可以在限界传播到这一层 ReLU 时加入一个额外的可优化参数

：

限界传播算法可以继续进行，例如在上面的例子中，我们将得到一个有额外

参数的线性下界：

通过优化额外的参数

，我们让下界变的更紧。文献 [5] 提供了更多的公式推导细节。

α,β-CROWN 验证器同时优化了

参数和

参数，以取得尽可能紧的下界。由于 CROWN、α-CROWN 和β-CROWN 算法均可在 GPU 上高效实现，并通过 PyTorch 自动微分获得梯度进行优化，α,β-CROWN 验证器有非常高的运行效率。想深入研究该验证器的读者可以在 http://PaperCode.cc/a-b-CROWN 找到开源代码。

小结

本文中我们介绍了神经网络验证的基本问题，并详细介绍了本届神经网络验证大赛 (VNN-COMP 2021) 获胜工具α,β-CROWN 中使用的基于限界传播的算法。限于篇幅，我们在上面只介绍了算法中最简单的情况，有兴趣的读者可以阅读文献 [1][2][3] 和代码对α,β-CROWN 进行更深入的了解。除了我们在本文中介绍的算法之外，我们也推荐读者阅读综述文献 [5, 6] 了解其他相关的神经网络验证算法。

和深度学习中的其他领域相比，神经网络验证还非常年轻，其中不乏很多有挑战性的问题，例如对包含更复杂的非线性函数的网络（如 Transformer）的完备验证，以及将算法拓展到更大规模的网络（如 ImageNet）中。早期的完备验证 (complete verification) 方法在一个 4 层 CNN 网络中需要大概一小时才能完成一张 CIFAR 图片的验证；而β-CROWN [6]通过基于 GPU 加速的限界传播和分支定界法已经将这个验证时间压缩到了 10 秒左右。我们希望在未来的几年中，严格验证大规模神经网络的属性不再困难。此外，我们也希望验证技术可以扩展到更多问题中（例如神经网络的公平性、正确性验证）和更多应用场景中（如强化学习、生成模型等）。

参考文献：

[1]Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. "Efficient neural network robustness certification with general activation functions." NeurIPS 2018. https://arxiv.org/pdf/1811.00866.pdf

[2]Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. "Automatic perturbation analysis for scalable certified robustness and beyond." NeurIPS 2020. https://arxiv.org/pdf/2002.12920.pdf

[3]Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. "Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers." ICLR 2020. https://arxiv.org/pdf/2011.13824.pdf

[4]Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. "Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification." https://arxiv.org/pdf/2103.06624.pdf

[5]Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett, and Mykel J. Kochenderfer. "Algorithms for verifying deep neural networks." https://arxiv.org/pdf/1903.06758.pdf

[6]Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. "A convex relaxation barrier to tight robustness verification of neural networks." NeurIPS 2019. https://arxiv.org/pdf/1902.08722.pdf

理论国际神经网络验证大赛

相关数据

深度学习技术

深度学习（deep learning）是机器学习的分支，是一种试图使用包含复杂结构或由多重非线性变换构成的多个处理层对数据进行高层抽象的算法。深度学习是机器学习中一种基于对数据进行表征学习的算法，至今已有数种深度学习框架，如卷积神经网络和深度置信网络和递归神经网络等已被应用在计算机视觉、语音识别、自然语言处理、音频识别与生物信息学等领域并获取了极好的效果。

来源：LeCun, Y., Bengio, Y., & Hinton, G. (2015). Deep learning. nature, 521(7553), 436.

范数技术

范数(norm)，是具有“长度”概念的函数。在线性代数、泛函分析及相关的数学领域，是一个函数，其为向量空间内的所有向量赋予非零的正长度或大小。半范数反而可以为非零的向量赋予零长度。

来源：CSDN Blog

激活函数技术

在计算网络中，一个节点的激活函数定义了该节点在给定的输入或输入的集合下的输出。标准的计算机芯片电路可以看作是根据输入得到"开"(1)或"关"(0)输出的数字网络激活函数。这与神经网络中的线性感知机的行为类似。一种函数（例如 ReLU 或 S 型函数），用于对上一层的所有输入求加权和，然后生成一个输出值（通常为非线性值），并将其传递给下一层。

来源：维基百科 Google ML glossary

权重技术

线性模型中特征的系数，或深度网络中的边。训练线性模型的目标是确定每个特征的理想权重。如果权重为 0，则相应的特征对模型来说没有任何贡献。

来源：Google AI Glossary

参数技术

在数学和统计学裡，参数（英语：parameter）是使用通用变量来建立函数和变量之间关系（当这种关系很难用方程来阐述时）的一个数量。

来源：维基百科

凸优化技术

凸优化，或叫做凸最优化，凸最小化，是数学最优化的一个子领域，研究定义于凸集中的凸函数最小化的问题。凸优化在某种意义上说较一般情形的数学最优化问题要简单，譬如在凸优化中局部最优值必定是全局最优值。凸函数的凸性使得凸分析中的有力工具在最优化问题中得以应用，如次导数等。凸优化应用于很多学科领域，诸如自动控制系统，信号处理，通讯和网络，电子电路设计，数据分析和建模，统计学（最优化设计），以及金融。在近来运算能力提高和最优化理论发展的背景下，一般的凸优化已经接近简单的线性规划一样直捷易行。许多最优化问题都可以转化成凸优化（凸最小化）问题，例如求凹函数f最大值的问题就等同于求凸函数 -f最小值的问题。

来源：维基百科

线性规划技术

在数学中，线性规划（Linear Programming，简称LP）特指目标函数和约束条件皆为线性的最优化问题。

来源：维基百科

神经网络技术

（人工）神经网络是一种起源于 20 世纪 50 年代的监督式机器学习模型，那时候研究者构想了「感知器（perceptron）」的想法。这一领域的研究者通常被称为「联结主义者（Connectionist）」，因为这种模型模拟了人脑的功能。神经网络模型通常是通过反向传播算法应用梯度下降训练的。目前神经网络有两大主要类型，它们都是前馈神经网络：卷积神经网络（CNN）和循环神经网络（RNN），其中 RNN 又包含长短期记忆（LSTM）、门控循环单元（GRU）等等。深度学习是一种主要应用于神经网络帮助其取得更好结果的技术。尽管神经网络主要用于监督学习，但也有一些为无监督学习设计的变体，比如自动编码器和生成对抗网络（GAN）。

来源：机器之心

神经元技术

（人工）神经元是一个类比于生物神经元的数学计算模型，是神经网络的基本组成单元。对于生物神经网络，每个神经元与其他神经元相连，当它“兴奋”时会向相连的神经元发送化学物质，从而改变这些神经元的电位；神经元的“兴奋”由其电位决定，当它的电位超过一个“阈值”（threshold）便会被激活，亦即“兴奋”。目前最常见的神经元模型是基于1943年 Warren McCulloch 和 Walter Pitts提出的“M-P 神经元模型”。在这个模型中，神经元通过带权重的连接接处理来自n个其他神经元的输入信号，其总输入值将与神经元的阈值进行比较，最后通过“激活函数”（activation function）产生神经元的输出。

来源：Overview of Artificial Neural Networks and its Applications. (2018). medium.com.

物体识别技术

计算机视觉领域的一个分支，研究物体的识别任务

对抗样本技术

对抗样本是一类被设计来混淆机器学习器的样本，它们看上去与真实样本的几乎相同（无法用肉眼分辨），但其中噪声的加入却会导致机器学习模型做出错误的分类判断。

来源：Goodfellow, I. J., Shlens, J., & Szegedy, C. (2014). Explaining and harnessing adversarial examples. arXiv preprint arXiv:1412.6572.

生成模型技术

在概率统计理论中, 生成模型是指能够随机生成观测数据的模型，尤其是在给定某些隐含参数的条件下。它给观测值和标注数据序列指定一个联合概率分布。在机器学习中，生成模型可以用来直接对数据建模（例如根据某个变量的概率密度函数进行数据采样），也可以用来建立变量间的条件概率分布。

来源：维基百科

图像分类技术

图像分类，根据各自在图像信息中所反映的不同特征，把不同类别的目标区分开来的图像处理方法。它利用计算机对图像进行定量分析，把图像或图像中的每个像元或区域划归为若干个类别中的某一种，以代替人的视觉判读。

来源：百度百科

强化学习技术

强化学习是一种试错方法，其目标是让软件智能体在特定环境中能够采取回报最大化的行为。强化学习在马尔可夫决策过程环境中主要使用的技术是动态规划（Dynamic Programming）。流行的强化学习方法包括自适应动态规划（ADP）、时间差分（TD）学习、状态-动作-回报-状态-动作（SARSA）算法、Q 学习、深度强化学习（DQN）；其应用包括下棋类游戏、机器人控制和工作调度等。

来源：机器之心

目标检测技术

一般目标检测（generic object detection）的目标是根据大量预定义的类别在自然图像中确定目标实例的位置，这是计算机视觉领域最基本和最有挑战性的问题之一。近些年兴起的深度学习技术是一种可从数据中直接学习特征表示的强大方法，并已经为一般目标检测领域带来了显著的突破性进展。

来源：机器之心