From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification

📄 arXiv: 2604.22601v1 📥 PDF

作者: Md Erfan, Md Kamal Hossain Chowdhury, Ahmed Ryan, Md Rayhanur Rahman

分类: cs.SE, cs.AI

发布日期: 2026-04-24

备注: 16 pages

💡 一句话要点

提出NL2VC-60数据集，结合Dafny形式验证，提升LLM代码生成正确率。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式验证 代码生成 大型语言模型 Dafny NL2VC-60数据集

📋 核心要点

  1. 现有LLM代码生成易出错，缺乏形式验证保证，难以满足高可靠性软件需求。
  2. 提出NL2VC-60数据集，并结合分层提示策略与Dafny形式验证，提升代码生成质量。
  3. 实验表明，结构签名和迭代自修复提示能显著提高LLM的代码验证成功率。

📝 摘要（中文）

大型语言模型(LLMs)在自动化软件工程中展现出潜力，但其正确性常因错误或幻觉代码而受损。为了保证模型的可靠性，形式验证要求LLMs生成实现逻辑以及形式规范，并通过数学验证器证明其正确性。然而，从非正式自然语言到精确形式规范的转换仍然是一项艰巨的任务。本文通过提供NaturalLanguage2VerifiedCode (NL2VC)-60数据集来解决这个问题，该数据集包含60个复杂的算法问题。我们使用分层提示策略（无上下文提示、提供结构锚点的签名提示以及利用Dafny验证器迭代反馈的自修复提示）在七个开放权重LLMs上评估了11个随机选择的问题集。为了解决空洞验证问题（模型使用简单的规范来满足验证器），我们集成了uDebug平台以确保功能验证。结果表明，虽然无上下文提示几乎导致完全失败，但结构签名和迭代自修复促进了性能的显著提升。具体而言，Gemma 4-31B实现了90.91%的验证成功率，而GPT-OSS 120B在签名引导反馈下从零上升到81.82%的成功率。这些发现表明，形式验证现在对于开放权重LLMs是可行的，它们可以作为合成复杂注释和促进高保证软件开发的有效助手。

🔬 方法详解

问题定义：论文旨在解决大型语言模型（LLMs）在代码生成过程中出现的正确性问题。现有方法生成的代码容易出错，缺乏形式验证，难以保证软件的可靠性。特别是从自然语言描述到形式化规范的转换过程，对LLM来说是一个巨大的挑战。

核心思路：论文的核心思路是利用形式验证工具Dafny，结合精心设计的提示策略，引导LLM生成既满足功能需求，又能通过形式验证的代码。通过迭代反馈，不断修正LLM生成的代码和规范，最终得到高可靠性的软件。

技术框架：整体框架包含以下几个主要阶段：1) 使用NL2VC-60数据集，该数据集包含自然语言描述的算法问题和对应的形式化规范。2) 采用分层提示策略，包括无上下文提示、签名提示（提供函数签名等结构信息）和自修复提示（利用Dafny验证器的反馈进行迭代修正）。3) 使用Dafny验证器对生成的代码进行形式验证。4) 集成uDebug平台进行功能验证，防止模型生成空洞的、看似正确但实际无意义的代码。

关键创新：最重要的创新点在于将形式验证工具Dafny与LLM的代码生成过程相结合，通过迭代反馈机制，引导LLM生成可验证的代码。此外，NL2VC-60数据集的构建以及分层提示策略的设计，也为LLM在形式验证领域的应用提供了有力的支持。与现有方法相比，该方法能够显著提高代码的正确性和可靠性。

关键设计：分层提示策略是关键设计之一。签名提示通过提供函数签名等结构信息，引导LLM生成符合规范的代码框架。自修复提示则利用Dafny验证器的反馈信息，迭代修正LLM生成的代码和规范，直至通过验证。uDebug的集成用于功能验证，确保生成的代码不仅在形式上正确，而且在功能上也能满足需求。

📊 实验亮点

实验结果表明，在NL2VC-60数据集上，通过结构签名和迭代自修复提示，Gemma 4-31B模型达到了90.91%的验证成功率，GPT-OSS 120B模型从0%提升至81.82%。这些结果表明，开放权重LLMs在形式验证方面具有巨大的潜力，能够生成高质量、可验证的代码。

🎯 应用场景

该研究成果可应用于自动化软件开发、安全关键系统、智能合约等领域。通过形式验证保证代码的正确性，可以显著降低软件缺陷率，提高软件系统的可靠性和安全性。未来，该技术有望应用于更广泛的软件工程领域，实现AI辅助的高可靠性软件开发。

📄 摘要（原文）

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.