論文の概要: WybeCoder: Verified Imperative Code Generation
- arxiv url: http://arxiv.org/abs/2603.29088v1
- Date: Tue, 31 Mar 2026 00:06:44 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-01 15:25:02.952939
- Title: WybeCoder: Verified Imperative Code Generation
- Title（参考訳）: WybeCoder: 検証済みインペラティブコード生成
- Authors: Fabian Gloeckle, Mantas Baksys, Darius Feher, Kunhao Zheng, Amaury Hayat, Sean B. Holden, Gabriel Synnaeve, Peter O'Hearn,
- Abstract要約: WybeCoderはエージェントコード検証フレームワークである。
コード、不変性、そして証明が共進化する所で、証明・アズ・ユー・ジェネレーション開発を可能にする。
- 参考スコア（独自算出の注目度）: 22.401681809856896
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
- Abstract（参考訳）: 大規模言語モデル(LLM)の最近の進歩は、高度な自動コード生成と形式的定理の証明が進んでいるが、ソフトウェア検証は、同様の改善をみていない。
このギャップに対処するため、我々は、コード、不変量、および証明が共進化する所で、コード生成の証明を可能にするエージェントコード検証フレームワークであるWybeCoderを提案する。
自動検証条件生成とSMTソルバをリーンのインタラクティブな証明と組み合わせた,最近のフレームワークの上に構築されている。
体系的な評価を可能にするため、Lean、Verina、Cleverの2つの機能検証ベンチマークを同等の命令型コード仕様に変換する。
Heapsortのような複雑なアルゴリズムでは、我々のアプローチをスケールし、数十の有効な不変量を合成し、数十のサブゴールをディスパッチすることで一貫したパフォーマンス改善を観察する。
我々の最良のシステムは、適度な計算予算でVerinaタスクの74%とCleverタスクの62%を解決し、以前の評価を大幅に上回り、検証命令コードの大規模なデータセットの自動構築への道を開いた。
関連論文リスト
- Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification [34.98335927187393]
大規模言語モデル(LLM)は可塑性コードを生成することができるが、正確性には限界がある。
本稿では,Lean4における自動コード検証のための階層的証明検索フレームワークを提案する。
Goedel-Code-Prover-8Bは、分解と完了の両方のための単一の統一ポリシーです。
論文 参考訳（メタデータ） (2026-03-18T18:42:04Z) - Scaling Code-Assisted Chain-of-Thoughts and Instructions for Model Reasoning [65.20602712957725]
Cacoは、高品質で検証可能な多様な命令-CoT推論データの合成を自動化する新しいフレームワークである。
我々の研究は、人間の介入なしに自己持続的で信頼できる推論システムを構築するためのパラダイムを確立します。
論文 参考訳（メタデータ） (2025-10-05T07:59:24Z) - Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking [54.43083499412643]
言語モデルの生成能力をプロセス検証器と組み合わせたテストタイムアルゴリズムは、新しい推論能力を引き出すための有望なレバーを提供する。
提案手法は, 理論的に根拠付きバックトラックを用いて, 検証誤差に対して, 確実な堅牢性を実現するための新しいプロセス誘導型テスト時間サンプリングアルゴリズムであるVGBを導入する。
論文 参考訳（メタデータ） (2025-10-03T16:21:14Z) - AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction [32.14733357890831]
本稿では,高品質なSVAを自動的に生成する新しい統合フレームワークAssertCoderを提案する。
AssertCoderは、不均一な仕様フォーマットを解析するために、モダリティに敏感な事前処理を使用する。
このフレームワークは、アサーションの品質を評価するために、突然変異に基づく評価アプローチを取り入れている。
論文 参考訳（メタデータ） (2025-07-14T14:43:14Z) - VERINA: Benchmarking Verifiable Code Generation [46.582574591358735]
大規模言語モデル(LLM)は、ソフトウェア開発にますます統合されている。
LLM生成コードの正確性を保証することは依然として困難である。
検証可能なコード生成は、この制限に対処するための有望なパスを提供する。
論文 参考訳（メタデータ） (2025-05-29T06:12:52Z) - VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。
評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
論文 参考訳（メタデータ） (2025-05-25T19:00:52Z) - CodeDPO: Aligning Code Models with Self Generated and Verified Source Code [52.70310361822519]
我々は、コード生成に好み学習を統合するフレームワークであるCodeDPOを提案し、コードの正確性と効率性という2つの重要なコード優先要因を改善した。
CodeDPOは、コードとテストケースを同時に生成、評価するセルフジェネレーション・アンド・バリデーションメカニズムを利用して、新しいデータセット構築方法を採用している。
論文 参考訳（メタデータ） (2024-10-08T01:36:15Z) - Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
Code-Development Benchmark (Codev-Bench)は、細粒度で現実世界、リポジトリレベル、開発者中心の評価フレームワークです。
Codev-Agentは、リポジトリのクローリングを自動化し、実行環境を構築し、既存のユニットテストから動的呼び出しチェーンを抽出し、データ漏洩を避けるために新しいテストサンプルを生成するエージェントベースのシステムである。
論文 参考訳（メタデータ） (2024-10-02T09:11:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。