AIGC動(dòng)態(tài)歡迎閱讀

原標(biāo)題：清華校友用AI162個(gè)高數(shù)定理，智能體LeanAgent攻克困擾陶哲軒難題！
關(guān)鍵字：定理,代碼,可塑性,數(shù)據(jù),數(shù)學(xué)
文章來(lái)源：新智元
內(nèi)容字?jǐn)?shù)：0字

內(nèi)容摘要：

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

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

聯(lián)系作者

文章來(lái)源：新智元
作者微信：
作者簡(jiǎn)介：