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

大语言模型（LLMs）在自动化软件工程领域展现出广阔前景，但其生成代码的正确性却常因错误或“幻觉”（hallucinated）内容而难以保障。为促使模型“诚实”输出，形式化验证要求LLM不仅生成实现逻辑，还需同步产出形式化规约（formal specification），再由数学验证器（mathematical verifier）对二者进行严格证明。然而，从非形式化的自然语言描述到精确、无歧义的形式化规约之间的转化，始终是一项艰巨挑战。为此，本研究构建了NaturalLanguage2VerifiedCode（NL2VC）-60数据集：该数据集包含60道复杂算法问题，每道题均配备自然语言描述、形式化规约及经Dafny验证器确认正确的参考实现。我们选取其中11个问题集，在7种开源权重LLM上开展系统性评估，并采用分层提示策略：第一层为无上下文提示（contextless prompts），第二层为带函数签名的提示（signature prompts），通过提供结构化锚点（structural anchors）引导模型理解接口与约束；第三层为自修复提示（self-healing prompts），即利用Dafny验证器的迭代反馈驱动模型反复修正规约与代码。为防止“空洞验证”（vacuous verification）——即模型通过编写过于平凡（如恒真）的规约来“欺骗”验证器——我们进一步集成uDebug平台，对生成代码执行功能性测试（functional validation），确保其行为符合预期语义。实验结果表明：无上下文提示几乎全面失效；而引入结构化签名与基于验证反馈的迭代自修复机制后，模型性能实现显著跃升。具体而言，Gemma 4-31B模型达到了90.91%的形式验证通过率；GPT-OSS 120B模型则在签名引导式反馈的支持下，验证成功率从0%大幅提升至81.82%。这些发现表明：形式化验证目前已切实可行地应用于开源权重LLM，使其能够胜任高可靠软件开发中复杂规约与注解的协同合成任务，成为值得信赖的“数字学徒”（effective apprentices）。

如何让开源大语言模型（LLMs）在自动软件工程中生成既功能正确又形式可验证的代码，克服其易产生幻觉、缺乏形式规范能力、以及难以将非正式自然语言需求转化为精确形式规约的根本挑战。

提出NL2VC-60基准与三层渐进式提示策略（contextless → signature-guided → self-healing with Dafny feedback），首次系统性地将形式验证闭环（Dafny证明器）与功能验证闭环（uDebug测试平台）协同嵌入LLM代码生成流程，强制模型‘诚实’输出可证正确且行为等价的代码-规约对，而非仅满足语法或空洞规约的虚假验证。

构建首个面向形式验证的高质量算法级基准NL2VC-60（60个复杂、手工验证的算法问题）；引入uDebug功能验证机制，有效识别并过滤‘vacuous verification’（如spec trivially true）；在7个开源LLM上实证验证：Gemma-4-31B达90.91%验证通过率，GPT-OSS-120B从0%跃升至81.82%；所有prompting策略、评估脚本及NL2VC-60数据集已开源；工作揭示结构化锚点（signature）和迭代自修复是解锁开源LLM高保证代码合成能力的关键杠杆。

‘Code Generation with Formal Specifications: A Survey’ (ICSE’24); ‘VeriCode: End-to-End Verification-Aware Code Generation’ (NeurIPS’23); ‘DafnyGen: Prompting LLMs for Verified Dafny Programs’ (PLDI’24); ‘SpecSynth: Learning to Generate Coq Specifications from Code’ (ACL’23); ‘Test-Time Verification for LLM-Generated Code’ (ICML’24)