太卷了！

在國內歡度春節之時，DeepMind 與 OpenAI 兩個知名 AI 研究機構分別發布重要研究成果：DeepMind 發布了基于 Transformer 模型的 AlphaCode，可以編寫與人類相媲美的計算機程序；同時，OpenAI 開發的神經定理證明器成功解出了兩道國際奧數題。

有沒有覺得 AI 攻克的這兩個領域很熟悉？沒錯，就在 2021 年，OpenAI 發布了 AI 代碼補全工具 GitHub Copilot ，并公布了背后的技術 CodeX。同樣，在去年下半年，DeepMind 也公布了他們解決數學難題的 AI 研究成果，并登上了 Nature。

雖然兩家研究機構的新成果為 AI 解決老問題提供了新思路，但也不得不讓網友感嘆，AI 領域太卷了！

來源：網友微博截圖

擊敗 46% 參賽者的 AlphaCode

在最近的一篇論文中，DeepMind 的研究者介紹了 AlphaCode。AlphaCode 使用基于 Transformer 的語言模型實現大規模的代碼生成，并且將其編寫為程序。

論文連接：https://storage.googleapis.com/deepmind-media/AlphaCode/competition_level_code_generation_with_alphacode.pdf

研究者將 AlphaCode 放在 Codeforces 挑戰中進行了測試，Codeforces 是一個具有競爭力的編程平臺，它類似于國際象棋中使用的 Elo 評級系統，每周分享編程挑戰和問題排名。不同于編程人員在打造商業應用程序時可能面臨的任務，Codeforces 的挑戰更加獨立，需要對計算機科學中的算法和理論概念有更廣泛的了解，一般是結合邏輯、數學和編碼專業知識的非常專業的難題。

AlphaCode 針對 Codeforces 網站上 5000 名用戶解決的 10 項挑戰進行了測試，總體排名位于前 54.3%，也就是說它擊敗了 46% 的參賽者 。DeepMind 估計，AlphaCode 系統的 Codeforces Elo 為 1238，使其過去六個月內在該網站上競爭的用戶中排名前 28%。

舉個例子，在測試 AlphaCode 的一項挑戰中，試題要求參賽者找到一種方法，使用一組有限的輸入將一個隨機、重復的 s 和 t 字母字符串轉換為另一個相同字母的字符串。例如，競爭對手不能只輸入新字母，而必須使用「backspace」命令刪除原始字符串中的幾個字母。對于 AlphaCode 來說，這只是中等難度的挑戰：

其中十個挑戰以與人類完全相同的格式輸入 AlphaCode。然后，AlphaCode 生成大量可能的答案，并通過運行代碼和檢查輸出來篩選這些答案，就像人類競爭對手一樣。AlphaCode 論文的聯合負責人 Yujia Li 和 David Choi 表示：「整個過程是自動的，無需人工選擇最佳樣本。」

要想在 Codeforces 的挑戰中脫穎而出，原本不是一件容易的事。AlphaCode 項目開展于兩年多前，隨著大規模 Transformer 模型的進步與大規模采樣、濾波技術的結合，DeepMind 的研究者已經在 AI 能夠解決的問題數量上取得了重大進展。

受到疫情的影響，項目的大部分工作都是在家完成的。

研究者在選定的公共 GitHub 代碼上預訓練該模型，并在相對較小的競賽編程數據集上對其進行微調。在評估期間，研究者為每個問題創建了大量的 C++ 和 Python 程序，且數量級比以前的工作要大。然后對這些解決方案進行篩選、聚類和重新排序，將這些解決方案分配到一個由 10 個候選程序組成的小集合中，并提交給外部評估。這個自動化系統取代了競爭對手的調試、編譯、通過測試和最終提交的反復試驗過程。

總體來說，AlphaCode 的排名在競爭對手中大致相當于中位數。雖然遠遠沒能贏得比賽，但這個結果代表了人工智能解決問題能力的實質性飛躍。這一進步證明了深度學習模型在需要批判性思維的任務中的潛力。DeepMind 指出，AlphaCode 目前的技能組合目前僅適用于競賽性質的編程領域，但它的能力為創建未來工具打開了新的大門，這些工具使編程變得更加容易，并且有朝一日完全自動化。

許多其他公司正在開發類似的應用程序。對于終端的用戶來說，這些系統就像 Gmail 的 Smart Compose 功能一樣工作，提供一些關于你正在編寫的任何內容的建議。

近年來，AI 編程系統的開發取得了很大進展，但這些系統還遠未準備好接管人類程序員的工作。他們生成的代碼通常有問題，而且由于系統通常是在公共代碼庫上進行訓練的，所以有時會復制受版權保護的材料。

在一項關于 GitHub Copilot AI 編程工具的研究中，研究人員發現其輸出的代碼約有 40% 包含安全漏洞。安全分析師甚至建議，不良行為者可以故意編寫代碼并與隱藏的后門（backdoor）在線共享代碼，然后這些代碼可能被用來訓練 AI 程序，將這些錯誤插入到未來的程序中。

像這樣的挑戰意味著 AI 編程系統可能會慢慢融入程序員的工作中——換句話說，他們要進行學徒訓練，從助理開始做起，在被信任能夠自主執行工作之前，AI 給出的建議都要受到懷疑。

目前，DeepMind 已在 GitHub 上發布了競賽級編程問題和解決方案的數據集，其中也包括廣泛的測試的數據，以確保通過這些測試的程序是正確的，這是目前數據集所缺乏的一個關鍵特性。DeepMind 希望這個基準能夠推動在解決問題和代碼生成方面的進一步創新。

GitHub 項目地址：https://github.com/deepmind/code_contests

挑戰奧數題的神經定理證明器

在學科競賽領域，國際數學奧林匹克競賽（IMO）是非常有名的一個，我們熟悉的很多數學大神（如韋東奕）都在這一競賽中取得了驕人的成績。

2021 年，這項比賽迎來了一個微小的變化：微軟研發多年的數學 AI——Lean 也加入了競爭，和人類選手一決高下。據悉，Lean 是微軟研究院在 2013 年推出的計算機定理證明器：數學家可以把數學公式轉換成代碼，再輸入到 Lean 中，讓程序來驗證定理是否正確。

由于 Lean 劍指金牌，研究人員一直在對其進行不停的打磨，其中也包括被微軟收購了的 OpenAI。剛剛，OpenAI 發文表示，他們已經為 Lean 創建了一個神經定理證明器，用于解決各種具有挑戰性的高中奧林匹克問題，包括兩個改編自 IMO 的問題和來自 AMC12、AIME 競賽的若干問題。

該證明器使用一個語言模型來尋找形式化命題（formal statement）的證明。每次發現一個新的證明，研究者就把它作為新的訓練數據，這改善了神經網絡，使它能夠在迭代中找到越來越難的命題的解決方案。

該證明器在 miniF2F 基準測試中實現了 SOTA（41.2% vs 29.3%）水平，miniF2F 包含一組具有挑戰性的高中奧林匹克問題。

研究者將他們的方法稱為 statement curriculum learning，該方法包括手動收集的一組不同難度級別的命題（無需證明），其中最難的命題類似于目標基準。最初，他們的神經證明器很弱，只能證明其中的幾個。因此，他們迭代地搜索新的證明，并在新發現的證明上重新訓練他們的神經網絡。經過 8 次迭代，他們的證明器在 miniF2F 上取得了出色的成績。

形式化數學（formal mathematics）是一個令人興奮的研究領域，因為：1）它很豐富，可以讓你證明需要推理、創造力和洞察力的任意定理；2）它與游戲相似，也有一種自動化的方法來確定一個證明是否成立（即由形式系統驗證）。如下圖中的例子所示，證明一個形式化的命題需要生成一系列的證明步驟，每個證明步驟都包含對策略（ tactic）的調用。

形式化系統接受的 artifact 是低級的（就像匯編代碼），人類很難產生。策略是從更高層次的指令生成這種 artifact 的搜索過程，以輔助形式化。

這些策略以數學術語作為參數，每次策略調用都會將當前要證明的命題轉換為更容易證明的命題，直到沒有任何東西需要證明。

研究者觀察到，生成策略參數所需的原始數學術語的能力出現在了他們的訓練過程中，這是離開神經語言模型所無法完成的。下面的證明就是它的一個例子：證明步驟「use n + 1」（完全由模型生成）提出使用「n + 1」作為解決方案，剩下的形式證明依賴于「ring _ exp」策略來驗證它確實有效。

研究者還觀察到，他們的模型和搜索過程能夠產生鏈接多個重要推理步驟的證明。在下面的證明中，模型首先使用了引出存在性命題（existential statement） (? (x : ?), f x ≠ a * x + b) 的換質換位律（contraposition）。然后，它使用 use (0 : ?) 為它生成一個 witness，并通過利用 norm _ num 策略來完成證明。

該模型經過 statement curriculum learning 的訓練，能夠解決培訓教材以及 AMC12 和 AIME 中的各種問題，以及改編自 IMO 的兩個問題。下面是三個有關的例子。

形式數學涉及兩個主要的挑戰，使得單純的強化學習應用不太可能成功：

1. 無限的動作空間：形式數學不僅有超大的搜索空間（比如像圍棋），還有無限的動作空間。在搜索證明的每個步驟，模型的選擇范圍不是一組行為良好的有限動作，而是一組復雜且無限的策略，涉及必須生成的外生數學術語（例如，生成用作 witness 的數學命題)。

2. 缺乏自博弈（self-play）：與兩人游戲相反，證明器不是與對手對抗，而是與一系列需要證明的命題對抗。當面對一個過于困難的命題時，沒有明顯的重構可以讓證明器首先生成更容易處理的中間語句。這種不對稱性阻止了在雙人游戲中獲得成功的自博弈算法的簡單應用。

在這項工作中，研究者通過從一個語言模型中采樣動作來解決無限動作空間問題。語言模型能夠生成策略調用以及通常需要作為參數的原始數學術語。對于自博弈的缺乏，他們觀察到，自博弈在兩人游戲中的關鍵作用是提供一個無監督的課程（curriculum）。因此，他們建議用一套不同難度的輔助問題命題（不需要證明）來代替這種無監督的課程。他們的實驗結果表明，當這些輔助問題的難度變化足夠大時，他們的訓練程序就能夠解決一系列越來越難的問題，最終推廣到他們所關心的問題集。

雖然這些結果非常令人興奮，因為它們證明了深度學習模型在與形式系統交互時能夠進行重要的數學推理，但在競賽中，該證明器離最佳學生表現還差得很遠。研究者表示，他們希望自己的工作將推動這一領域的研究，特別是針對 IMO 的研究，并希望他們提出的 statement curriculum learning 方法能夠加快自動推理的研究進展。

小結

兩家機構最新的研究成果已經介紹完畢，網上已經零零散散地出現了關于效果的評價：

如有 AI 研究科學家發系列長推表示，AlphaCode 達到人類水平還需要幾年時間，它在 codeforce 上的排名是有限制的，如許多參與者是高中生或大學生；還有就是 AlphaCode 生成的絕大多數程序都是錯誤的，正是使用示例測試進行過濾才使得 AlphaCode 實際解決了某些問題。

也有研究人員表示，這像是 AlphaStar 大力出奇跡的結果。

國內的 AI 從業者們可以趁假期研究下這兩項研究，發表自己的看法。