<div id="readability-page-1">高級數學推理是現代人工智能的關鍵能力。今天，Google 宣佈了一項長期重大挑戰中的一個重要里程碑：Google 混合人工智能系統在今年的國際數學奧林匹克競賽（IMO）中獲得了相當於銀牌的成績 具體來説 google 展示了第一個以銀牌級別解決國際數學奧林匹克問題的人工智能 它結合了 AlphaProof（一種新的突破性形式推理模型）和 AlphaGeometry 2（之前系統的改進版本） 國際數學奧林匹克競賽是全球最悠久、規模最大、最具聲望的青年數學家比賽，自 1959 年起每年舉辦一次。參賽者需要解決六道涉及代數、組合學、幾何和數論的極其困難的問題。許多菲爾茲獎得主曾在青年時期代表國家參加過 IMO。近年來，IMO 也成為了機器學習領域的一個重要挑戰，被視為衡量人工智能系統高級數學推理能力的標杆 在今年的比賽中，DeepMind 的 AI 系統獲得了 28 分（滿分 42 分），相當於銀牌獲得者的水平。這一成績僅差 1 分就能達到金牌標準，而在今年的 609 名參賽者中，只有 58 人獲得了金牌 <img src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/544750ab-e0e1-4481-a546-47a442ae625a.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw?x-oss-process=image/auto-orient,1/interlace,1/resize,w_1440,h_1440/quality,q_95/format,jpg" width="640" height="640" original-src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/544750ab-e0e1-4481-a546-47a442ae625a.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw"/> <h2>AlphaProof：形式化數學推理的突破</h2> AlphaProof 系統採用強化學習方法，將預訓練的語言模型與 AlphaZero 算法相結合。這種方法的優勢在於可以正式驗證涉及數學推理的證明的正確性。為了克服形式化語言訓練數據不足的問題，研究團隊通過微調 Gemini 模型，創建了一個包含各種難度的形式化問題庫 AlphaProof 是一個自學習系統，專門用於在形式化數學語言 Lean 中證明數學陳述。它的核心創新在於結合了預訓練語言模型和 AlphaZero 強化學習算法 工作流程如下： <img src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/2041e0fd-1562-4867-b465-d5c43a1fd165.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw?x-oss-process=image/auto-orient,1/interlace,1/resize,w_1440,h_1440/quality,q_95/format,jpg" width="640" height="640" original-src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/2041e0fd-1562-4867-b465-d5c43a1fd165.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw"/> 1.問題轉化：首先，使用經過微調的 Gemini 模型將自然語言的數學問題自動轉換為 Lean 的形式化語言。這一步驟創建了一個大型的形式化問題庫，涵蓋不同難度級別 <img src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/d17b6ac9-1238-4a42-8b81-90326c49db97.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw?x-oss-process=image/auto-orient,1/interlace,1/resize,w_1440,h_1440/quality,q_95/format,jpg" width="640" height="640" original-src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/d17b6ac9-1238-4a42-8b81-90326c49db97.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw"/> 2.解決方案生成：面對一個新問題時，AlphaProof 會生成可能的解決方案 3.證明搜索：系統在 Lean 中搜索可能的證明步驟，試圖證明或反駁這些解決方案 4.強化學習：每找到並驗證一個證明，就用它來強化 AlphaProof 的語言模型，提高系統解決後續更具挑戰性問題的能力 5.持續訓練：在準備 IMO 比賽期間，AlphaProof 在數週內證明或反駁了數百萬個問題，覆蓋各種難度和數學主題。在比賽過程中，它還繼續應用這個訓練循環，通過證明自己生成的比賽問題變體來增強能力，直到找到完整解決方案 <h2>AlphaGeometry 2</h2> AlphaGeometry 2 是 AlphaGeometry 的改進版本，它的語言模型基於 Gemini，並在比前代多一個數量級的合成數據上進行了訓練 <img src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/bf039204-358c-469b-9ef2-ff7ed613e75f.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw?x-oss-process=image/auto-orient,1/interlace,1/resize,w_1440,h_1440/quality,q_95/format,jpg" width="640" height="640" original-src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/bf039204-358c-469b-9ef2-ff7ed613e75f.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw"/> 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 分即可摘金牌》 </div>

谷歌-A

谷歌-C

谷歌的人工智能系統在國際數學奧林匹克競賽中獲得了相當於銀牌的成績，展示了其在解決數學問題方面的突破性能力。該系統結合了 AlphaProof 和 AlphaGeometry 2，以較高水平解答了國際數學奧林匹克問題。這是一項重要的里程碑，顯示了人工智能在數學領域的潛力。

- Google 混合人工智能系統在國際數學奧林匹克競賽獲得相當於銀牌的成績，展示了高級數學推理能力。
- AlphaProof 結合了預訓練語言模型和 AlphaZero 算法，用於形式化數學推理，通過強化學習方法驗證數學證明的正確性。
- AlphaGeometry 2 是神經符號混合系統，速度更快，能解決過去 25 年 IMO 幾何問題的 83%，在今年的比賽中僅用 19 秒解決一個問題。