Baldur: Whole-Proof Generation and Repair with Large Language Models
Baldur: Whole-Proof Generation and Repair with Large Language Models
复制标题
DOI：
10.1145/3611643.3616243
复制
发表时间：
2023-03
期刊：
影响因子：
--
通讯作者：
E. First;M. Rabe;T. Ringer;Yuriy Brun
中科院分区：
文献类型：
--
作者：
E. First;M. Rabe;T. Ringer;Yuriy Brun
正式验证软件是一项非常理想但劳动密集型的任务。最近的工作开发了使用证明助手（例如Coq和Isabelle/Hol）自动验证正式验证的方法，例如，通过训练模型一次预测一个证明步骤，并使用该模型搜索可能的证明空间。本文介绍了一种自动化正式验证的新方法：我们使用大型语言模型，对自然语言和代码进行了培训，并对证明进行了微调，以一次生成全部证明。然后，我们证明了一个微调修复生成的证据的模型进一步增加了证明能力。本文：（1）证明了使用变压器的全能生成是可能的，并且比基于搜索的技术有效但更有效。 （2）证明，为学习的模型提供其他上下文，例如先前的失败的证明尝试和随后的错误消息，导致证明修复以进一步改善自动证明的生成。 （3）与先前的工作一起建立了一种新的技术状态，用于全自动证明综合。我们在原型（Baldur）中对方法进行了验证，并以6,336个isabelle/hol定理的基准进行评估，并进行了证明，从经验上显示了全部隔离生成，修复和附加背景的有效性。我们还表明，Baldur通过自动生成8.7％定理的证明来补充最先进的工具Thor。 Baldur和Thor一起可以自动证明65.7％的定理。本文为使用大型语言模型自动进行正式验证的新研究铺平了道路。
Formally verifying software is a highly desirable but labor-intensive task. Recent work has developed methods to automate formal verification using proof assistants, such as Coq and Isabelle/HOL, e.g., by training a model to predict one proof step at a time and using that model to search through the space of possible proofs. This paper introduces a new method to automate formal verification: We use large language models, trained on natural language and code and fine-tuned on proofs, to generate whole proofs at once. We then demonstrate that a model fine-tuned to repair generated proofs further increasing proving power. This paper: (1) Demonstrates that whole-proof generation using transformers is possible and is as effective but more efficient than search-based techniques. (2) Demonstrates that giving the learned model additional context, such as a prior failed proof attempt and the ensuing error message, results in proof repair that further improves automated proof generation. (3) Establishes, together with prior work, a new state of the art for fully automated proof synthesis. We reify our method in a prototype, Baldur, and evaluate it on a benchmark of 6,336 Isabelle/HOL theorems and their proofs, empirically showing the effectiveness of whole-proof generation, repair, and added context. We also show that Baldur complements the state-of-the-art tool, Thor, by automatically generating proofs for an additional 8.7% of the theorems. Together, Baldur and Thor can prove 65.7% of the theorems fully automatically. This paper paves the way for new research into using large language models for automating formal verification.