世界本來已經(jīng)很卷，有了 AI 加入之后，卷上加卷……
在國內(nèi)歡度春節(jié)之時(shí)，DeepMind 與 OpenAI 兩個(gè)知名 AI 研究機(jī)構(gòu)分別發(fā)布重要研究成果：DeepMind 發(fā)布了基于 Transformer 模型的 AlphaCode，可以編寫與人類相媲美的計(jì)算機(jī)程序；同時(shí)，OpenAI 開發(fā)的神經(jīng)定理證明器成功解出了兩道國際奧數(shù)題。
雖然兩家研究機(jī)構(gòu)的新成果為 AI 解決老問題提供了新思路，但也不得不讓網(wǎng)友感嘆，AI 領(lǐng)域太卷了！
在最近的一篇論文中，DeepMind 的研究者介紹了 AlphaCode。AlphaCode 使用基于 Transformer 的語言模型實(shí)現(xiàn)大規(guī)模的代碼生成，并且將其編寫為程序。
論文連接：https://storage./deepmind-media/AlphaCode/competition_level_code_generation_with_alphacode.pdf研究者將 AlphaCode 放在 Codeforces 挑戰(zhàn)中進(jìn)行了測試，Codeforces 是一個(gè)具有競爭力的編程平臺(tái)，它類似于國際象棋中使用的 Elo 評(píng)級(jí)系統(tǒng)，每周分享編程挑戰(zhàn)和問題排名。不同于編程人員在打造商業(yè)應(yīng)用程序時(shí)可能面臨的任務(wù)，Codeforces 的挑戰(zhàn)更加獨(dú)立，需要對(duì)計(jì)算機(jī)科學(xué)中的算法和理論概念有更廣泛的了解，一般是結(jié)合邏輯、數(shù)學(xué)和編碼專業(yè)知識(shí)的非常專業(yè)的難題。AlphaCode 針對(duì) Codeforces 網(wǎng)站上 5000 名用戶解決的 10 項(xiàng)挑戰(zhàn)進(jìn)行了測試，總體排名位于前 54.3%，也就是說它擊敗了 46% 的參賽者 。DeepMind 估計(jì)，AlphaCode 系統(tǒng)的 Codeforces Elo 為 1238，使其過去六個(gè)月內(nèi)在該網(wǎng)站上競爭的用戶中排名前 28%。
舉個(gè)例子，在測試 AlphaCode 的一項(xiàng)挑戰(zhàn)中，試題要求參賽者找到一種方法，使用一組有限的輸入將一個(gè)隨機(jī)、重復(fù)的 s 和 t 字母字符串轉(zhuǎn)換為另一個(gè)相同字母的字符串。例如，競爭對(duì)手不能只輸入新字母，而必須使用「backspace」命令刪除原始字符串中的幾個(gè)字母。對(duì)于 AlphaCode 來說，這只是中等難度的挑戰(zhàn)：
其中十個(gè)挑戰(zhàn)以與人類完全相同的格式輸入 AlphaCode。然后，AlphaCode 生成大量可能的答案，并通過運(yùn)行代碼和檢查輸出來篩選這些答案，就像人類競爭對(duì)手一樣。AlphaCode 論文的聯(lián)合負(fù)責(zé)人 Yujia Li 和 David Choi 表示：「整個(gè)過程是自動(dòng)的，無需人工選擇最佳樣本。」要想在 Codeforces 的挑戰(zhàn)中脫穎而出，原本不是一件容易的事。AlphaCode 項(xiàng)目開展于兩年多前，隨著大規(guī)模 Transformer 模型的進(jìn)步與大規(guī)模采樣、濾波技術(shù)的結(jié)合，DeepMind 的研究者已經(jīng)在 AI 能夠解決的問題數(shù)量上取得了重大進(jìn)展。
受到疫情的影響，項(xiàng)目的大部分工作都是在家完成的。
研究者在選定的公共 GitHub 代碼上預(yù)訓(xùn)練該模型，并在相對(duì)較小的競賽編程數(shù)據(jù)集上對(duì)其進(jìn)行微調(diào)。在評(píng)估期間，研究者為每個(gè)問題創(chuàng)建了大量的 C++ 和 Python 程序，且數(shù)量級(jí)比以前的工作要大。然后對(duì)這些解決方案進(jìn)行篩選、聚類和重新排序，將這些解決方案分配到一個(gè)由 10 個(gè)候選程序組成的小集合中，并提交給外部評(píng)估。這個(gè)自動(dòng)化系統(tǒng)取代了競爭對(duì)手的調(diào)試、編譯、通過測試和最終提交的反復(fù)試驗(yàn)過程。
總體來說，AlphaCode 的排名在競爭對(duì)手中大致相當(dāng)于中位數(shù)。雖然遠(yuǎn)遠(yuǎn)沒能贏得比賽，但這個(gè)結(jié)果代表了人工智能解決問題能力的實(shí)質(zhì)性飛躍。這一進(jìn)步證明了深度學(xué)習(xí)模型在需要批判性思維的任務(wù)中的潛力。DeepMind 指出，AlphaCode 目前的技能組合目前僅適用于競賽性質(zhì)的編程領(lǐng)域，但它的能力為創(chuàng)建未來工具打開了新的大門，這些工具使編程變得更加容易，并且有朝一日完全自動(dòng)化。許多其他公司正在開發(fā)類似的應(yīng)用程序。對(duì)于終端的用戶來說，這些系統(tǒng)就像 Gmail 的 Smart Compose 功能一樣工作，提供一些關(guān)于你正在編寫的任何內(nèi)容的建議。近年來，AI 編程系統(tǒng)的開發(fā)取得了很大進(jìn)展，但這些系統(tǒng)還遠(yuǎn)未準(zhǔn)備好接管人類程序員的工作。他們生成的代碼通常有問題，而且由于系統(tǒng)通常是在公共代碼庫上進(jìn)行訓(xùn)練的，所以有時(shí)會(huì)復(fù)制受版權(quán)保護(hù)的材料。在一項(xiàng)關(guān)于 GitHub Copilot AI 編程工具的研究中，研究人員發(fā)現(xiàn)其輸出的代碼約有 40% 包含安全漏洞。安全分析師甚至建議，不良行為者可以故意編寫代碼并與隱藏的后門（backdoor）在線共享代碼，然后這些代碼可能被用來訓(xùn)練 AI 程序，將這些錯(cuò)誤插入到未來的程序中。像這樣的挑戰(zhàn)意味著 AI 編程系統(tǒng)可能會(huì)慢慢融入程序員的工作中——換句話說，他們要進(jìn)行學(xué)徒訓(xùn)練，從助理開始做起，在被信任能夠自主執(zhí)行工作之前，AI 給出的建議都要受到懷疑。
目前，DeepMind 已在 GitHub 上發(fā)布了競賽級(jí)編程問題和解決方案的數(shù)據(jù)集，其中也包括廣泛的測試的數(shù)據(jù)，以確保通過這些測試的程序是正確的，這是目前數(shù)據(jù)集所缺乏的一個(gè)關(guān)鍵特性。DeepMind 希望這個(gè)基準(zhǔn)能夠推動(dòng)在解決問題和代碼生成方面的進(jìn)一步創(chuàng)新。GitHub 項(xiàng)目地址：https://github.com/deepmind/code_contests挑戰(zhàn)奧數(shù)題的神經(jīng)定理證明器在學(xué)科競賽領(lǐng)域，國際數(shù)學(xué)奧林匹克競賽（IMO）是非常有名的一個(gè)，我們熟悉的很多數(shù)學(xué)大神（如韋東奕）都在這一競賽中取得了驕人的成績。2021 年，這項(xiàng)比賽迎來了一個(gè)微小的變化：微軟研發(fā)多年的數(shù)學(xué) AI——Lean 也加入了競爭，和人類選手一決高下。據(jù)悉，Lean 是微軟研究院在 2013 年推出的計(jì)算機(jī)定理證明器：數(shù)學(xué)家可以把數(shù)學(xué)公式轉(zhuǎn)換成代碼，再輸入到 Lean 中，讓程序來驗(yàn)證定理是否正確。由于 Lean 劍指金牌，研究人員一直在對(duì)其進(jìn)行不停的打磨，其中也包括被微軟收購了的 OpenAI。剛剛，OpenAI 發(fā)文表示，他們已經(jīng)為 Lean 創(chuàng)建了一個(gè)神經(jīng)定理證明器，用于解決各種具有挑戰(zhàn)性的高中奧林匹克問題，包括兩個(gè)改編自 IMO 的問題和來自 AMC12、AIME 競賽的若干問題。該證明器使用一個(gè)語言模型來尋找形式化命題（formal statement）的證明。每次發(fā)現(xiàn)一個(gè)新的證明，研究者就把它作為新的訓(xùn)練數(shù)據(jù)，這改善了神經(jīng)網(wǎng)絡(luò)，使它能夠在迭代中找到越來越難的命題的解決方案。該證明器在 miniF2F 基準(zhǔn)測試中實(shí)現(xiàn)了 SOTA（41.2% vs 29.3%）水平，miniF2F 包含一組具有挑戰(zhàn)性的高中奧林匹克問題。研究者將他們的方法稱為 statement curriculum learning，該方法包括手動(dòng)收集的一組不同難度級(jí)別的命題（無需證明），其中最難的命題類似于目標(biāo)基準(zhǔn)。最初，他們的神經(jīng)證明器很弱，只能證明其中的幾個(gè)。因此，他們迭代地搜索新的證明，并在新發(fā)現(xiàn)的證明上重新訓(xùn)練他們的神經(jīng)網(wǎng)絡(luò)。經(jīng)過 8 次迭代，他們的證明器在 miniF2F 上取得了出色的成績。形式化數(shù)學(xué)（formal mathematics）是一個(gè)令人興奮的研究領(lǐng)域，因?yàn)椋?）它很豐富，可以讓你證明需要推理、創(chuàng)造力和洞察力的任意定理；2）它與游戲相似，也有一種自動(dòng)化的方法來確定一個(gè)證明是否成立（即由形式系統(tǒng)驗(yàn)證）。如下圖中的例子所示，證明一個(gè)形式化的命題需要生成一系列的證明步驟，每個(gè)證明步驟都包含對(duì)策略（ tactic）的調(diào)用。形式化系統(tǒng)接受的 artifact 是低級(jí)的（就像匯編代碼），人類很難產(chǎn)生。策略是從更高層次的指令生成這種 artifact 的搜索過程，以輔助形式化。這些策略以數(shù)學(xué)術(shù)語作為參數(shù)，每次策略調(diào)用都會(huì)將當(dāng)前要證明的命題轉(zhuǎn)換為更容易證明的命題，直到?jīng)]有任何東西需要證明。
研究者觀察到，生成策略參數(shù)所需的原始數(shù)學(xué)術(shù)語的能力出現(xiàn)在了他們的訓(xùn)練過程中，這是離開神經(jīng)語言模型所無法完成的。下面的證明就是它的一個(gè)例子：證明步驟「use n + 1」（完全由模型生成）提出使用「n + 1」作為解決方案，剩下的形式證明依賴于「ring _ exp」策略來驗(yàn)證它確實(shí)有效。
研究者還觀察到，他們的模型和搜索過程能夠產(chǎn)生鏈接多個(gè)重要推理步驟的證明。在下面的證明中，模型首先使用了引出存在性命題（existential statement） (? (x : ?), f x ≠ a * x + b) 的換質(zhì)換位律（contraposition）。然后，它使用 use (0 : ?) 為它生成一個(gè) witness，并通過利用 norm _ num 策略來完成證明。
該模型經(jīng)過 statement curriculum learning 的訓(xùn)練，能夠解決培訓(xùn)教材以及 AMC12 和 AIME 中的各種問題，以及改編自 IMO 的兩個(gè)問題。下面是三個(gè)有關(guān)的例子。
形式數(shù)學(xué)涉及兩個(gè)主要的挑戰(zhàn)，使得單純的強(qiáng)化學(xué)習(xí)應(yīng)用不太可能成功：1. 無限的動(dòng)作空間：形式數(shù)學(xué)不僅有超大的搜索空間（比如像圍棋），還有無限的動(dòng)作空間。在搜索證明的每個(gè)步驟，模型的選擇范圍不是一組行為良好的有限動(dòng)作，而是一組復(fù)雜且無限的策略，涉及必須生成的外生數(shù)學(xué)術(shù)語（例如，生成用作 witness 的數(shù)學(xué)命題)。2. 缺乏自博弈（self-play）：與兩人游戲相反，證明器不是與對(duì)手對(duì)抗，而是與一系列需要證明的命題對(duì)抗。當(dāng)面對(duì)一個(gè)過于困難的命題時(shí)，沒有明顯的重構(gòu)可以讓證明器首先生成更容易處理的中間語句。這種不對(duì)稱性阻止了在雙人游戲中獲得成功的自博弈算法的簡單應(yīng)用。在這項(xiàng)工作中，研究者通過從一個(gè)語言模型中采樣動(dòng)作來解決無限動(dòng)作空間問題。語言模型能夠生成策略調(diào)用以及通常需要作為參數(shù)的原始數(shù)學(xué)術(shù)語。對(duì)于自博弈的缺乏，他們觀察到，自博弈在兩人游戲中的關(guān)鍵作用是提供一個(gè)無監(jiān)督的課程（curriculum）。因此，他們建議用一套不同難度的輔助問題命題（不需要證明）來代替這種無監(jiān)督的課程。他們的實(shí)驗(yàn)結(jié)果表明，當(dāng)這些輔助問題的難度變化足夠大時(shí)，他們的訓(xùn)練程序就能夠解決一系列越來越難的問題，最終推廣到他們所關(guān)心的問題集。雖然這些結(jié)果非常令人興奮，因?yàn)樗鼈冏C明了深度學(xué)習(xí)模型在與形式系統(tǒng)交互時(shí)能夠進(jìn)行重要的數(shù)學(xué)推理，但在競賽中，該證明器離最佳學(xué)生表現(xiàn)還差得很遠(yuǎn)。研究者表示，他們希望自己的工作將推動(dòng)這一領(lǐng)域的研究，特別是針對(duì) IMO 的研究，并希望他們提出的 statement curriculum learning 方法能夠加快自動(dòng)推理的研究進(jìn)展。兩家機(jī)構(gòu)最新的研究成果已經(jīng)介紹完畢，網(wǎng)上已經(jīng)零零散散地出現(xiàn)了關(guān)于效果的評(píng)價(jià)：
如有 AI 研究科學(xué)家發(fā)系列長推表示，AlphaCode 達(dá)到人類水平還需要幾年時(shí)間，它在 codeforce 上的排名是有限制的，如許多參與者是高中生或大學(xué)生；還有就是 AlphaCode 生成的絕大多數(shù)程序都是錯(cuò)誤的，正是使用示例測試進(jìn)行過濾才使得 AlphaCode 實(shí)際解決了某些問題。也有研究人員表示，這像是 AlphaStar 大力出奇跡的結(jié)果。
國內(nèi)的 AI 從業(yè)者們可以趁假期研究下這兩項(xiàng)研究，發(fā)表自己的看法。參考鏈接：https:///blog/formal-math/?continueFlag=6cc759bbfb87d518f6d6948bcf276707https:///blog/article/Competitive-programming-with-AlphaCode?continueFlag=b34ed7683541bab09a68d7ab1d608057
|
