Rango用动态检索增强，自动帮Coq写证明，效率比之前高29%。
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
- 每步推理时自动检索相关定理和证明，动态更新上下文。
- 在新数据集上证明32.0%的定理，比SOTA工具多29%。
- 适合需要自动化验证的开源项目开发者使用。
使用证明助手（如Coq）进行形式化验证可生成高质量软件，但过程需大量专业知识与人工投入。近期研究尝试用机器学习和大语言模型（LLMs）自动化证明生成，发现识别相关前提（如引理、定义）有助于合成。本文提出Rango，一个完全自动化的Coq证明合成工具，能自动识别当前项目中的相关前提及相似证明，并在合成过程中使用检索增强。Rango在每个证明步骤中对细调后的LLM进行检索增强，动态适应项目和证明进展。我们构建了新数据集CoqStoq，包含2,226个GitHub开源Coq项目和196,929个定理，涵盖训练数据与精选评估基准。在该基准上，Rango成功合成32.0%的定理，比先前最先进工具Tactician多出29%。评估还显示，引入相关证明使证明数量提升47%。
原文摘要 · Abstract (English)
Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual effort to write proofs. Recent work has explored automating proof synthesis using machine learning and large language models (LLMs). This work has shown that identifying relevant premises, such as lemmas and definitions, can aid synthesis. We present Rango, a fully automated proof synthesis tool for Coq that automatically identifies relevant premises and also similar proofs from the current project and uses them during synthesis. Rango uses retrieval augmentation at every step of the proof to automatically determine which proofs and premises to include in the context of its fine-tuned LLM. In this way, Rango adapts to the project and to the evolving state of the proof. We create a new dataset, CoqStoq, of 2,226 open-source Coq projects and 196,929 theorems from GitHub, which includes both training data and a curated evaluation benchmark of well-maintained projects. On this benchmark, Rango synthesizes proofs for 32.0% of the theorems, which is 29% more theorems than the prior state-of-the-art tool Tactician. Our evaluation also shows that Rango adding relevant proofs to its context leads to a 47% increase in the number of theorems proven.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。