大型语言模型可通过为定理生成整个证明和修复定理来实现形式验证自动化，实现了最先进的性能，无需昂贵的搜索。

Baldur: Whole-Proof Generation and Repair with Large Language Models

E First, M N. Rabe, T Ringer, Y Brun
[University of Massachusetts & Google & University of Illinois Urbana-Champaign]

  1. 使用 transformer 的整体证明生成与基于搜索的技术一样有效，而不需要昂贵的搜索；

  2. 为习得的模型提供额外的上下文，如失败的证明尝试和错误信息，改善了证明修复，进一步提高了自动证明生成；

  3. Baldur 是一种使用 LLM 生成整个形式化证明的新方法，当与之前的技术相结合时，改善了定理证明的最先进水平；

  4. 本文工作为使用 LLM 进行自动定理证明和修复方法，以及在证明生成中使用上下文开辟了新的研究途径。

https://arxiv.org/abs/2303.04910 

图片
图片
图片
图片

内容中包含的图片若涉及版权问题，请及时与我们联系删除