让代码、断言和证明同步生成，实现可验证的编程新范式。
WybeCoder: Verified Imperative Code Generation
- 通过代码、断言与证明协同演化，构建可验证的智能编程框架。
- 在堆排序等复杂算法上生成上百行已验证代码，解决以往方法的性能瓶颈。
- 适合研究形式化验证与自动化编程的开发者，推动可信软件工程发展。
大型语言模型在自动代码生成和形式化定理证明方面取得显著进展，但软件验证尚未获得同等提升。为此，我们提出 WybeCoder，一种代理式代码验证框架，支持‘边写边证’的开发模式，使代码、不变量与证明共同演化。该框架基于结合自动验证条件生成、SMT求解与 Lean 中交互式证明的最新技术。为实现系统评估，我们将两个用于 Lean 中函数式验证的基准测试集 Verina 与 Clever 转换为等价的指令式代码规范。在堆排序等复杂算法上，随着方法扩展，我们持续观察到性能提升，成功合成数十个有效不变量，处理数十个子目标，最终生成数百行已验证代码，突破了先前工作中的性能瓶颈。最优系统在中等计算预算下解决了 74% 的 Verina 任务和 62% 的 Clever 任务，显著超越此前评估结果，为大规模已验证指令式代码数据集的自动化构建铺平道路。
原文摘要 · Abstract (English)
Recent progress in large language models (LLMs) has substantially advanced automatic code generation and formal theorem proving, yet software verification has not seen comparable gains. To address this gap, we propose WybeCoder, an agentic code verification framework that enables prove-as-you-generate development, in which code, invariants, and proofs co-evolve. WybeCoder builds on a recent framework that combines automatic verification condition generation and SMT solving with interactive proofs in Lean. To enable systematic evaluation, we translate two benchmarks for functional verification in Lean, Verina and Clever, into equivalent imperative code specifications. On complex algorithms such as Heapsort, we observe consistent performance improvements as we scale our approach, synthesizing dozens of valid invariants and dispatching dozens of subgoals, ultimately producing hundreds of lines of verified code and overcoming plateaus reported in previous work. Our best system solves 74% of Verina tasks and 62% of Clever tasks at moderate compute budgets, substantially surpassing previous evaluations and paving the way for the automated construction of large-scale datasets of verified imperative code.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。