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

原標(biāo)題：加州理工華人用AI顛覆數(shù)學(xué)證明！提速5倍震驚陶哲軒，80%數(shù)學(xué)步驟全自動化
關(guān)鍵字：策略,定理,前提,目標(biāo),報(bào)告
文章來源：新智元
內(nèi)容字?jǐn)?shù)：13184字

內(nèi)容摘要：

新智元報(bào)道編輯：編輯部
【新智元導(dǎo)讀】讓陶哲軒大神贊不絕口的形式化研究神器Lean，運(yùn)行LLM的推理卻有個(gè)bug。最近，加州理工團(tuán)隊(duì)解決了這個(gè)bug，把80%以上的數(shù)學(xué)證明步驟，都自動化了！Lean Copilot，讓陶哲軒等眾多數(shù)學(xué)家贊不絕口的這個(gè)形式化數(shù)學(xué)工具，又有超強(qiáng)進(jìn)化了？
就在剛剛，加州理工教授Anima Anandkumar宣布，團(tuán)隊(duì)發(fā)布了Lean Copilot論文的擴(kuò)展版本，并且更新了代碼庫。
論文地址：https://arxiv.org/pdf/2404.12534.pdf
最新實(shí)驗(yàn)表明，這個(gè)Copilot工具，可以自動化80%以上的數(shù)學(xué)證明步驟了！這個(gè)紀(jì)錄，比以前的基線aesop還要好2.3倍。
并且，和以前一樣，它在MIT許可下是開源的。
而對此做出巨大貢獻(xiàn)的，是一位華人小哥宋沛洋，他是UCSB的榮譽(yù)CS本科生，加州理工學(xué)院計(jì)算+數(shù)學(xué)科學(xué)（CMS）系的SURF研究員。
網(wǎng)友驚呼：所以，陶哲軒現(xiàn)在的數(shù)學(xué)研究可以原地加速5倍了？
LLM提出證明策略，人類無縫干預(yù)團(tuán)隊(duì)就發(fā)布了這個(gè)Lean Copilot的工具，希望啟動人類和LLM的協(xié)作，編寫出100%準(zhǔn)確的形式化數(shù)學(xué)

原文鏈接：加州理工華人用AI顛覆數(shù)學(xué)證明！提速5倍震驚陶哲軒，80%數(shù)學(xué)步驟全自動化

聯(lián)系作者

文章來源：新智元
作者微信：AI_era
作者簡介：智能+中國主平臺，致力于推動中國從互聯(lián)網(wǎng)+邁向智能+新紀(jì)元。重點(diǎn)關(guān)注人工智能、機(jī)器人等前沿領(lǐng)域發(fā)展，關(guān)注人機(jī)融合、人工智能和機(jī)器人對人類社會與文明進(jìn)化的影響，領(lǐng)航中國新智能時(shí)代。