陶哲軒看了都直呼內行！谷歌等用LLM自動證明定理拿頂會杰出論文，上下文越全證得越好

AIGC動態歡迎閱讀

原標題：陶哲軒看了都直呼內行！谷歌等用LLM自動證明定理拿頂會杰出論文，上下文越全證得越好
關鍵字：模型,定理,上下文,研究人員,錯誤
文章來源：新智元
內容字數：5915字

內容摘要：

新智元報道編輯：alan
【新智元導讀】在軟件工程頂會ESEC/FSE上，來自馬薩諸塞大學、谷歌和伊利諾伊大學厄巴納-香檳分校（UIUC）的研究人員發表了新的成果，使用LLM解決自動化定理證明問題。Transformer的技能樹是越來越厲害了。
來自馬薩諸塞大學、谷歌和伊利諾伊大學厄巴納-香檳分校（UIUC）的研究人員發表了一篇論文，利用大語言模型自動生成定理的完整證明。
論文地址：https://arxiv.org/pdf/2303.04910.pdf
這篇工作以Baldur（北歐神話中雷神Thor的兄弟）命名，首次證明了使用Transformer生成全證明是可能的，并且當為模型提供額外的上下文時，還可以改進模型先前的證明。
文章發表于2023年12月在舊金山舉行的ESEC/FSE（ACM歐洲軟件工程聯合會議和軟件工程基礎研討會）上，并獲得了杰出論文獎（Distinguished Paper award）。
眾所周知，軟件存在bug（廢話），這在一般應用程序或者網站上問題不大，但對于比如加密協議、醫療設備和航天飛機等關鍵系統背后的軟件而言，必須確保沒有錯誤。
——一般的代碼審查和測

原文鏈接：陶哲軒看了都直呼內行！谷歌等用LLM自動證明定理拿頂會杰出論文，上下文越全證得越好

聯系作者

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