Baldur：基于大语言模型的完整证明生成与修复
机器学习
2023-03-17 v2 计算机科学中的逻辑
软件工程
摘要
形式化验证软件属性是一项极受青睐但劳动密集的任务。近期工作已开发出使用证明助手（如 Coq 和 Isabelle/HOL）自动化形式化验证的方法，例如训练模型一次预测一个证明步骤，并利用该模型在可能证明的空间中搜索。本文提出一种自动化形式化验证的新方法：我们使用在自然语言文本和代码上训练并微调于证明的大语言模型，一次性为定理生成完整证明，而非逐步生成。我们将该证明生成模型与微调的修复模型相结合，以修复生成的证明，进一步提升证明能力。本文的主要贡献首次证明了：(1) 使用 transformer 的整证明生成是可行的，且与基于搜索的技术同样有效，而无需代价高昂的搜索。(2) 为学习到的模型提供额外上下文（如先前的失败证明尝试及随之产生的错误信息）可实现证明修复，并进一步改进自动化证明生成。(3) 我们确立了全自动证明合成的新 state of the art。我们将方法实现为原型 Baldur，并在包含 6,336 个 Isabelle/HOL 定理及其证明的基准上评估。除经验性展示整证明生成、修复与附加上下文的有效性外，我们表明 Baldur 相较 SOTA 工具 Thor 自动为多 8.7% 的定理生成了证明。Baldur 与 Thor 结合可全自动证明 65.7% 的定理。本文为使用大语言模型自动化形式化验证的新研究铺平了道路。
引用
@article{arxiv.2303.04910,
title = {Baldur: Whole-Proof Generation and Repair with Large Language Models},
author = {Emily First and Markus N. Rabe and Talia Ringer and Yuriy Brun},
journal= {arXiv preprint arXiv:2303.04910},
year = {2023}
}