The AlphaGo moment in the mathematical world: Google's DeepMind AI solves an IMO geometry problem in 19 seconds, just 1 point away from winning the gold medal

高級數學推理是現代人工智能的關鍵能力。今天，Google 宣佈了一項長期重大挑戰中的一個重要里程碑：Google 混合人工智能系統在今年的國際數學奧林匹克競賽（IMO）中獲得了相當於銀牌的成績

具體來説 google 展示了第一個以銀牌級別解決國際數學奧林匹克問題的人工智能

它結合了 AlphaProof（一種新的突破性形式推理模型）和 AlphaGeometry 2（之前系統的改進版本）

國際數學奧林匹克競賽是全球最悠久、規模最大、最具聲望的青年數學家比賽，自 1959 年起每年舉辦一次。參賽者需要解決六道涉及代數、組合學、幾何和數論的極其困難的問題。許多菲爾茲獎得主曾在青年時期代表國家參加過 IMO。近年來，IMO 也成為了機器學習領域的一個重要挑戰，被視為衡量人工智能系統高級數學推理能力的標杆

在今年的比賽中，DeepMind 的 AI 系統獲得了 28 分（滿分 42 分），相當於銀牌獲得者的水平。這一成績僅差 1 分就能達到金牌標準，而在今年的 609 名參賽者中，只有 58 人獲得了金牌

AlphaProof：形式化數學推理的突破

AlphaProof 系統採用強化學習方法，將預訓練的語言模型與 AlphaZero 算法相結合。這種方法的優勢在於可以正式驗證涉及數學推理的證明的正確性。為了克服形式化語言訓練數據不足的問題，研究團隊通過微調 Gemini 模型，創建了一個包含各種難度的形式化問題庫

AlphaProof 是一個自學習系統，專門用於在形式化數學語言 Lean 中證明數學陳述。它的核心創新在於結合了預訓練語言模型和 AlphaZero 強化學習算法

工作流程如下：

1.問題轉化：首先，使用經過微調的 Gemini 模型將自然語言的數學問題自動轉換為 Lean 的形式化語言。這一步驟創建了一個大型的形式化問題庫，涵蓋不同難度級別

2.解決方案生成：面對一個新問題時，AlphaProof 會生成可能的解決方案

3.證明搜索：系統在 Lean 中搜索可能的證明步驟，試圖證明或反駁這些解決方案

4.強化學習：每找到並驗證一個證明，就用它來強化 AlphaProof 的語言模型，提高系統解決後續更具挑戰性問題的能力

5.持續訓練：在準備 IMO 比賽期間，AlphaProof 在數週內證明或反駁了數百萬個問題，覆蓋各種難度和數學主題。在比賽過程中，它還繼續應用這個訓練循環，通過證明自己生成的比賽問題變體來增強能力，直到找到完整解決方案

AlphaGeometry 2

AlphaGeometry 2 是 AlphaGeometry 的改進版本，它的語言模型基於 Gemini，並在比前代多一個數量級的合成數據上進行了訓練

AlphaGeometry 2 是一個神經符號混合系統。主要改進包括：

1.增強的語言模型：基於 Gemini，從頭開始訓練，使用了比前代多一個數量級的合成數據。這大大提高了模型處理複雜幾何問題的能力，包括物體運動、角度方程、比例或距離等問題

2.更快的符號引擎：新版本的符號處理引擎速度提高了兩個數量級，大大加快了問題解決速度

3.知識共享機制：引入了新的知識共享機制，能夠高級組合不同的搜索樹，以解決更復雜的問題

4.性能提升：在接受今年 IMO 比賽前，AlphaGeometry 2 能夠解決過去 25 年 IMO 幾何問題的 83%，遠超前代系統 53% 的解決率

5.實時表現：在今年的 IMO 中，AlphaGeometry 2 在接收到形式化的第 4 題後，僅用 19 秒就解決了這個問題

6.DeepMind 的研究團隊還在探索基於自然語言推理的系統，這種系統不需要將問題轉換為形式化語言，可能與其他 AI 系統結合使用。這種方法在今年的 IMO 問題上也顯示出了巨大的潛力

本文作者：AI 寒武紀，來源：AI 寒武紀，原文標題：《數學界的 AlphaGo 時刻：谷歌 DeepMind AI 19 秒解 IMO 幾何題，僅差 1 分即可摘金牌》