機器之心報道
編輯：張倩、蛋醬
世界本來已經很卷，有了 AI 加入之後，卷上加卷……
太卷了！
在國内歡度春節之時，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 從業者們可以趁假期研究下這兩項研究，發表自己的看法。
參考連結：https://openai.com/blog/formal-math/?continueFlag=6cc759bbfb87d518f6d6948bcf276707
https://deepmind.com/blog/article/Competitive-programming-with-AlphaCode?continueFlag=b34ed7683541bab09a68d7ab1d608057