水平接近人類金牌選手，人工智能（AI）學會做國際數學奧林匹克競賽難題了。
這個名爲 AlphaGeometry 的 AI 模型由來自 Google DeepMind 和紐約大學的聯合團隊研發，是一個能解國際數學奧林匹克競賽級别幾何題的 AI 系統，于近日登上了頂級科學期刊 Nature。
據介紹，AlphaGeometry 通過自主合成數百萬個定理和證明，解決了 30 個最新奧林匹克級别（優等高中生參加的數學定理證明大賽）問題中的 25 個，接近國際數學奧林匹克競賽金牌選手的平均表現，遠超之前最好的自動化定理證明系統。
這一突破标志着 AI 在數學問題解決方面取得了顯著的進展——無需人類演示即可自主應對複雜的幾何學挑戰。
該研究證明了 AI 能以接近人類最高水平破解複雜邏輯挑戰的潛力——這正是 AI 研究的一個主要目标。
值得一提的是，AlphaGeometry 能生成人類可閱讀的證明，甚至發現了 2004 年國際數學奧林匹克競賽定理的一個新版本。
相關研究論文以 "Solving olympiad geometry without human demonstrations" 爲題，1 月 17 日發表在 Nature 上。
AI 搞定奧數題，很難嗎？
自 20 世紀 50 年代以來，追求更好的定理證明能力一直是 AI 研究的焦點。數學奧林匹克競賽是世界上最著名的定理證明競賽，其曆史可以追溯到 1959 年，在發現卓越人才方面有着重要作用。
國際數學奧林匹克競賽的題目通常涉及深度的數學理論和抽象的數學概念，需要獨立思考、創造性解決問題和運用直覺。這些問題往往要求高度的邏輯推理和創造性的思維，這是人類數學家所具備的，但超越了傳統的機器學習方法的應用範圍。
此外，與其他領域相比，人類解決數學問題的過程不容易轉化爲大規模的可用于訓練的數據集。幾何學具有特有的翻譯困難，在通用數學語言中的證明示例也很少。并且幾何語言具有非常精準的定義，無法表達許多使用幾何範圍之外的人類證明，比如複數。
圖｜IMO2000P6 的人類證明和 AlphaGeometry 證明的并排比較。這是一個較難的問題（人類平均得分 = 1.05/7），問題陳述中包含大量對象。左圖，人類解決方案使用複數。通過精心選擇的坐标系，問題會大大簡化，并且通過代數運算自然可以得出解決方案。右圖，AlphaGeometry 解決方案涉及兩個輔助構造和 100 多個推導步驟，其中許多低級步驟對于人類來說極其乏味。在這種情況下，基于搜索的解決方案的可讀性和直觀性要差得多。更具結構性的組織，即高級的證明大綱，可以大大提高 AlphaGeometry 解決方案的可讀性。在 AlphaGeometry 中構建許多高級推導規則，有助于減少低級推導并簡化證明步驟。（來源：該論文）
缺乏足夠的樣本數據，特别是包含人類專業數學家的解答過程，使得機器學習模型難以學習和理解解題方法。因此，目前的幾何方法仍主要依賴于符号方法和人工設計的硬編碼搜索啓發式。
無需人類，自主解決複雜問題
在該研究中，AlphaGeometry 的關鍵創新點在于，其能夠綜合數百萬條複雜程度各異的定理和證明，利用從頭訓練的神經語言模型進行自主訓練。這意味着 AlphaGeometry 能夠獨立學習和解決各類複雜問題，而無需依賴人類輸入。
神經語言模型在引導符号演繹引擎（能夠搜索難題中的大量分支點）方面具有獨特的優勢。神經模型的引入使得 AlphaGeometry 在處理具有挑戰性的問題時能夠做出更爲精準的推理。這種綜合運用符号演繹引擎和神經語言模型的方法是該研究的重要創新之一。
圖｜AlphaGeometry 概述以及它如何解決簡單問題和 IMO2015 問題 3。頂行顯示 AlphaGeometry 如何解決簡單問題。a）簡單的例子及其圖表。b）模型通過運行符号推演引擎來啓動證明搜索。引擎從定理前提中詳盡地推導出新的陳述，直到定理被證明或新的陳述被窮舉爲止。c）由于符号引擎未能找到證明，語言模型構造一個輔助點，在符号引擎重試之前增長證明狀态。循環繼續直到找到解決方案。d）對于簡單的例子，循環在第一個輔助結構 "D 作爲 BC 的中點 " 之後終止。該證明包括另外兩個步驟，這兩個步驟都利用了中點屬性："BD = DC" 和 "B、D、C 共線 "。底行顯示了 AlphaGeometry 如何解決 IMO 2015 Problem 3 ( IMO 2015 P3 ) 。e）IMO 2015 P3 問題陳述和圖表。f IMO 2015 P3 的解有 3 個輔助點。（來源：該論文）
盡管 AlphaGeometry 在解決奧林匹克級别的幾何問題上取得了顯著的成功，但也存在一些局限性。
據論文描述，AlphaGeometry 主要專注于解決奧林匹克級别的幾何問題，應用範圍相對狹窄。這限制了該方法在其他數學領域或實際問題中的推廣。未來的研究需要探讨如何擴展該方法以涵蓋更廣泛的數學領域。
而且，研究團隊采用了大規模的人工合成數據來訓練 AlphaGeometry，這雖然爲模型提供了廣泛的學習材料，但合成數據仍然可能無法完全覆蓋真實數學問題的多樣性和複雜性。因此，模型在真實場景中的性能可能會受到數據不足的影響。
此外，雖然 AlphaGeometry 能夠生成人類可讀的證明，但在處理極其複雜的推理時，其生成的結果可能變得難以理解。這使得人們在一些情況下難以追蹤和解釋模型的推理過程。
解決數學問題，AI 大有可爲
近年來，使用 AI 技術來理解和證明數學定理，是科學家們重點關注的研究方向之一。
例如，AI 可以被用來開發自動定理證明系統，這些系統可以獨立地推導和證明數學定理。這種方法旨在減輕人工證明的負擔，并提供更高效的證明方法。
此外，AI 也可以被用來構建數學知識圖譜，有助于将數學概念之間的關系建模成圖結構。這種圖譜可以用于改進定理的推理和證明，使得系統能夠更好地理解數學領域的知識體系。
對于創造性思維的開發，AI 也有一席之地。一些研究采用生成式模型，比如生成對抗網絡（GANs），來生成符合數學結構和規範的新定理。這種方法有助于拓展數學領域的創造性思維，引入新的數學概念和結論。
當然，要使得 AI 在數學領域展現出如人類頂尖數學家一般的水平，還有很長的路要走。
盡管如此，AlphaGeometry 展現出了 AI 在數學方面的應用潛力，這一成果不僅爲數學領域帶來了創新，也爲 AI 在其他領域的應用帶來了新的可能。
本文來自微信公衆号：學術頭條 （ID：SciTouTiao），作者：學術頭條
