清華校友用AI162個高數定理，智能體LeanAgent攻克困擾陶哲軒難題！

AIGC動態歡迎閱讀

原標題：清華校友用AI162個高數定理，智能體LeanAgent攻克困擾陶哲軒難題！
關鍵字：定理,代碼,可塑性,數據,數學
文章來源：新智元
內容字數：0字

內容摘要：

新智元報道編輯：編輯部 HYZ
【新智元導讀】就在剛剛，清華校友用AI證明了162個未被人類證明的數學定理，解決了AI無法解決陶哲軒對多項式Freiman-Ruzsa猜想的形式化難題！諾貝爾物理學獎和化學獎被AI「包圓」后，人們再次確信：基礎科學研究的范式，已經被AI從根本上改變。
果然，就在剛剛，AI成功證明了162個以前未被證明的數學定理，再次印證了這一點。
到目前為止，LLM仍然是靜態的，無法在線學習新知識，更別提證明高數定理了。
對此，來自加州理工、斯坦福和威大的研究人員提出了LeanAgent——一個終身學習，并能證明定理的AI智能體。
論文地址：https://arxiv.org/abs/2410.06209
LeanAgent會根據數學難度優化的學習軌跡課程，來提高學習策略。并且，它還有一個動態數據庫，有效管理不斷擴展的數學知識。
值得一提的是，整個學習過程中，它既能自我學習新知識，同時不會遺忘已具備的能力。
實驗結果發現，LeanAgent從來自23個不同Lean代碼庫中，成功證明162個此前未被人類證明的數學定理。
相較于基于Lean數據微調大模型，LeanAgen

原文鏈接：清華校友用AI162個高數定理，智能體LeanAgent攻克困擾陶哲軒難題！

聯系作者

文章來源：新智元
作者微信：
作者簡介：