用自迭代翻译与验证反馈，让大模型生成可数学证明正确的代码。
AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement
- 通过树搜索算法结合验证器反馈，自动优化生成代码
- 无需人工干预即可在HumanEval和MBPP上生成经验证的正确代码
- 适合追求高可靠性的自动化编程系统研究者
大型语言模型在自动化代码生成方面取得显著进展，但生成代码的正确性无法保证。本文旨在通过形式化验证为生成代码提供数学层面的正确性保障。然而，由于训练数据稀缺和形式化证明复杂，现有方法受限。为此，我们提出AlphaVerus框架，通过迭代式将程序从高资源语言翻译至目标语言，并利用验证器反馈实现自我改进。该框架包含三个阶段：候选翻译探索、Treefinement——一种基于验证反馈的新型树搜索程序优化算法，以及过滤不匹配规范与代码以防止奖励劫持。通过这一循环过程，仅使用未微调的LLaMA-3.1-70B模型即可实现无监督生成形式化验证的代码。AlphaVerus在HumanEval与MBPP基准上展现出生成经验证正确解的能力，为构建真正可信的代码生成代理奠定基础。
原文摘要 · Abstract (English)
Automated code generation with large language models has gained significant traction, but there remains no guarantee on the correctness of generated code. We aim to use formal verification to provide mathematical guarantees that the generated code is correct. However, generating formally verified code with LLMs is hindered by the scarcity of training data and the complexity of formal proofs. To tackle this challenge, we introduce AlphaVerus, a self-improving framework that bootstraps formally verified code generation by iteratively translating programs from a higher-resource language and leveraging feedback from a verifier. AlphaVerus operates in three phases: exploration of candidate translations, Treefinement -- a novel tree search algorithm for program refinement using verifier feedback, and filtering misaligned specifications and programs to prevent reward hacking. Through this iterative process, AlphaVerus enables a LLaMA-3.1-70B model to generate verified code without human intervention or model finetuning. AlphaVerus shows an ability to generate formally verified solutions for HumanEval and MBPP, laying the groundwork for truly trustworthy code-generation agents.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。