在從圍棋到戰略棋類游戲的所有領域戰勝人類后，美國谷歌公司旗下的DeepMind表示，它即將在解決數學問題方面擊敗全球最優秀的學生。
7月25日，DeepMind宣布，其人工智能（AI）系統已經解答了本月在英國巴斯舉行的2024年國際數學奧林匹克競賽（IMO）6個題目中的4個。AI給出了嚴謹、循序漸進的證明，并由兩名頂級數學家打分，得分為28/42，這相當于銀牌的成績，僅比金牌差1分。
“這顯然是一個非常重大的進步?！庇鴦虼髮W數學家Joseph Myers說。他與菲爾茲獎獲得者Tim Gowers一起，幫助挑選了今年IMO的原始題目并審查了這些解題方案。
DeepMind和其他公司正在競相讓機器最終提供證明，以解決數學領域的實質性研究問題。該公司表示，IMO的題目已經成為實現這一目標的基準，并被視為機器學習的“重大挑戰”。
“這是AI系統首次達到獎牌級別的表現。”DeepMind負責AI科學的副總裁Pushmeet Kohli表示，“這是高級定理證明過程中的一座關鍵里程碑?！?/p>
今年1月，DeepMind的AI系統AlphaGeometry在解決一類IMO問題——歐幾里得幾何方面取得了獎牌級別的成績。這是第一個在整體測試中達到金牌水平的AI，包括代數、組合數學和數論。這些問題通常被認為比幾何更具挑戰性，解決它們將有資格獲得500萬美元獎金。
在最新研究中，研究人員使用AlphaGeometry2在20秒內解決了幾何問題。DeepMind計算機科學家Thang Luong表示，該AI是他們創紀錄系統的改進版本，速度更快。
對于其他類型的問題，該團隊開發了一個名為AlphaProof的全新系統。新系統花了3天時間解決了競賽中的兩道代數題，外加一道數論題。不過，它無法解決組合數學領域的兩道題。
當試圖用語言模型回答數學問題時，研究人員得到了喜憂參半的結果。有時，這些模型給出了正確答案，但無法合理解釋其推理；有時，它們會胡說八道。
據介紹，AlphaProof將語言模型與強化學習技術相結合，使用了DeepMind的AlphaZero系統，后者成功用于“狙擊”圍棋等游戲以及解決一些特定數學問題。
在強化學習中，神經網絡通過試錯進行學習。當它的答案可以被客觀指標評估時，這種方法就很有效。為此，AlphaProof被訓練用一種名為Lean的正式語言來閱讀和編寫證明，Lean被用于數學家常用的同名“證明助手”軟件包。AlphaProof在Lean軟件包中運行并測試其輸出是否正確，這有助于填充代碼中的一些步驟。
訓練任何語言模型都需要大量數據，但Lean中幾乎沒有數學證明。DeepMind機器學習研究員Thomas Hubert表示，為了解決這個問題，團隊設計了一個額外網絡，試圖將現有的100萬個用自然語言編寫的問題轉化成Lean語言，但不包括人工編寫的解題方案。
許多Lean的翻譯都是荒謬的，但足夠多的翻譯足以讓AlphaProof開啟它的強化學習周期。Gowers說，結果遠遠好于預期。在某些情況下，AlphaProof似乎能夠提供額外的創造力，在無限的可能性中做出正確的選擇。但Gowers補充說，還需要進一步分析才能確定。
Myers表示，這些技術能否完善到在數學領域進行研究級別的工作，仍有待觀察?！八軘U展到其他類型的數學問題嗎？在那里可能沒有100萬個問題可以訓練?！?/p>
來源：《中國科學報》
