Automated Proof Generation for Rust Code via Self-Evolution
作者: Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu K Lahiri, Tao Xie, Lidong Zhou
分类: cs.SE, cs.AI
发布日期: 2024-10-21 (更新: 2025-04-15)
💡 一句话要点
SAFE：通过自进化提升LLM在Rust代码形式化验证中的自动证明生成能力
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 形式化验证 代码证明生成 大型语言模型 自进化学习 Rust编程语言
📋 核心要点
- 形式化验证是保证代码正确性的关键，但人工构建证明成本高昂，自动化程度低。
- SAFE框架通过数据合成和模型微调的自进化循环，提升模型自动生成代码证明的能力。
- 实验表明，SAFE显著优于GPT-4o，在Rust代码证明生成任务上取得了52.52%的准确率。
📝 摘要（中文）
代码生成的正确性至关重要。形式化验证能够提供明确的正确性保证，但证明构建需要大量的人工干预，因此迫切需要自动化。主要的障碍在于数据的严重缺乏——与代码片段相比，用于训练大型语言模型（LLM）的证明数据要少得多。本文提出了SAFE，一个克服人工编写证明数据不足的框架，旨在实现Rust代码的自动证明生成。SAFE建立了一个自进化循环，其中数据合成和微调协同工作，以增强模型的能力，并利用符号验证器来区分正确和不正确的证明。SAFE还重新利用大量合成的不正确证明来训练微调模型的自我调试能力，使其能够根据验证器的反馈修复不正确的证明。SAFE在效率和精度方面均优于GPT-4o。通过数万个合成证明和自我调试机制，我们将最初不熟悉形式化验证的开源模型的能力提升到可以自动编写Rust代码证明的水平。这一进步显著提高了性能，在人类专家设计的基准测试中达到了52.52%的准确率，远高于GPT-4o的14.39%。
🔬 方法详解
问题定义：论文旨在解决Rust代码形式化验证中自动生成证明的问题。现有方法，特别是基于大型语言模型的方法，面临着训练数据严重不足的挑战，因为人工编写的证明数据远少于代码数据。这限制了LLM在形式化验证领域的应用，使其难以生成正确的代码证明。
核心思路：SAFE的核心思路是建立一个自进化循环，通过自动合成大量的证明数据来弥补人工标注数据的不足。该循环利用符号验证器来区分正确和不正确的证明，并将这些数据用于微调LLM，从而提升其生成正确证明的能力。此外，SAFE还利用不正确的证明来训练模型的自我调试能力，使其能够根据验证器的反馈修复证明。
技术框架：SAFE框架包含两个主要阶段：数据合成和模型微调。在数据合成阶段，SAFE生成大量的Rust代码及其对应的潜在证明。然后，使用符号验证器验证这些证明的正确性，并将验证结果作为标签。在模型微调阶段，SAFE使用合成的数据集微调LLM，使其能够生成正确的证明。此外，SAFE还训练模型根据验证器的反馈进行自我调试，以修复不正确的证明。
关键创新：SAFE的关键创新在于其自进化循环和自我调试机制。自进化循环通过自动合成数据来克服数据稀缺问题，而自我调试机制则使模型能够从错误中学习，进一步提升其生成正确证明的能力。与传统的监督学习方法相比，SAFE能够更有效地利用数据，并显著提高模型的性能。
关键设计：SAFE的关键设计包括：1) 使用符号验证器作为自动标注器，生成大规模的训练数据；2) 设计自我调试机制，利用不正确的证明来提升模型的鲁棒性；3) 选择合适的LLM作为基础模型，并进行有效的微调。
🖼️ 关键图片
📊 实验亮点
SAFE在Rust代码证明生成任务上取得了显著的性能提升。在人类专家设计的基准测试中，SAFE达到了52.52%的准确率，远高于GPT-4o的14.39%。这表明SAFE能够有效地利用合成数据和自我调试机制，显著提升LLM在形式化验证领域的性能。
🎯 应用场景
SAFE框架可应用于各种需要形式化验证的软件开发场景，例如操作系统内核、嵌入式系统和安全关键型应用。通过自动生成代码证明，SAFE可以显著降低验证成本，提高软件的可靠性和安全性。未来，SAFE有望成为软件开发流程中的一个重要组成部分，帮助开发者构建更加健壮和可靠的软件系统。
📄 摘要（原文）
Ensuring correctness is crucial for code generation. Formal verification offers a definitive assurance of correctness, but demands substantial human effort in proof construction and hence raises a pressing need for automation. The primary obstacle lies in the severe lack of data-there is much fewer proofs than code snippets for Large Language Models (LLMs) to train upon. In this paper, we introduce SAFE, a framework that overcomes the lack of human-written proofs to enable automated proof generation of Rust code. SAFE establishes a self-evolving cycle where data synthesis and fine-tuning collaborate to enhance the model capability, leveraging the definitive power of a symbolic verifier in telling correct proofs from incorrect ones. SAFE also re-purposes the large number of synthesized incorrect proofs to train the self-debugging capability of the fine-tuned models, empowering them to fix incorrect proofs based on the verifier's feedback. SAFE demonstrates superior efficiency and precision compared to GPT-4o. Through tens of thousands of synthesized proofs and the self-debugging mechanism, we improve the capability of open-source models, initially unacquainted with formal verification, to automatically write proofs for Rust code. This advancement leads to a significant improvement in performance, achieving a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.