WybeCoder: Verified Imperative Code Generation

📄 arXiv: 2603.29088v1 📥 PDF

作者: Fabian Gloeckle, Mantas Baksys, Darius Feher, Kunhao Zheng, Amaury Hayat, Sean B. Holden, Gabriel Synnaeve, Peter O'Hearn

分类: cs.SE, cs.AI

发布日期: 2026-03-31

💡 一句话要点

提出WybeCoder，实现指令式代码生成过程中的同步验证，提升代码质量。

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

关键词: 代码生成 软件验证 形式化证明 大型语言模型 指令式编程

📋 核心要点

  1. 现有软件验证方法在自动代码生成方面存在不足，难以实现代码生成与验证的同步进行。
  2. WybeCoder通过agentic框架，结合自动验证条件生成、SMT求解器和交互式证明，实现代码、不变量和证明的协同演化。
  3. 实验结果表明，WybeCoder在复杂算法上表现出持续的性能提升，并在Verina和Clever基准测试中显著超越了现有方法。

📝 摘要（中文）

大型语言模型（LLMs）在自动代码生成和形式化定理证明方面取得了显著进展，但软件验证领域的提升相对滞后。为了弥补这一差距，我们提出了WybeCoder，一个agentic代码验证框架，支持在代码生成的同时进行验证，实现代码、不变量和证明的协同演化。该框架基于自动验证条件生成和SMT求解器，并结合Lean中的交互式证明。为了进行系统评估，我们将Lean中用于函数验证的两个基准数据集Verina和Clever转换为等效的指令式代码规范。在诸如Heapsort等复杂算法上，我们观察到通过扩展我们的方法，能够持续提升性能，合成数十个有效的循环不变式并处理数十个子目标，最终生成数百行经过验证的代码，克服了先前工作中报告的性能瓶颈。在适度的计算预算下，我们最好的系统解决了74%的Verina任务和62%的Clever任务，显著超越了之前的评估结果，为自动构建大规模的经过验证的指令式代码数据集铺平了道路。

🔬 方法详解

问题定义：现有方法在自动代码生成过程中，软件验证的自动化程度较低，难以保证生成代码的正确性。尤其是在指令式编程范式下，循环不变式等关键信息的自动推导和验证仍然面临挑战，导致软件验证效率低下且容易出错。

核心思路：WybeCoder的核心思路是在代码生成过程中同步进行验证，将代码生成、不变量推导和形式化证明紧密结合。通过agentic框架，利用大型语言模型生成代码片段，并使用自动验证工具和SMT求解器验证其正确性，同时允许交互式证明来处理复杂情况。这种协同演化的方式能够更有效地发现和修复代码中的错误，提高代码质量。

技术框架：WybeCoder框架包含以下主要模块：1) 代码生成器：使用大型语言模型生成指令式代码片段。2) 验证条件生成器：自动生成验证代码正确性的条件。3) SMT求解器：自动求解验证条件，判断代码是否满足规范。4) 交互式证明环境：允许人工干预，辅助完成复杂的证明过程。5) 循环不变式推导器：自动推导循环不变式，用于验证循环结构的正确性。整个流程是一个迭代过程，代码生成、验证和证明相互促进，共同演化。

关键创新：WybeCoder的关键创新在于其agentic代码验证框架，实现了代码生成与验证的紧密集成。与传统的先生成代码再进行验证的方法不同，WybeCoder在代码生成的同时进行验证，能够及早发现和修复错误，避免错误累积。此外，WybeCoder还结合了自动验证和交互式证明，充分利用了自动化工具和人工专家的优势。

关键设计：WybeCoder的关键设计包括：1) 使用Lean作为交互式证明环境，提供强大的形式化证明能力。2) 将Verina和Clever等函数式验证基准转换为指令式代码规范，方便系统评估。3) 设计合适的提示工程，引导大型语言模型生成符合规范的代码。4) 采用有效的循环不变式推导算法，提高验证效率。5) 通过实验评估不同计算预算下的性能表现，优化系统配置。

📊 实验亮点

WybeCoder在Verina和Clever基准测试中取得了显著的性能提升，分别解决了74%和62%的任务，超越了之前的评估结果。在Heapsort等复杂算法上，WybeCoder能够生成数百行经过验证的代码，克服了先前工作中报告的性能瓶颈，表明其在处理复杂软件验证问题方面的潜力。

🎯 应用场景

WybeCoder具有广泛的应用前景，可用于开发高质量、高可靠性的软件系统，尤其是在安全攸关的领域，如操作系统、嵌入式系统和金融系统。该研究成果有助于提高软件开发的自动化程度，降低开发成本，并减少软件缺陷，从而提升软件质量和安全性。

📄 摘要（原文）

Recent progress in large language models (LLMs) has advanced automatic code generation and formal theorem proving, yet software verification has not seen the same improvement. To address this gap, we propose WybeCoder, an agentic code verification framework that enables prove-as-you-generate development where code, invariants, and proofs co-evolve. It builds on a recent framework that combines automatic verification condition generation and SMT solvers with interactive proofs in Lean. To enable systematic evaluation, we translate two benchmarks for functional verification in Lean, Verina and Clever, to equivalent imperative code specifications. On complex algorithms such as Heapsort, we observe consistent performance improvements by scaling our approach, synthesizing dozens of valid invariants and dispatching of dozens of subgoals, resulting in hundreds of lines of verified code, overcoming plateaus reported in previous works. Our best system solves 74% of Verina tasks and 62% of Clever tasks at moderate compute budgets, significantly surpassing previous evaluations and paving a path to automated construction of large-scale datasets of verified imperative code.