谷歌旗下的AI研究機(jī)構(gòu)DeepMind和紐約大學(xué)的研究人員聯(lián)合開發(fā)了一個AI模型——AlphaGeometry。

AlphaGeometr是一種神經(jīng)符號模型,內(nèi)置了大語言模型和符號推理引擎等功能,主要用于解決各種超難幾何數(shù)學(xué)題，同時可以自動生成易于查看的解題原理。

為了驗(yàn)證AlphaGeometr的性能，研究人員使用了正規(guī)國際奧數(shù)比賽的規(guī)則對其進(jìn)行測試。

結(jié)果顯示，AlphaGeometry 在官方奧林匹克競賽時間限制下正確解決了，30道題中的25 道，接近人類金牌得主的25.9道。

而之前最先進(jìn)的模型只能解決30道中的10道題。AlphaGeometry成為目前功能最強(qiáng)的解決幾何難題模型。

論文地址：https://www.nature.com/articles/s41586-023-06747-5?ref=maginative.com

AlphaGeometry的核心技術(shù)創(chuàng)新在于，破除了定理證明，對人類證明示例數(shù)據(jù)的嚴(yán)重依賴。

數(shù)學(xué)定理證明一直是檢驗(yàn)邏輯思維和問題求解能力的關(guān)鍵任務(wù)，一直是AI研究的重要方向。盡管當(dāng)前機(jī)器學(xué)習(xí)方法在許多領(lǐng)域取得長足進(jìn)步,但是面對大部分?jǐn)?shù)學(xué)任務(wù)仍然束手無策。

主要原因是，翻譯人類證明樣本到機(jī)器可驗(yàn)證的格式是極其耗時、耗力的，這在幾何證明中尤其突出,翻譯難度加大導(dǎo)致了嚴(yán)重的數(shù)據(jù)稀缺。

AlphaGeometry通過大規(guī)模隨機(jī)生成幾何定理和相應(yīng)的證明，來解決數(shù)據(jù)稀疏的問題,產(chǎn)生了上億組訓(xùn)練數(shù)據(jù)。

具體來說,AlphaGeometry 首先使用圖形構(gòu)建語言隨機(jī)生成大量候選定理陳述,然后利用符號演繹引擎(如演繹數(shù)據(jù)庫 DD)推導(dǎo)出所有可能的新結(jié)論,遞歸地回溯每個新結(jié)論所依賴的前提,提取出最小依賴集作為該定理的證明。

為了擴(kuò)大證明的范圍,除了純符號演繹,該方法還通過代數(shù)推理引擎新增了許多依賴代數(shù)操作的證明步驟。最終，得到了大約1億組合成的定理證明訓(xùn)練數(shù)據(jù)。

在獲得大規(guī)模訓(xùn)練數(shù)據(jù)后,AlphaGeometry使用 Transformer 大語言模型進(jìn)行預(yù)訓(xùn)練,學(xué)習(xí)預(yù)測證明的序列。

此外,它還進(jìn)行了針對性微調(diào),集中優(yōu)化輔助構(gòu)造的生成。以解決幾何證明中一個關(guān)鍵難題,定理證明中的外生項(xiàng)生成問題。

在實(shí)際應(yīng)用時,AlphaGeometry采用了交互式的神經(jīng)符號框架。簡單來說,大語言模型會首先生成一組輔助構(gòu)造候選,然后符號引擎基于新構(gòu)造判斷定理是否得證。

如果仍未成功,則迭代上述流程,語言模型會在更豐富的上下文中生成新的輔助構(gòu)造候選。

這個框架設(shè)計(jì)的非常巧妙,大語言模型負(fù)責(zé)開拓解空間,提出新的假設(shè),而符號引擎則保證精確正確的推理。完美地結(jié)合神經(jīng)網(wǎng)絡(luò)的創(chuàng)造力和符號系統(tǒng)的解釋性、精確性。

AlphaGeometry基本解決了幾何定理證明領(lǐng)域數(shù)據(jù)稀疏的關(guān)鍵難題,開創(chuàng)了不依賴人類證明示例、利用合成數(shù)據(jù)訓(xùn)練AI模型的創(chuàng)新方法。

本文素材來源AlphaGeometry論文，如有侵權(quán)請聯(lián)系刪除

繼續(xù)閱讀：

未經(jīng)允許不得轉(zhuǎn)載：RPA中國 | RPA全球生態(tài) | 數(shù)字化勞動力 | RPA新聞 | 推動中國RPA生態(tài)發(fā)展 | 流 > 大模型獨(dú)立解答30道國際奧數(shù)難題，能力接近金牌選手！