Google DeepMind的 AI 在國際數學奧林匹克競賽中達到銀牌標準

DeepMind的突破性模型AlphaProof和AlphaGeometry 2解決了高級數學推理問題，在今年的國際數學奧林匹克競賽（IMO）中達到銀牌水平。AlphaProof基於強化學習進行形式化數學推理，而AlphaGeometry 2則是改進版幾何問題解決系統。這些系統解決了本年度競賽的六道題中的四道，得分28分，與銀牌標準相當。

AlphaProof是一種基於強化學習的形式化數學推理系統，能夠證明數學陳述的正確性。它結合了預訓練語言模型和AlphaZero強化學習算法，使用形式語言Lean進行訓練和推理。

AlphaGeometry 2是改進版的幾何問題解決系統，採用神經符號混合方法，並在大量合成數據上進行了訓練。該系統能夠更快、更高效地解決幾何問題。

• 國際數學奧林匹克簡介：IMO是歷史最悠久、規模最大、最負盛名的青年數學競賽，每年吸引世界頂尖的預科學家參加。
• 模型表現：在今年的IMO中，AlphaProof和AlphaGeometry 2共解決了四個問題，得到了28分，與銀牌得主的成績相當。
• AlphaProof的工作原理：通過訓練數百萬個數學問題，AlphaProof生成並驗證解決方案，強化其語言模型的推理能力。
• AlphaGeometry 2的改進：通過更快的符號引擎和知識共享機制，AlphaGeometry 2在更短時間內解決了更多複雜的幾何問題。

圖中顯示了Deepmind的人工智能系統在 2024 年國際海事組織（IMO）比賽中相對於人類選手的表現。在 42 分的總分中，我們獲得了 28 分，達到了與銀牌獲得者相同的水平。

AlphaProof

• 能力

  • AlphaProof能夠理解並解決複雜的數學證明問題。
  • 它可以處理代數和數論等領域的問題。
  • 在國際數學奧林匹克（IMO）比賽中，AlphaProof成功解決了兩個代數問題和一個數論問題，其中包括一個只有五個參賽選手能夠解決的極難問題。

• 原理

  • 強化學習：AlphaProof使用強化學習算法，通過不斷嘗試和學習，逐步提高自己的解題能力。
  • 形式語言Lean：它將數學問題轉換成形式語言Lean來處理。形式語言可以讓AI更準確地理解和驗證數學證明的正確性。
  • 自動生成證明：當面對一個新問題時，AlphaProof會生成多個可能的解法，然後逐一驗證這些解法，找到正確的答案。
  • 持續訓練：AlphaProof通過訓練數百萬個數學問題，不斷提升自己的推理能力和解題速度。

• 應用

  • AlphaProof的能力使其能夠解決高難度的數學問題，尤其是在學術研究和科學發現中具有重要應用潛力。
  • 它還能夠輔助數學家驗證複雜的數學證明，節省大量時間和精力。

AlphaProof 強化學習訓練循環過程信息圖：約一百萬個非正式數學問題被形式化網絡翻譯成正式數學語言。然後，求解器網絡搜索問題的證明或反證，通過 AlphaZero 算法逐步訓練自己解決更具挑戰性的問題。

AlphaGeometry 2

• 能力

  • AlphaGeometry 2專注於解決幾何問題，具有極高的準確性和效率。
  • 它在處理幾何問題時表現出色，在今年的IMO中，成功解決了一個幾何問題，用時僅19秒。
  • 它的改進版本相比前代解決了更多的幾何問題，在過去25年的IMO幾何題中達到了83%的解決率。

• 原理

  • 神經符號混合方法：AlphaGeometry 2結合了神經網絡和符號推理的方法。神經網絡幫助理解和處理幾何題目，符號推理用於精確計算和驗證解法。
  • 知識共享機制：當面對新問題時，AlphaGeometry 2利用已有的知識庫，通過共享和組合不同的搜索樹，快速找到解法。
  • 高速符號引擎：改進後的符號引擎比前代快了兩個數量級，使得AlphaGeometry 2能夠更快地處理複雜的幾何問題。
  • 合成數據訓練：通過大量的合成數據進行訓練，使模型在處理各種不同類型的幾何問題時更加靈活和高效。

• 應用

  • AlphaGeometry 2的幾何問題解決能力使其在教育、科學研究和工程應用中具有廣泛的潛力。
  • 它能夠幫助學生和研究人員快速解決幾何問題，提高學習和研究效率。

官方博客翻譯

AI在解決國際數學奧林匹克問題上達到銀牌標準

突破性模型AlphaProof和AlphaGeometry 2解決了數學中的高級推理問題

具備高級數學推理能力的通用人工智能 (AGI) 有望在科學和技術領域開闢新前沿。

我們在開發幫助數學家發現新見解、新算法和解決未解問題的AI系統方面取得了重大進展。但目前的AI系統在解決一般數學問題時仍存在推理能力和訓練數據的限制。

今天，我們推出了AlphaProof，這是一個基於強化學習的形式數學推理新系統，還有改進版的AlphaGeometry 2，我們的幾何解題系統。這兩個系統共同解決了今年國際數學奧林匹克 (IMO) 的六個問題中的四個，首次達到了銀牌水平。

解決複雜數學問題的突破性AI表現

IMO是歷史最悠久、規模最大、最負盛名的年輕數學家比賽，自1959年起每年舉辦。

每年，頂尖的預科數學家會訓練數千小時，以解決代數、組合數學、幾何和數論中的六個異常困難的問題。許多費爾茲獎得主曾代表他們的國家參加過IMO。

近些年，年度IMO競賽也被視為機器學習中的一大挑戰，併成為衡量AI系統高級數學推理能力的理想基準。

今年，我們的AI系統被應用於IMO主辦方提供的競賽問題。我們的解決方案由著名數學家、IMO金牌得主和費爾茲獎獲得者Timothy Gowers爵士和兩次IMO金牌得主、IMO 2024問題選擇委員會主席Joseph Myers博士根據IMO評分規則進行評分。

首先，這些問題被手動翻譯成我們系統可以理解的形式數學語言。在正式比賽中，學生需要在兩個4.5小時的會話中提交答案。我們的系統在幾分鐘內解決了一個問題，而解決其他問題則花費了三天時間。

AlphaProof解決了兩個代數問題和一個數論問題，通過確定答案並證明其正確性。這包括今年IMO中只有五名參賽者解決的最難問題。AlphaGeometry 2解決了幾何問題，而兩個組合數學問題未能解決。

每個問題可以獲得七分，總分為42分。我們的系統最終得分為28分，在每個解決的問題上都獲得了滿分——相當於銀牌類別的最高端。今年，金牌分數線從29分起，共有58名參賽者達到了這個分數。

AlphaProof：形式化推理的新方法

AlphaProof是一個用形式語言Lean證明數學陳述的系統。它結合了預訓練語言模型與之前自學掌握國際象棋、將棋和圍棋遊戲的AlphaZero強化學習算法。

形式語言提供了一個關鍵優勢，可以形式化驗證數學推理的證明。然而，之前由於人類編寫的數據非常有限，這些語言在機器學習中的應用受到限制。

相比之下，儘管自然語言方法可以使用更多數量級的數據，但在生成中間推理步驟和解決方案時可能會出現合理但不正確的情況。我們通過微調Gemini模型自動將自然語言問題陳述轉換為形式陳述，創建了一個包含不同難度形式問題的大型庫，在這兩個互補領域之間建立了橋樑。

面對一個問題時，AlphaProof會生成解決方案候選，並通過搜索Lean中的可能證明步驟來證明或反駁它們。每個找到並驗證的證明都會加強AlphaProof的語言模型，提高其解決後續更具挑戰性問題的能力。

在比賽前的幾週內，我們通過證明或反駁數百萬個問題，涵蓋各種難度和數學主題，對AlphaProof進行了訓練。比賽期間也應用了訓練循環，強化自生成的比賽問題變體的證明，直到找到完整的解決方案。

更強大的AlphaGeometry 2

AlphaGeometry 2是AlphaGeometry的顯著改進版。它是一個神經符號混合系統，基於Gemini的語言模型，並從頭開始在比前身多一個數量級的合成數據上進行訓練。這幫助模型解決了更具挑戰性的幾何問題，包括物體運動和角度、比率或距離方程的問題。

AlphaGeometry 2使用的符號引擎比前身快兩個數量級。面對新問題時，採用了一種新穎的知識共享機制，使不同搜索樹的高級組合能夠解決更複雜的問題。

在今年的比賽前，AlphaGeometry 2可以解決過去25年所有歷史IMO幾何問題的83%，而前身的解決率為53%。在IMO 2024中，AlphaGeometry 2在接收到形式化後在19秒內解決了問題4。

問題 4 的示例，要求證明∠KIL 與∠XPY 的和等於 180°。AlphaGeometry 2 提議在直線 BI 上構造點 E，使得∠AEB = 90°。點 E 有助於實現 AB 的中點 L 的目的，從而創建許多對相似三角形，如 ABE ~ YBI 和 ALE ~ IPC，以證明結論。

數學推理的新前沿

作為IMO工作的一部分，我們還嘗試了一個基於自然語言推理的系統，建立在Gemini和我們最新研究的基礎上，以實現高級問題解決能力。該系統不需要將問題翻譯成形式語言，並且可以與其他AI系統結合。我們還在今年的IMO問題上測試了這種方法，結果顯示出很大的希望。

我們的團隊繼續探索多種AI方法以推進數學推理，並計劃很快發佈更多關於AlphaProof的技術細節。

我們對未來感到興奮，在這個未來中，數學家可以使用AI工具探索假設，嘗試解決長期問題的新方法，並快速完成證明的耗時部分——AI系統如Gemini在數學和更廣泛的推理方面變得更有能力。

致謝

我們感謝國際數學奧林匹克組織的支持。

AlphaProof的開發由Thomas Hubert、Rishi Mehta和Laurent Sartran領導；AlphaGeometry 2和自然語言推理工作由Thang Luong領導。

原文：https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/