近日，一年一度的國際神經網絡驗證大賽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