太卷了！

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

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

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

來源：網(wǎng)友微博截圖

擊敗 46% 參賽者的 AlphaCode

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

挑戰(zhàn)奧數(shù)題的神經(jīng)定理證明器

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

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

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

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

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

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

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

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

這些策略以數(shù)學術語作為參數(shù)，每次策略調(diào)用都會將當前要證明的命題轉(zhuǎn)換為更容易證明的命題，直到?jīng)]有任何東西需要證明。

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

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

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

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

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

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

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

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

小結

兩家機構最新的研究成果已經(jīng)介紹完畢，網(wǎng)上已經(jīng)零零散散地出現(xiàn)了關于效果的評價：

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

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

國內(nèi)的 AI 從業(yè)者們可以趁假期研究下這兩項研究，發(fā)表自己的看法。