華人學生團隊獲國際神經(jīng)網(wǎng)絡(luò)驗證大賽佳績：總分第一，五大單項第一

由來自卡內(nèi)基梅隆大學、美國東北大學、哥倫比亞大學、加州大學洛杉磯分校的成員共同開發(fā)的工具α,β-CROWN 獲得了第二屆國際神經(jīng)網(wǎng)絡(luò)驗證大賽總分第一，以及 5 個單項第一！其中該團隊的學生作者均為華人。

近日，一年一度的國際神經(jīng)網(wǎng)絡(luò)驗證大賽VNN-COMP落下帷幕。由來自卡內(nèi)基梅隆大學(CMU)、美國東北大學、哥倫比亞大學、加州大學洛杉磯分校(UCLA)的成員共同研發(fā)的工具α,β-CROWN獲得了第二屆國際神經(jīng)網(wǎng)絡(luò)驗證大賽總分第一，比分大幅度領(lǐng)先。該工具由華人學者張歡(CMU)、許凱第（東北大學）和王世褀（哥倫比亞大學）帶領(lǐng)的團隊開發(fā)。本文中，我們將介紹神經(jīng)網(wǎng)絡(luò)驗證的基本問題、國際神經(jīng)網(wǎng)絡(luò)驗證大賽的背景和本次競賽獲勝算法 α,β-CROWN。

神經(jīng)網(wǎng)絡(luò)已經(jīng)成為了現(xiàn)代人工智能中非常重要的元素。然而由于其復雜性，神經(jīng)網(wǎng)絡(luò)常常被視為「黑盒」，因為我們很難精確的刻畫神經(jīng)網(wǎng)絡(luò)所表達的函數(shù)。例如，對抗樣本 (adversarial examples) 是神經(jīng)網(wǎng)絡(luò)中的一個常見的問題：當在神經(jīng)網(wǎng)絡(luò)的輸入中加入少量對抗擾動時，神經(jīng)網(wǎng)絡(luò)的輸出可能產(chǎn)生錯誤的改變，比如將物體識為和輸入毫不相關(guān)的類。這對于把神經(jīng)網(wǎng)絡(luò)應(yīng)用到對安全性、魯棒性要求較高的應(yīng)用中提出了很大的挑戰(zhàn)。

神經(jīng)網(wǎng)絡(luò)驗證的主要任務(wù)是為神經(jīng)網(wǎng)絡(luò)的行為提供嚴格的理論保證，用嚴格的數(shù)學方法保證魯棒性、正確性、公平性、安全性等。比如，在魯棒性驗證問題中，我們需要證明對于一個給定的網(wǎng)絡(luò)，在某張圖片上無論采用何種對抗攻擊方法，只要對抗擾動的大小不超過某個閥值，任何攻擊都一定不會成功。

舉例來說，給定一個二分類網(wǎng)絡(luò) f，若假設(shè)輸入x_0為正樣本（即 f(x_0)>0），我們需要在 x_0 附近的某個區(qū)域中，證明 f(x) 均為正數(shù)。例如在下圖中，驗證算法可以證明 x_0 附近的綠色區(qū)域中 f(x)>0。越強的神經(jīng)網(wǎng)絡(luò)驗證算法，能證明安全的綠色區(qū)域就越大，最大可以達到神經(jīng)網(wǎng)絡(luò)的決策邊界（藍色虛線框）。

然而，神經(jīng)網(wǎng)絡(luò)驗證問題通常非常困難，因為它可以等效于一個在高維神經(jīng)網(wǎng)絡(luò)上的非凸優(yōu)化問題，所以直接采用隨機采樣或者梯度下降法都無法有效解決這個問題。隨著神經(jīng)網(wǎng)絡(luò)驗證問題受到越來越多的重視，在這個新興的領(lǐng)域中的已經(jīng)涌現(xiàn)出了一些十分有競爭力的算法。為了能夠更好地評價不同算法的優(yōu)劣，研究人員需要一套標準化的測評環(huán)境和benchmark。由此，神經(jīng)網(wǎng)絡(luò)驗證大賽應(yīng)運而生。

國際神經(jīng)網(wǎng)絡(luò)驗證大賽 (International Verification of Neural Networks Competition，縮寫 VNN-COMP) 由 Taylor Johnson 教授（Vanderbilt）和 Changliu Liu 教授（CMU）于 2020 年創(chuàng)立，背靠計算機輔助驗證領(lǐng)域國際頂會 International Conference on Computer Aided Verification (CAV)，旨在為神經(jīng)網(wǎng)絡(luò)的驗證算法提供標準化的評測環(huán)境，并增強研究者之間的互相交流，創(chuàng)造一個完善的生態(tài)環(huán)境。

本次比賽征集了 9 個 benchmark（包含一個不計分的 benchmark），其內(nèi)容涉及不同領(lǐng)域的神經(jīng)網(wǎng)絡(luò)（圖像分類、控制和數(shù)據(jù)庫），并包含不同類型的網(wǎng)絡(luò)結(jié)構(gòu)（前饋神經(jīng)網(wǎng)絡(luò)、卷積神經(jīng)網(wǎng)絡(luò)和殘差網(wǎng)絡(luò)）和激活函數(shù)（ReLU, Sigmoid, Maxpool）以及不同規(guī)模的網(wǎng)絡(luò)大小。這對參賽工具的通用性、兼容性帶來了很大挑戰(zhàn)。

每個 benchmark 中都有數(shù)十個或者數(shù)百個待驗證的神經(jīng)網(wǎng)絡(luò)屬性（例如，在魯棒性驗證任務(wù)中，每個輸入數(shù)據(jù)點上的魯棒性被視為一個屬性）。每個屬性都有一個指定的超時時間（例如 3 分鐘），每個工具需要在超時時間內(nèi)之內(nèi)返回驗證結(jié)果，否則算作超時不計分。工具的運行效率在比賽中至關(guān)重要：好的驗證算法會在較短的時間內(nèi)，驗證盡可能多的神經(jīng)網(wǎng)絡(luò)屬性。

每支隊伍提交的工具由比賽主辦方在 Amazon AWS 的機器上統(tǒng)一測評以保證比賽的公平性。每個驗證成功的屬性記 10 分，此外驗證某個屬性所需時間最少和第二少的工具將獲得額外 2 分和 1 分。同時，每個 benchmark 的成績會按照在此 benchmark 中得分最高的工具，歸一化到 100 分（總分最高為 800 分）。

本次比賽共有來自全球多所大學的 12 支隊伍參加比賽。其中包含斯坦福大學、卡內(nèi)基梅隆大學、哥倫比亞大學、牛津大學、帝國理工等多所國際知名學校的隊伍在 8 個 benchmark 上展開激烈角逐。最終，由來自卡內(nèi)基梅隆大學 (CMU)、東北大學、哥倫比亞大學、加州大學洛杉磯分校(UCLA) 的成員共同開發(fā)的工具α,β-CROWN 以 779.2 分獲得總分第一名，并獲得 5 個 benchmark 的單項第一名；來自帝國理工團隊開發(fā)的 VeriNet 獲得 701.23 的總分排名第二；來自牛津大學的 OVAL、ETH 蘇黎世理工和 UIUC 的 ERAN 成績非常接近獲得并列第三名。

獲勝工具α,β-CROWN 如何取勝？

本次比賽獲勝的工具α,β-CROWN（開源代碼：http://PaperCode.cc/a-b-CROWN）由來自卡內(nèi)基梅隆大學的博士后研究員 Huan Zhang (張歡) 帶領(lǐng)的團隊開發(fā)，學生作者均為華人。開發(fā)者包括 Huan Zhang (CMU)、Kaidi Xu (共同一作，東北大學)、Shiqi Wang (共同一作，哥倫比亞大學)、Zhouxing Shi (UCLA)、Yihan Wang (UCLA)以及來自卡內(nèi)基梅隆大學的 Zico Kolter 教授、UCLA 的 Cho-Jui Hsieh 教授、哥倫比亞大學的 Suman Jana 教授和來自東北大學的 Xue Lin 教授。

α,β-CROWN（也寫作 alpha-beta-CROWN）驗證器主要有兩大特色：

1. 使用非常高效的限界傳播 (Bound Propagation) 算法來計算神經(jīng)網(wǎng)絡(luò)在給定輸入擾動空間內(nèi)的下界，然后使用分支定界法 (branch and bound) 實現(xiàn)完備神經(jīng)網(wǎng)絡(luò)驗證 (complete verification)。

2. 整個驗證算法由 PyTorch 實現(xiàn)并可在 GPU 上高效執(zhí)行，可以不依賴于線性規(guī)劃 (LP)、混合整數(shù)規(guī)劃(MIP) 等較慢且一般只能在 CPU 上運行的驗證算法。α,β-CROWN 是當前少數(shù)幾個能完全在 GPU 上運行的神經(jīng)網(wǎng)絡(luò)驗證工具之一。

α,β-CROWN 中主要采用了以下幾種神經(jīng)網(wǎng)絡(luò)驗證算法：

1.CROWN [3] 是一個基于線性松弛 (linear relaxation) 和限界傳播 (Bound Propagation) 的非完備 (incomplete) 神經(jīng)網(wǎng)絡(luò)驗證算法；

2.LiRPA [4] 將 CROWN 擴展到任意的神經(jīng)網(wǎng)絡(luò)結(jié)構(gòu)上，例如 ResNet, LSTM 和 Transformer，并在 GPU 上高效實現(xiàn)；

3.α-CROWN [5] 采用梯度上升技術(shù)來優(yōu)化 CROWN 中的線性松弛參數(shù)α，讓限界傳播過程中產(chǎn)生邊界更緊，顯著提升了驗證效果；

4.β-CROWN [6] 將α-CROWN 和分支定界法 (branch and bound) 相結(jié)合，通過在限界傳播過程中加入與分支約束條件對應(yīng)的參數(shù)β，將非完備驗證算法 CROWN 變成完備 (complete) 驗證算法，進一步提升驗證效果。

回望最近五年，神經(jīng)網(wǎng)絡(luò)驗證取得了突飛猛進的發(fā)展。早期的完備驗證 (complete verification) 方法在一個 4 層 CNN 網(wǎng)絡(luò)中需要大概一小時才能完成一張 CIFAR 圖片的驗證。而β-CROWN [6]通過基于 GPU 加速的限界傳播和分支定界法已經(jīng)將這個驗證時間壓縮到了 10 秒左右。對神經(jīng)網(wǎng)絡(luò)驗證領(lǐng)域感興趣的讀者可以閱讀入門綜述文獻 [7,8]。

團隊介紹

從 CROWN [3] (2018 年) 到 LiRPA [4]（2020 年）到α-CROWN [5] （2020 年） 再到β-CROWN [6]（2021 年），該團隊一直走在神經(jīng)網(wǎng)絡(luò)驗證的前沿，并在此次重量級大賽中展現(xiàn)出了超一流的實力，拔得頭籌。該團隊的主要貢獻成員張歡、許凱第、王世褀均在神經(jīng)網(wǎng)絡(luò)安全性和魯棒性領(lǐng)域中均有突出建樹。

張歡博士于 2020 年畢業(yè)于 UCLA，現(xiàn)任卡內(nèi)基梅隆大學 (CMU) 博士后研究員。張歡是機器學習魯棒性和安全性領(lǐng)域的早期研究者之一，對于神經(jīng)網(wǎng)絡(luò)、決策樹等機器學習模型提出了開創(chuàng)性的驗證算法，并將這些算法應(yīng)用于構(gòu)建更加安全和魯棒的圖像分類、自然語言處理 (NLP)、強化學習(RL) 等任務(wù)中，在 NeurIPS、ICML、ICLR 等一流會議中發(fā)表論文數(shù)十篇。

許凱第博士畢業(yè)于美國東北大學，于 2021 年 9 月加入德雷塞爾大學計算機學院擔任助理教授。其博士期間在 NeurIPS、ICML、ICLR、ICCV 等各大頂會發(fā)表十余篇一作 / 共同一作文章，對人工智能中的安全問題有著廣泛的研究，其中由他領(lǐng)導的 Adversarial T-shirt (ECCV 2020 Spotlight paper)曾被多家媒體報道。

王世褀就讀于哥倫比亞大學，即將在 2022 年獲得博士學位，是神經(jīng)網(wǎng)絡(luò)魯棒性、可驗證性和模型在安全領(lǐng)域應(yīng)用的早期研究者之一。博士期間在 ICLR、NeurIPS、Usenix Security、CCS 等機器學習和安全頂會發(fā)表文章十余篇。

神經(jīng)網(wǎng)絡(luò)驗證是一個年輕而重要的領(lǐng)域，其中仍然有很多有挑戰(zhàn)性的問題亟待解決，比如對包含更復雜的非線性函數(shù)的網(wǎng)絡(luò)（如 Transformer）的完備驗證，以及將驗證技術(shù)擴展到更多的領(lǐng)域中（例如網(wǎng)絡(luò)的公平性和正確性驗證）。此外，由于問題的難度（NP-Complete），目前還很難嚴格驗證 ImageNet 規(guī)模網(wǎng)絡(luò)的屬性。我們希望未來能有更多的研究人員加入這個領(lǐng)域，創(chuàng)建出更高效、更強大的驗證算法，為人工智能在各行各業(yè)的應(yīng)用場景中提供嚴謹?shù)聂敯粜浴踩院驼_性保證。

參考文獻：

[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