AI“雙子星”同日聯動：DeepMind加速編程自動化，OpenAI新方法解開2道國際奧數題

2022 年開年不久，全球人工智能領域兩大明星公司不約而同在今天宣布了重要進展：OpenAI 稱自己構建了一個神經定理證明器，該證明器學會了解決各種具有挑戰性的高中數學問題，包括 AMC12 和 AIME 比賽的問題，以及改編自 IMO 的兩個問題。 DeepMind 則表示，由其開發的名為 AlphaCode 的人工智能系統，該系統的“編程能力能與一般人類程序員相競爭”。DeepMind 說，該系統的結果是朝著自主編程邁出的重要一步，盡管現在為止 AlphaCode 的能力不一定能代替普通程序員完成日常編程任務。 本文將分別介紹這兩項成果。
OpenAI：AI 進軍數學

根據 OpenAI 的介紹，他們的證明器使用語言模型來尋找形式陳述的證明。每次找到一個新的證明時，OpenAI 都會將其用作新的訓練數據，用來改進神經網絡，并使其能夠通過迭代進而找到解決更難更復雜陳述的方案。

OpenAI 在 miniF2F 基準——一個具有挑戰性的高中奧林匹克問題集合，測試中取得了目前的最先進的水平（41.2% vs 29.3%）。 OpenAI 的方法稱之為陳述課程學習（statement curriculum learning），包括手動收集一組不同難度級別的陳述（沒有證據），其中最難的陳述與OpenAI的目標基準相似。最初，OpenAI 的神經證明器能力很弱，只能證明其中的幾個。 OpenAI 反復搜索新的證明，并在新發現的證明上重新訓練 OpenAI 的神經網絡，經過 8 次迭代，最終 OpenAI 的證明器在 miniF2F 上測試時表現得非常出色。 形式數學是一個令人興奮的研究領域，首先因為它具有豐富性，讓你可以證明需要推理、創造力和洞察力的任意定理；其次因為它與游戲的相似性——人工智能在游戲領域取得了驚人的成功——因為它用一種自動化的方式來確定證明是否成功（即，由形式系統驗證）。  如下面的簡單示例所示，證明形式陳述需要生成一系列證明步驟，每個證明步驟都包含對策略的調用。這些策略以數學術語作為論據，每個策略調用都會將當前要證明的陳述轉換為更容易證明的陳述，直到沒有任何東西可以證明。
圖1 問題1
通過觀察發現，在 OpenAI 的訓練過程中出現了一種能力，即生成作為戰術參數所需的原始數學術語。如果沒有神經語言模型，這是無法完成的。下面的證明就是一個例子：證明步驟提出使用 n+1 作為解決方案（這完全由 OpenAI 的模型生成），其余的正式證明依靠 ring_exp 策略來驗證它確實是有效的。
圖2 問題2
OpenAI 還觀察到，OpenAI 的模型和搜索程序能夠生成鏈接多個非平凡推理步驟的證明。在下面的證明中，模型首先使用存在性陳述的對立。然后使用為它生成一個見證，并通過利用 norm_num 策略完成證明。
圖3 問題3
OpenAI 的模型經過陳述課程學習訓練，能夠解決培訓教科書和 AMC12 和 AIME 比賽中的各種問題，以及改編自 IMO 的 2 個問題。下面 OpenAI 展示此類生成證明的三個示例。
圖4 問題4
圖5 問題5
圖6 問題6

形式數學涉及兩個主要挑戰，這使得強化學習的應用不太可能成功。
1）無限的動作空間：形式數學不僅有一個非常大的搜索空間（例如圍棋），它還有一個無限的動作空間。在證明搜索的每一步，模型不是從行為良好的有限動作集中進行選擇，而是必須從一組復雜且無限的策略中進行選擇，其中涉及必須生成的外生數學術語（例如，生成用作見證的數學語句，諸如“存在一個 xx st ...”之類的步驟中使用的對象“，或作為剪切，證明中間引理引入和鏈接）。
2）缺乏自我博弈：與二人博弈相反，證明器不是與對手比賽，而是與一組要證明的陳述進行比賽。當面對一個太難的陳述時，沒有明顯的重構可以讓證明器生成中間更容易首先解決的陳述。這種不對稱性阻止了在二人博弈中成功的自我博弈算法的應用。
在 OpenAI 的工作中，通過在搜索證明時，從語言模型中采樣動作來解決無限動作空間問題。語言模型能夠生成策略調用以及通常需要作為參數的原始數學術語。
其次，OpenAI 觀察到自我博弈在二人博弈中的關鍵作用是提供無監督的課程，以此作為解決缺乏自我博弈的基礎，OpenAI 的方法建議用一組不同難度的輔助問題陳述（不需要證明）來代替這種無監督的課程。OpenAI 的經驗表明，當這些輔助問題的難度足夠多時，OpenAI 的訓練程序能夠解決越來越難的問題的課程，最終推廣到 OpenAI 關心的問題集。
雖然這些結果非常令人興奮，它們證明了深度學習模型在與正式系統交互時能夠進行非凡的數學推理，但與這些比賽中最好的學生的表現相比，OpenAI 的方法還差得很遠。 未來，OpenAI 希望，自己的工作能夠激發該領域的研究，特別是針對 IMO 大挑戰，與此同時，OpenAI 提出的陳述式課程學習方法，或將有助于加速自動化推理的總體進展。
DeepMind：寫代碼自動化更進一步
DeepMind 創建了一個名為 AlphaCode 的人工智能系統，該系統的“編程能力能與一般人類程序員相競爭”。

開發團隊針對人類競賽中使用的編程挑戰題目測試了該人工智能系統，發現其程序達到了“預期的排名”，使其在人類程序員中排名前 54%。DeepMind 說，該系統的結果是朝著自主編程邁出的重要一步，盡管現在為止 AlphaCode 的能力不一定能代替普通程序員完成日常編程任務。 DeepMind 的首席研究科學家 OriolVinyals 通過電子郵件告訴 The Verge，研究仍處于早期階段，但結果使公司更接近于創建一個靈活的、解決問題的人工智能——一個可以自主應對目前僅屬于人類領域的編碼挑戰的程序。Vinyals 說：“從長遠來看，我們對【AlphaCode】幫助程序員和非程序員編寫代碼、提高生產力或者創建新的軟件制作方法的潛力感到興奮?！?/span> AlphaCode 根據 Codeforces 策劃的挑戰進行了測試，Codeforces 是一個競爭性的編碼平臺，每周共享問題，并為編碼人員發布類似于國際象棋中使用的 Elo 評級系統的排名。這些挑戰不同于編碼器在制作（例如商業應用程序）時可能面臨的任務類型。它們更自成一體，需要更廣泛地了解計算機科學的算法和理論概念。把它們想象成結合了邏輯、數學和編碼專業知識的非常專業的謎題。 在 AlphaCode 測試的一個示例挑戰中，要求競爭對手找到一種方法，使用有限的輸入集將一串隨機、重復的s和t字母轉換為另一串相同的字母。例如，競爭對手不能只鍵入新字母，而是必須使用刪除原始字符串中幾個字母的“退格”命令。您可以閱讀以下挑戰的完整描述：

其中 10 個挑戰以與人類完全相同的格式輸入 AlphaCode。然后，AlphaCode 生成大量可能的答案，并像人類競爭對手一樣通過運行代碼和檢查輸出來篩選這些答案?！罢麄€過程是自動的，無需人工選擇最佳樣本，”AlphaCode 論文的聯合負責人 Yujia Li 和 David Choi 通過電子郵件告訴 The Verge。 AlphaCode 針對 Codeforces 網站上 5,000 名用戶解決的 10 項挑戰進行了測試。平均而言，它的排名在前 54.3%，DeepMind 估計這使該系統的 Codeforces Elo 為 1238，這使其在過去六個月中在該網站上競爭的用戶中排名前 28%。 “我可以肯定地說 AlphaCode 的結果超出了我的預期，”Codeforces 創始人 Mike Mirzayanov 在 DeepMind 發布的一份聲明中這樣說?！拔页謶岩蓱B度，因為即使在簡單的競爭問題中，通常不僅需要實現算法，更需要（這是最困難的部分）發明它。AlphaCode 成功地達到了一個有前途的、新競爭對手的水平。”

DeepMind 指出，AlphaCode 目前的技能僅適用于競爭性編程領域，但它的能力為創建未來工具打開了新大門，這些工具使編程更易于進行，并且有朝一日完全自動化。 許多其他公司正在開發類似的應用程序。例如，微軟和 AI 實驗室 OpenAI 已將后者的語言生成程序 GPT-3 改編為輸出代碼字符串的自動完成程序。（與 GPT-3 一樣，AlphaCode 也基于稱為 transformer 的 AI 架構，它特別擅長解析自然語言和代碼這類順序文本）。對于終端用戶來說，這些系統就像 Gmail 的 Smart Compose 功能一樣工作：為完成您正在編寫的任何內容出謀劃策。 近年來，人工智能編程系統的開發取得了很大進展，但這些系統還遠未準備好接管人類程序員的工作。他們產出的代碼通常有些問題，而且由于系統通常是在公共代碼庫上進行訓練的，因此他們有時會“復制”受版權保護的材料。 在一項由代碼存儲庫 GitHub 開發的名為 Copilot 的 AI 編程工具的研究中，研究人員發現其輸出代碼的大約 40% 包含安全漏洞。安全分析師甚至建議，不良行為者可以故意編寫代碼并與隱藏的在線后門共享代碼，然后這些代碼可能被用來訓練人工智能程序，將這些錯誤插入到未來的程序中。 像這樣的挑戰意味著人工智能編程系統可能會慢慢融入程序員的工作中——從助手開始，他們的建議在能夠被信任之前都將受到懷疑。換句話說：他們要香徒弟跟師傅一樣接受專業程序員的訓練。目前為止，這些 AI 編程系統正在飛快地學習。