Auto Byte

专注未来出行及智能汽车科技

微信扫一扫获取更多资讯

Science AI

关注人工智能与其他前沿技术、基础学科的交叉研究与融合发展

微信扫一扫获取更多资讯

机器之心编辑部机器之心专栏

华人学生团队获国际神经网络验证大赛佳绩:总分第一,五大单项第一

由来自卡内基梅隆大学、美国东北大学、哥伦比亚大学、加州大学洛杉矶分校的成员共同开发的工具α,β-CROWN 获得了第二届国际神经网络验证大赛总分第一,以及 5 个单项第一!其中该团队的学生作者均为华人。


近日,一年一度的国际神经网络验证大赛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
理论神经网络验证国际神经网络验证大赛
相关数据
人工智能技术

在学术研究领域,人工智能通常指能够感知周围环境并采取行动以实现最优的可能结果的智能体(intelligent agent)

神经网络技术

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

暂无评论
暂无评论~