近日，一年一度的国际神经网络验证大赛VNN-COMP落下帷幕。由来自卡内基梅隆大学(CMU)、美国东北大学、哥伦比亚大学、加州大学洛杉矶分校(UCLA)的成员共同研发的工具α,β-CROWN获得了第二届国际神经网络验证大赛总分第一，比分大幅度领先。该工具由华人学者张欢(CMU)、许凯第（东北大学）和王世褀（哥伦比亚大学）带领的团队开发。本文中，我们将介绍神经网络验证的基本问题、国际神经网络验证大赛的背景和本次竞赛获胜算法 α,β-CROWN。
神经网络已经成为了现代人工智能中非常重要的元素。然而由于其复杂性，神经网络常常被视为「黑盒」，因为我们很难精确的刻画神经网络所表达的函数。例如，对抗样本 (adversarial examples) 是神经网络中的一个常见的问题：当在神经网络的输入中加入少量对抗扰动时，神经网络的输出可能产生错误的改变，比如将物体识为和输入毫不相关的类。这对于把神经网络应用到对安全性、鲁棒性要求较高的应用中提出了很大的挑战。
神经网络验证的主要任务是为神经网络的行为提供严格的理论保证，用严格的数学方法保证鲁棒性、正确性、公平性、安全性等。比如，在鲁棒性验证问题中，我们需要证明对于一个给定的网络，在某张图片上无论采用何种对抗攻击方法，只要对抗扰动的大小不超过某个阀值，任何攻击都一定不会成功。
举例来说，给定一个二分类网络 f，若假设输入x_0为正样本（即 f(x_0)>0），我们需要在 x_0 附近的某个区域中，证明 f(x) 均为正数。例如在下图中，验证算法可以证明 x_0 附近的绿色区域中 f(x)>0。越强的神经网络验证算法，能证明安全的绿色区域就越大，最大可以达到神经网络的决策边界（蓝色虚线框）。
然而，神经网络验证问题通常非常困难，因为它可以等效于一个在高维神经网络上的非凸优化问题，所以直接采用随机采样或者梯度下降法都无法有效解决这个问题。随着神经网络验证问题受到越来越多的重视，在这个新兴的领域中的已经涌现出了一些十分有竞争力的算法。为了能够更好地评价不同算法的优劣，研究人员需要一套标准化的测评环境和benchmark。由此，神经网络验证大赛应运而生。
国际神经网络验证大赛 (International Verification of Neural Networks Competition，缩写 VNN-COMP) 由 Taylor Johnson 教授（Vanderbilt）和 Changliu Liu 教授（CMU）于 2020 年创立，背靠计算机辅助验证领域国际顶会 International Conference on Computer Aided Verification (CAV)，旨在为神经网络的验证算法提供标准化的评测环境，并增强研究者之间的互相交流，创造一个完善的生态环境。
本次比赛征集了 9 个 benchmark（包含一个不计分的 benchmark），其内容涉及不同领域的神经网络（图像分类、控制和数据库），并包含不同类型的网络结构（前馈神经网络、卷积神经网络和残差网络）和激活函数（ReLU, Sigmoid, Maxpool）以及不同规模的网络大小。这对参赛工具的通用性、兼容性带来了很大挑战。
每个 benchmark 中都有数十个或者数百个待验证的神经网络属性（例如，在鲁棒性验证任务中，每个输入数据点上的鲁棒性被视为一个属性）。每个属性都有一个指定的超时时间（例如 3 分钟），每个工具需要在超时时间内之内返回验证结果，否则算作超时不计分。工具的运行效率在比赛中至关重要：好的验证算法会在较短的时间内，验证尽可能多的神经网络属性。
每支队伍提交的工具由比赛主办方在 Amazon AWS 的机器上统一测评以保证比赛的公平性。每个验证成功的属性记 10 分，此外验证某个属性所需时间最少和第二少的工具将获得额外 2 分和 1 分。同时，每个 benchmark 的成绩会按照在此 benchmark 中得分最高的工具，归一化到 100 分（总分最高为 800 分）。
本次比赛共有来自全球多所大学的 12 支队伍参加比赛。其中包含斯坦福大学、卡内基梅隆大学、哥伦比亚大学、牛津大学、帝国理工等多所国际知名学校的队伍在 8 个 benchmark 上展开激烈角逐。最终，由来自卡内基梅隆大学 (CMU)、东北大学、哥伦比亚大学、加州大学洛杉矶分校(UCLA) 的成员共同开发的工具α,β-CROWN 以 779.2 分获得总分第一名，并获得 5 个 benchmark 的单项第一名；来自帝国理工团队开发的 VeriNet 获得 701.23 的总分排名第二；来自牛津大学的 OVAL、ETH 苏黎世理工和 UIUC 的 ERAN 成绩非常接近获得并列第三名。
获胜工具α,β-CROWN 如何取胜？
本次比赛获胜的工具α,β-CROWN（开源代码：http://PaperCode.cc/a-b-CROWN）由来自卡内基梅隆大学的博士后研究员 Huan Zhang (张欢) 带领的团队开发，学生作者均为华人。开发者包括 Huan Zhang (CMU)、Kaidi Xu (共同一作，东北大学)、Shiqi Wang (共同一作，哥伦比亚大学)、Zhouxing Shi (UCLA)、Yihan Wang (UCLA)以及来自卡内基梅隆大学的 Zico Kolter 教授、UCLA 的 Cho-Jui Hsieh 教授、哥伦比亚大学的 Suman Jana 教授和来自东北大学的 Xue Lin 教授。
α,β-CROWN（也写作 alpha-beta-CROWN）验证器主要有两大特色：
1. 使用非常高效的限界传播 (Bound Propagation) 算法来计算神经网络在给定输入扰动空间内的下界，然后使用分支定界法 (branch and bound) 实现完备神经网络验证 (complete verification)。
2. 整个验证算法由 PyTorch 实现并可在 GPU 上高效执行，可以不依赖于线性规划 (LP)、混合整数规划(MIP) 等较慢且一般只能在 CPU 上运行的验证算法。α,β-CROWN 是当前少数几个能完全在 GPU 上运行的神经网络验证工具之一。
α,β-CROWN 中主要采用了以下几种神经网络验证算法：
1.CROWN [3] 是一个基于线性松弛 (linear relaxation) 和限界传播 (Bound Propagation) 的非完备 (incomplete) 神经网络验证算法；
2.LiRPA [4] 将 CROWN 扩展到任意的神经网络结构上，例如 ResNet, LSTM 和 Transformer，并在 GPU 上高效实现；
3.α-CROWN [5] 采用梯度上升技术来优化 CROWN 中的线性松弛参数α，让限界传播过程中产生边界更紧，显著提升了验证效果；
4.β-CROWN [6] 将α-CROWN 和分支定界法 (branch and bound) 相结合，通过在限界传播过程中加入与分支约束条件对应的参数β，将非完备验证算法 CROWN 变成完备 (complete) 验证算法，进一步提升验证效果。
回望最近五年，神经网络验证取得了突飞猛进的发展。早期的完备验证 (complete verification) 方法在一个 4 层 CNN 网络中需要大概一小时才能完成一张 CIFAR 图片的验证。而β-CROWN [6]通过基于 GPU 加速的限界传播和分支定界法已经将这个验证时间压缩到了 10 秒左右。对神经网络验证领域感兴趣的读者可以阅读入门综述文献 [7,8]。
团队介绍
从 CROWN [3] (2018 年) 到 LiRPA [4]（2020 年）到α-CROWN [5] （2020 年） 再到β-CROWN [6]（2021 年），该团队一直走在神经网络验证的前沿，并在此次重量级大赛中展现出了超一流的实力，拔得头筹。该团队的主要贡献成员张欢、许凯第、王世褀均在神经网络安全性和鲁棒性领域中均有突出建树。
张欢博士于 2020 年毕业于 UCLA，现任卡内基梅隆大学 (CMU) 博士后研究员。张欢是机器学习鲁棒性和安全性领域的早期研究者之一，对于神经网络、决策树等机器学习模型提出了开创性的验证算法，并将这些算法应用于构建更加安全和鲁棒的图像分类、自然语言处理 (NLP)、强化学习(RL) 等任务中，在 NeurIPS、ICML、ICLR 等一流会议中发表论文数十篇。
许凯第博士毕业于美国东北大学，于 2021 年 9 月加入德雷塞尔大学计算机学院担任助理教授。其博士期间在 NeurIPS、ICML、ICLR、ICCV 等各大顶会发表十余篇一作 / 共同一作文章，对人工智能中的安全问题有着广泛的研究，其中由他领导的 Adversarial T-shirt (ECCV 2020 Spotlight paper)曾被多家媒体报道。
王世褀就读于哥伦比亚大学，即将在 2022 年获得博士学位，是神经网络鲁棒性、可验证性和模型在安全领域应用的早期研究者之一。博士期间在 ICLR、NeurIPS、Usenix Security、CCS 等机器学习和安全顶会发表文章十余篇。
神经网络验证是一个年轻而重要的领域，其中仍然有很多有挑战性的问题亟待解决，比如对包含更复杂的非线性函数的网络（如 Transformer）的完备验证，以及将验证技术扩展到更多的领域中（例如网络的公平性和正确性验证）。此外，由于问题的难度（NP-Complete），目前还很难严格验证 ImageNet 规模网络的属性。我们希望未来能有更多的研究人员加入这个领域，创建出更高效、更强大的验证算法，为人工智能在各行各业的应用场景中提供严谨的鲁棒性、安全性和正确性保证。
参考文献：[1]VNN-COMP Presentation at CAV can be found at: https://sites.google.com/view/vnn2021[2] Stanley Bak, Changliu Liu, Taylor Johnson. The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results. https://arxiv.org/abs/2109.00498[3]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[4]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[5]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[6]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[7]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[8]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
