用形式化验证让AI生成的代码真正正确，解决幻觉问题。
From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification
- 通过Dafny验证器迭代反馈，引导LLM自修正生成代码。
- Gemma 4-31B在复杂算法上达到90.91%验证成功率。
- 适合想提升AI编程可靠性的开发者和研究者。
大型语言模型（LLMs）在自动化软件工程中展现出潜力，但其生成代码的正确性常因错误或幻觉而受损。为强制模型输出真实代码，需结合形式化规范并由数学验证器证明其正确性。然而，从自然语言到精确形式规范的转换仍具挑战。本文提出NL2VC-60数据集，包含60个复杂算法问题。我们在7个开源大模型上评估了11个问题集，采用分层提示策略：无上下文提示、提供结构锚点的签名提示，以及利用Dafny验证器反馈进行迭代自修复的提示。为防止空验证（即模型用平凡规范骗过验证器），引入uDebug平台进行功能验证。结果表明，无上下文提示几乎全失败；而引入结构签名和自修复机制后，性能显著提升。其中，Gemma 4-31B达到90.91%的验证成功，GPT-OSS 120B从0提升至81.82%。这表明开源大模型已具备形式化验证能力，可作为高可信软件开发的有力助手。
原文摘要 · Abstract (English)
Large Language Models (LLMs) show promise in automated software engineering, yet their guarantee of correctness is frequently undermined by erroneous or hallucinated code. To enforce model honesty, formal verification requires LLMs to synthesize implementation logic alongside formal specifications that are subsequently proven correct by a mathematical verifier. However, the transition from informal natural language to precise formal specification remains an arduous task. Our work addresses this by providing the NaturalLanguage2VerifiedCode (NL2VC)-60 dataset: a collection of 60 complex algorithmic problems. We evaluate 11 randomly selected problem sets across seven open-weight LLMs using a tiered prompting strategy: contextless prompts, signature prompts providing structural anchors, and self-healing prompts utilizing iterative feedback from the Dafny verifier. To address vacuous verification, where models satisfy verifiers with trivial specifications, we integrate the uDebug platform to ensure functional validation. Our results show that while contextless prompting leads to near-universal failure, structural signatures and iterative self-healing facilitate a dramatic performance turnaround. Specifically, Gemma 4-31B achieved a 90.91\% verification success rate, while GPT-OSS 120B rose from zero to 81.82\% success with signature-guided feedback. These findings indicate that formal verification is now attainable for open-weight LLMs, which serve as effective apprentices for synthesizing complex annotations and facilitating high-assurance software development.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。