這項工作代表了 AI 在數學推理上的能力突破，是開發通用 AI 系統的重要里程碑。
這次，人工智慧演算法在數學奧林匹克競賽（IMO）上取得了重大成績突破。
在最新一期的國際權威期刊《自然》雜誌上，發表了一篇論文介紹了名為AlphaGeometry的人工智慧系統。該系統能夠解決奧林匹克幾何問題，而無需人類的示範。專家認為，這是人工智慧朝著具備人類推理能力的方向邁進的重要里程碑。這項研究成果的發表對於推動人工智慧的進一步發展具有重要意義。
論文連結：https://www.nature.com/articles/s41586-023-06747-5
DeepMind 也在論文發表的第一時間將程式碼和模型開源，GitHub：https://github.com/google-deepmind/alphageometry
這是一個人工智慧系統，來自Google DeepMind 研究者之手，它能夠以接近人類奧賽金牌得主的水平解決複雜的幾何問題。
在對30道奧數幾何題的基準測試中，AlphaGeometry在標準奧數時限內解決了25題，而之前最先進的系統只解決了其中10道幾何問題。與此相比，人類金牌得主的平均解答問題數為25.9個。
對於基於學習的AI模型來說，定理證明是一項具有挑戰性的任務。主要原因在於，大多數數學領域中的人類證明很難被翻譯成機器可驗證的語言，這限制了用於訓練AI模型的資料量。為了克服這個問題，DeepMind提出了一種替代方法，即使用合成資料進行定理證明。他們開發了一個通用的指導框架，稱為AlphaGeometry，該框架在許多領域都具有適用性。透過利用合成數據，AlphaGeometry能夠訓練AI模型進行定理證明，並產生高品質的結果。這方法為解決定理證明的困難提供了一個有效的解決方案。
研究介紹
AlphaGeometry 將語言模型與「符號引擎」結合，借助符號和邏輯規則進行數學推論。 在這其中，語言模型擅長識別、預測流程的後續步驟，但缺乏數學推理所需的嚴謹性；另一方面，符號引擎純粹基於形式邏輯和嚴格的規則，這使得它能夠引導語言模型走向理性決策。
在AlphaGeometry 的研究上，DeepMind 從跨越2000 年到2022 年之間的30 個奧林匹克幾何問題（IMO-AG-30）的基準測試集中進行了測試，結果表明，AlphaGeometry 在比賽時間限制下能夠解決25 個問題。而之前最先進的方法（Wu’s method）只能解決 10 個。
眾所周知，由於缺乏推理技能和訓練數據，AI 系統經常難以解決幾何和數學方面的複雜問題。 AlphaGeometry 系統將神經語言模型的預測能力與規則約束推理引擎結合，兩者協同工作以找到了新的解決方案。
此外，為了解決數據難題，該研究產生了大量的合成訓練數據，即1 億個示例，其中許多定理的證明步驟超過200 步，比數學奧林匹克競賽定理的平均證明長度長4倍。
AlphaGeometry 展示了 AI 不斷增長的邏輯推理能力以及發現和驗證新知識的能力。解決奧林匹克級的幾何問題是 AI 在邁向更先進和通用人工智慧系統道路上的一個重要里程碑。
菲爾茲獎得主、IMO 金牌得主Ngô Bảo Châu（吳寶珠）表示：「現在我完全明白了，為什麼AI 研究者們會先嘗試解決國際數學奧林匹克(IMO) 的幾何題目，因為找到它們的解決方案有點像下棋，我們在每一步都有相對較少的合理走法。但我仍然對他們能夠實現這一點感到震驚。這是一項令人印象深刻的成就。」
吳寶珠，2010 年菲爾茲獎得主，現任芝加哥大學教授。
#AlphaGeometry 是一個神經符號系統，由神經語言模型和符號推演引擎組成，它們共同尋找複雜幾何定理的證明。一個系統提供快速、直觀的想法，而另一種則提供更深思熟慮、理性的決策。
由於語言模型擅長識別資料中的一般模式和關係，因此它們可以快速預測潛在有用的結構，但通常缺乏嚴格推理或做出解釋。另一方面，符號推演引擎基於形式邏輯並使用明確的規則來得出結論，兩者相互配合，共同構成了 AlphaGeometry。
AlphaGeometry 的語言模型引導其符號推演引擎尋找幾何問題的可能解決方案。一般的奧林匹克幾何問題是基於圖表，需要添加新的幾何結構才能解決，例如點、線或圓。 AlphaGeometry 的語言模型可以從無數種可能性中預測添加哪些新結構最有用。這些線索有助於填補空白，並允許符號引擎對圖表進行進一步推論並接近解決方案。
舉例來說，下圖（上）為AlphaGeometry 解答簡單題的過程，題目為「設ABC 為AB = AC 的任意三角形。證明∠ABC = ∠BCA。」
# AlphaGeometry 證明過程是這樣的：AlphaGeometry 透過運行符號推演引擎（symbolic deduction engine）啟動證明搜尋。這個引擎會從定理的前提出發，詳盡地推導出新的陳述，直到定理被證明或新的陳述被耗盡。假如符號引擎未能找到證明，語言模型會建構一個輔助點，在符號引擎重新開始之前增加可證明的條件。這個循環一直持續到找到解決方案為止。對於簡單的例子，循環在第一個輔助結構“ BC 的中點添加 D 點”之後終止。
下圖（下）為 AlphaGeometry 解決 IMO 的解題思路。 「證明三角形 FKM 和 KQH 的外接圓 (O1) 和 (O2) 彼此相切……」，這麼複雜的問題，AlphaGeometry 同樣也能證明，證明過程還給出了輔助點等。出於說明目的，證明過程被大大縮短和編輯。
產生1 億數學推理訓練資料
人類可以在紙上進行勾勒來學習幾何、檢查圖表並使用現有知識來發現新的、更複雜的幾何屬性和關係。該研究產生合成數據的方法大規模模擬了這種知識建構過程。其中產生合成資料的方法如圖 3 所示。
使用高度並行計算，系統首先產生 5 億個幾何物件的隨機圖，並詳盡地導出每個圖中點和線之間的所有關係。 AlphaGeometry 找到每個圖表中包含的所有證明，然後逆向推導，找出需要哪些額外的結構（如果有的話）來獲得這些證明。此過程為「符號推演與回溯」。
AlphaGeometry 產生的合成資料的視覺化表示
之後，這個巨大的資料池被過濾以排除類似的範例，從而產生了1 億個訓練資料集。
開創性的人工智慧推理能力
AlphaGeometry 提供的每一道奧數題的解法都經過電腦檢查和驗證。研究人員還將其結果與先前的人工智慧方法以及人類在奧林匹克競賽中的表現進行了比較。此外，數學教練、前奧賽金牌得主 Evan Chen（陳誼廷）為我們評估了 AlphaGeometry 的一系列解決方案。
陳誼廷，MIT 數學在讀博士，曾獲得 IMO 2014 年金牌。
Evan Chen 表示：「AlphaGeometry 的輸出令人印象深刻，因為它既可驗證又乾淨。過去針對基於證明的競爭問題的人工智慧解決方案有時是碰巧的（輸出有時是正確的，需要人工檢查），而AlphaGeometry 沒有這個弱點：它的解決方案具有機器可驗證的結構。另一方面，它的輸出仍然是人類可讀的。人們可以想像一個通過強力坐標系解決幾何問題的電腦程式：想想一頁又一頁繁瑣的代數計算，AlphaGeometry 不是這樣做的，它像人類學生一樣使用帶有角度和相似三角形的經典幾何規則。」
最近一段時間，金融科技公司 XTX Markets 設立了人工智慧奧林匹克數學獎（AI-MO Prize），旨在鼓勵能夠進行數學推理的人工智慧模型的開發。由於每個奧林匹克競賽都有六個問題，其中只有兩個通常集中在幾何上，因此 AlphaGeometry 只能應用於給定奧林匹克競賽中的三分之一問題。
儘管如此，AlphaGeometry 僅靠自己的幾何解題能力就成為了世界上第一個能夠在 2000 年和 2015 年通過 IMO 銅牌門檻的人工智慧模型。
DeepMind 已在著手推進下一代人工智慧系統的推理。研究人員認為，鑑於利用大規模合成資料從頭開始訓練人工智慧系統的廣泛潛力，這種方法可能會影響未來人工智慧系統發現數學及其他領域新知識的方向。
AlphaGeometry 開創了人工智慧數學推理的先河 —— 從探索純數學之美到使用語言模型解決數學和科學問題。人們希望這種技術能持續提升，進而解決更高階、抽象的數學問題。
而在數學之外，AlphaGeometry 的影響或許還可以涵蓋更多包含幾何問題的領域，如電腦視覺、建築，甚至理論物理學等。
參考內容：
https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system -for-geometry/
#以上是深度學習在幾何推理上獲得天才級表現，Nature發表了DeepMind的模型，並在菲爾茲獎得主新聞中獲得讚譽的詳細內容。更多資訊請關注PHP中文網其他相關文章！
