《自然》17日發表的一項計算科學研究，描述了一個能解國際數學奧林匹克競賽級別幾何題的人工智能（AI）系統。其表現超過了之前最好的自動化定理證明系統。該研究證明了AI已接近人類破解復雜邏輯問題的最高水平。
奧林匹克競賽中的數學定理證明需要高水平的邏輯推理和解題能力。然而，當前基于機器學習的AI系統在證明數學定理方面還有困難。機器學習通過向計算機提供參考數據，讓計算機學習如何執行特定任務。但由于作為訓練數據的人類示范很少，所以定理證明，尤其是幾何學定理很難被證明。
谷歌“深度思維”團隊此次描述了一種不需要人類示范的定理證明方法。基于這一方法的AI系統名為“阿爾法幾何”（G0）。它綜合了復雜程度各異的數百萬條定理和證明，并利用一個神經語言模型完成自我訓練。這種方法結合符號演繹引擎（能搜索難題中的大量分支點），能讓G0在無需人類直接輸入的情況下學習并解開復雜問題。
團隊用國際數學奧林匹克競賽2000年至2020年間的30個問題測試了該系統。G0解出了其中25題，接近國際數學奧林匹克競賽金牌選手的平均表現。而之前最優秀的方法只解出了10題。值得一提的是，G0能生成人類可閱讀的證明，甚至發現了2004年國際數學奧林匹克競賽定理的一個新版本。
研究人員指出，G0目前僅限于證明幾何學定理，但這種方法或許能應用于其他數學領域。
《自然》17日發表的一項計算科學研究，描述了一個能解國際數學奧林匹克競賽級別幾何題的人工智能（AI）系統。其表現超過了之前最好的自動化定理證明系統。該研究證明了AI已接近人類破解復雜邏輯問題的最高水平。
奧林匹克競賽中的數學定理證明需要高水平的邏輯推理和解題能力。然而，當前基于機器學習的AI系統在證明數學定理方面還有困難。機器學習通過向計算機提供參考數據，讓計算機學習如何執行特定任務。但由于作為訓練數據的人類示范很少，所以定理證明，尤其是幾何學定理很難被證明。
谷歌“深度思維”團隊此次描述了一種不需要人類示范的定理證明方法?；谶@一方法的AI系統名為“阿爾法幾何”（G0）。它綜合了復雜程度各異的數百萬條定理和證明，并利用一個神經語言模型完成自我訓練。這種方法結合符號演繹引擎（能搜索難題中的大量分支點），能讓G0在無需人類直接輸入的情況下學習并解開復雜問題。
團隊用國際數學奧林匹克競賽2000年至2020年間的30個問題測試了該系統。G0解出了其中25題，接近國際數學奧林匹克競賽金牌選手的平均表現。而之前最優秀的方法只解出了10題。值得一提的是，G0能生成人類可閱讀的證明，甚至發現了2004年國際數學奧林匹克競賽定理的一個新版本。
研究人員指出，G0目前僅限于證明幾何學定理，但這種方法或許能應用于其他數學領域。
本文鏈接：能解國際奧數競賽題的AI系統問世http://m.lensthegame.com/show-2-2309-0.html
聲明：本網站為非營利性網站，本網頁內容由互聯網博主自發貢獻，不代表本站觀點，本站不承擔任何法律責任。天上不會到餡餅，請大家謹防詐騙！若有侵權等問題請及時與本網聯系，我們將在第一時間刪除處理。
上一篇： 納米機器人將膀胱腫瘤縮小90%
下一篇： 二維重費米子材料首次創建