陶哲轩看了都直呼内行！谷歌等用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自动证明定理拿顶会杰出论文，上下文越全证得越好