機器之心報道
機器之心編輯部
對於 AI 來說，奧數不再是問題了。
本周四，谷歌 DeepMind 的人工智能完成了一項壯舉：用 AI 做出了今年國際數學奧林匹克競賽 IMO 的真題，並且距拿金牌僅一步之遙。
上周剛剛結束的 IMO 競賽共有六道賽題，涉及代數、組合學、幾何和數論。谷歌提出的混合 AI 系統做對了四道，獲得 28 分，達到了銀牌水平。
本月初，UCLA 終身教授陶哲軒剛剛宣傳了百萬美元獎金的 AI 數學奧林匹克競賽（AIMO 進步獎），沒想到 7 月還沒過，AI 的做題水平就進步到了這種水平。
IMO 上同步做題，做對了最難題
IMO 是歷史最悠久、規模最大、最負盛名的青年數學家競賽，自 1959 年以來每年舉辦一次。近來，IMO 競賽也被廣泛認為是機器學習領域的一項重大挑戰，成為衡量人工智能系統高級數學推理能力的理想基準。
在今年的 IMO 競賽上，由 DeepMind 團隊研發的 AlphaProof 和 AlphaGeometry 2 共同實作了裏程碑式的突破。
其中，AlphaProof 是一種用於形式化數學推理的強化學習系統，而 AlphaGeometry 2 是 DeepMind 幾何求解系統 AlphaGeometry 的改進版本。
這一突破表明具有先進數學推理能力的通用人工智能 (AGI) 有潛力開啟科學技術新領域。
那麽，DeepMind 的 AI 系統是如何參加 IMO 競賽的？
簡單來說，首先這些數學問題被手動轉譯成形式化的數學語言，以便 AI 系統理解。在正式比賽中，人類參賽選手分兩節（兩天）送出答案，每節限時 4.5 小時。AlphaProof+AlphaGeometry 2 組合成的 AI 系統在幾分鐘內就解決了一個問題，但花了三天時間來解決其他問題。雖然如果嚴格按照規則來說的話，DeepMind 的系統超時了。有人推測，這裏面可能涉及大量的暴力破解。
谷歌表示，AlphaProof 透過確定答案並證明其正確性解決了兩道代數問題和一道數論問題。其中包括本次競賽中最難的問題，在今年的 IMO 上只有五名參賽者解決了。而 AlphaGeometry 2 證明了一道幾何問題。
AI 給出的解：https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html
IMO 金牌得主、費斯獎得主 Timothy Gowers 和兩屆 IMO 金牌得主、IMO 2024 問題選擇委員會主席 Joseph Myers 博士根據 IMO 評分規則，對該組合系統給出的解決方案進行了評分。
六個問題中的每一個問題滿分 7 分，總分最高 42 分。DeepMind 的系統最終得分為 28 分，意味著解決的 4 個問題都獲得了滿分——相當於銀牌類別的最高分。今年的金牌門檻為 29 分，正式比賽的 609 名選手中有 58 人獲得了金牌。
該圖顯示了谷歌 DeepMind 的人工智能系統在 IMO 2024 上相對於人類競爭對手的表現。在總分為 42 分的情況下，該系統獲得了 28 分，達到了與比賽銀牌獲得者相同的水平。另外，今年 29 分是能拿金牌的。
AlphaProof：一種形式化推理方法
在谷歌使用的混合 AI 系統中，AlphaProof 是一個以形式語言 Lean 來證明數學陳述的自訓練系統。它結合了預訓練語言模型與 AlphaZero 強化學習演算法。
其中，形式語言為形式化地驗證數學推理證明的正確性，提供了重要優勢。在此之前，這在機器學習中的使用一直受限，因為人工編寫數據數量非常有限。
相比之下，基於自然語言的方法盡管可以存取更多量級的數據，但會產生看似合理而不正確的中間推理步驟與解法。
谷歌 DeepMind 透過微調 Gemini 模型自動將自然語言問題陳述轉譯為形式陳述，在這兩個互補領域之間建立了一座橋梁，從而建立了一個包含不同難度形式問題的大型庫。
給到數學問題，AlphaProof 會生成候選解題方案，然後透過搜尋 Lean 中可能的證明步驟來證明它們。找到並驗證的每個證明方案，都用來強化 AlphaProof 的語言模型，增強其解決後續更具挑戰性問題的能力。
為訓練 AlphaProof，谷歌 DeepMind 在 IMO 比賽前幾周內證明或反證明了涵蓋廣泛難度與主題的數百萬個數學問題。比賽期間還套用了訓練 loop，以強化自生成競賽題變體的證明，直到找到完整的解決方案。
AlphaProof 強化學習訓練 loop 過程資訊圖：約一百萬個非形式化數學問題被形式化網絡轉譯成形式化數學語言。然後，求解器網絡搜尋問題的證明或反證，透過 AlphaZero 演算法逐步訓練自己解決更具挑戰性的問題。
更具競爭力的 AlphaGeometry 2
AlphaGeometry 2 是今年登上【自然】雜誌的數學 AI AlphaGeometry 的重大改進版本。它是一個神經 - 符號混合系統，其中的語言模型基於 Gemini，並在比其前身多一個數量級的合成數據上從頭開始訓練。這有助於該模型解決更具挑戰性的幾何問題，包括有關物體運動以及角度、比例或距離方程式的問題。
AlphaGeometry 2 采用的符號引擎比上一代產品快兩個數量級。當遇到新問題時，新穎的共享創意機制可實作不同搜尋樹的高級組合，以解決更復雜的問題。
在今年的比賽之前，AlphaGeometry 2 可以解決過去 25 年中所有 IMO 幾何歷史問題的 83%，而其前身的解決率僅為 53%。在 IMO 2024 中，AlphaGeometry 2 在收到問題 4 的形式化後 19 秒內就解決了它。
問題 4 的範例，要求證明∠KIL 與∠XPY 的和等於 180°。AlphaGeometry 2 提議在直線 BI 上構造點 E，使得∠AEB = 90°。點 E 有助於賦予線段 AB 中點 L 以意義，從而建立許多對相似三角形，如 ABE ~ YBI 和 ALE ~ IPC，以證明結論。
谷歌 DeepMind 還報告說，作為 IMO 工作的一部份，研究人員還試驗了一種基於 Gemini 和一種最新的自然語言推理系統，希望實作高級的問題解決能力。該系統不需要將問題轉譯成正式語言，並且可以與其他 AI 系統相結合。在今年的 IMO 賽題的測試中「顯示出了巨大的潛力」。
谷歌正在繼續探索推進數學推理的 AI 方法，並計劃很快釋出有關 AlphaProof 的更多技術細節。
我們對未來充滿期待，數學家們將使用 AI 工具探索假設，嘗試大膽的新方法來解決長期存在的問題，並快速完成耗時的證明元素——而像 Gemini 這樣的 AI 系統將在數學和更廣泛的推理方面變得更加強大。
研究團隊
谷歌表示，新研究得到了國際數學奧林匹克組織的支持，此外：
AlphaProof 的開發由 Thomas Hubert、Rishi Mehta 和 Laurent Sartran 領導；主要貢獻者包括 Hussain Masoom、Aja Huang、Miklós Z. Horváth、Tom Zahavy、Vivek Veeriah、Eric Wieser、Jessica Yung、Lei Yu、Yannick Schroecker、Julian Schrittwieser、Ottavia Bertolli、Borja Ibarz、Edward Lockhart、Edward Hughes、Mark Rowland 和 Grace Margand。
其中，Aja Huang、Julian Schrittwieser、Yannick Schroecker 等成員也是 8 年前（2016 年）AlphaGo 論文的核心成員。8 年前，他們基於強化學習打造的 AlphaGo 聲名大噪。8 年後，強化學習在 AlphaProof 中再次大放異彩。有人在朋友圈感嘆說：RL is so back！
AlphaGeometry 2 和自然語言推理工作由 Thang Luong 領導。AlphaGeometry 2 的開發由 Trieu Trinh 和 Yuri Chervonyi 領導，Mirek Olšák、Xiaomeng Yang、Hoang Nguyen、Junehyuk Jung、Dawsen Hwang 和 Marcelo Menegali 做出了重要貢獻。
此外，David Silver、Quoc Le、哈薩比斯和 Pushmeet Kohli 負責協調和管理整個專案。
參考內容：
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
