从自然语言到经过验证的代码：通过基于 Dafny 的形式验证实现人工智能辅助问题到代码生成

大语言模型 (LLM) 在自动化软件工程中展现了前景，但它们对正确性的保证经常被错误或幻觉代码破坏。为了加强模型的诚实性，形式验证需要 LLM 综合实现逻辑以及随后由数学验证者证明正确的形式规范。然而，从非正式的自然语言到精确的形式化规范的转变仍然是一项艰巨的任务。我们的工作通过提供 NaturalLanguage2VerifiedCode (NL2VC)-60 数据集来解决这个问题：60 个复杂算法问题的集合。我们使用分层提示策略评估 7 个开放权重 LLM 中随机选择的 11 个问题集：无上下文提示、提供结构锚点的签名提示以及利用来自 Dafny 验证器的迭代反馈的自我修复提示。为了解决模型通过琐碎规范满足验证者的空洞验证问题，我们集成了 uDebug 平台以确保功能验证。我们的结果表明，虽然无背景的提示会导致几乎普遍的失败，但结构特征和迭代的自我修复促进了戏剧性的绩效转变。具体来说，Gemma 4-31B 实现了 90.91% 的验证成功率，而 GPT-OSS 120B 通过签名引导反馈，成功率从零上升到 81.82%。这些发现表明，开放权重 LLM 现在可以实现形式验证，它可以作为合成复杂注释和促进高保证软件开发的有效学徒。