中新網北京1月18日電 (記者 孫自法)國際著名學術期刊《自然》最新發表一篇計算機科學論文稱,研究人員開發出一個能解國際數學奧林匹克競賽級別幾何題的人工智能(AI)系統,表現超過了之前最好的自動化定理證明系統。該研究證明了AI能以接近人類最高水平破解復雜邏輯挑戰的潛力,而這正是AI研究的一個主要目標。
該論文介紹,奧林匹克水平的數學定理證明需要高水平的邏輯推理和解題能力。然而,當前基于機器學習的AI系統在證明數學定理方面還有困難。機器學習這種AI形式通過向計算機提供參考數據,讓計算機學習如何執行特定任務,但由于作為訓練數據的人類示范很少,所以定理證明(尤其是幾何學定理)很難被掌握。
在本項研究中,論文第一作者兼共同通訊作者、美國谷歌Deepmind和紐約大學的Trieu H. Trinh與同事合作,開發出一種不需要人類示范的定理證明方法的系統并命名為AlphaGeometry,其通過綜合復雜程度各異的數百萬條定理和證明,利用一個神經語言模型完成自我訓練。這種方法結合符號演繹引擎(能搜索難題中的大量分支點),能讓AlphaGeometry在無需人類直接輸入的情況下學習并解開復雜問題。
他們用國際數學奧林匹克競賽(優秀高中生參加的數學定理證明大賽)2000-2020年的30個問題對G0進行測試,結果AlphaGeometry解出了其中25題,接近國際數學奧林匹克競賽金牌選手的平均表現,而之前最優秀的方法只解出了10題。值得一提的是,AlphaGeometry能生成人類可閱讀的證明,甚至發現了2004年國際數學奧林匹克競賽定理的一個新版本。
論文作者指出,應用AI技術的AlphaGeometry系統目前雖然僅限于幾何學,但這種方法或許也能應用于其他數學領域。