加州理工華人用AI顛覆數學證明！提速5倍震驚陶哲軒，80%數學步驟全自動化

AIGC動態歡迎閱讀

原標題：加州理工華人用AI顛覆數學證明！提速5倍震驚陶哲軒，80%數學步驟全自動化
關鍵字：策略,定理,前提,目標,報告
文章來源：新智元
內容字數：13184字

內容摘要：

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

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

聯系作者

文章來源：新智元
作者微信：AI_era
作者簡介：智能+中國主平臺，致力于推動中國從互聯網+邁向智能+新紀元。重點關注人工智能、機器人等前沿領域發展，關注人機融合、人工智能和機器人對人類社會與文明進化的影響，領航中國新智能時代。