論文の概要: P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation
- arxiv url: http://arxiv.org/abs/2608.09277v1
- Date: Mon, 10 Aug 2026 08:33:18 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-11 19:16:37.160472
- Title: P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation
- Title（参考訳）: P$^{3}$: 検証コード生成のための共同プログラムと証明計画
- Abstract要約: 検証されたコード生成は、プログラムの実行可能プログラムとマシンチェック可能な証明の両方を生成するために、大きな言語モデル(LLM)を要求する。
このシーケンシャルパイプラインは、実際には非効率かつ非効率である可能性があることを観察する。
プログラムとその正当性引数を手作業で開発するべきだというディクストラの見解に触発されて、我々は$P3$を提案する。
- 参考スコア（独自算出の注目度）: 19.3449645807529
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification, promising software that is correct by construction. The de facto workflow decouples the two halves of the problem: first synthesize a program, then attempt to prove it correct. We observe that this sequential pipeline can be both ineffective and inefficient in practice. A program generated without anticipating its proof can be subtly incorrect or structurally difficult to verify, forcing the LLM into brittle repair loops that alternate between patching the code and patching the proof. Inspired by Dijkstra's view that a program and its correctness argument should be developed hand in hand, we propose $P^3$, an LLM-based agentic workflow that first derives a unified program-and-proof plan from the specification, then elaborates the implementation and proof scaffold under this shared plan. To evaluate verified code generation in realistic settings, we further introduce Lean4Commit0, a repository-derived, library-level benchmark built by extracting core APIs from real-world software repositories and translating their requirements, including relational specifications across APIs, into Lean tasks. Using four frontier LLM backends, we evaluate $P^3$ on Verina, AlgoVeri, and our Lean4Commit0 benchmark, where it achieves the highest solve rate in every benchmark--model setting. Compared with the stronger baseline, it improves solve rates by 4.6--11.2 percentage points and reduces per-task API cost by up to roughly 40\% and wall-clock time by up to roughly 37\% on the difficult subset of each benchmark. A targeted ablation further shows gains of 3.3--8.3 points over implementation-only planning, isolating the benefit of planning the program and proof jointly.
- Abstract（参考訳）: 検証されたコード生成は、実行可能プログラムとマシンチェック可能な証明の両方を生成するために大きな言語モデル(LLM)を要求する。
デファクトワークフローは問題の2つのハーフを分離する。まずプログラムを合成し、次にそれを正しく証明しようとする。
このシーケンシャルパイプラインは、実際には非効率かつ非効率である可能性があることを観察する。
証明を予想せずに生成されたプログラムは、コードへのパッチと証明のパッチの交互にLLMを不安定な修復ループに強制することで、不正確または構造的に検証が難しい可能性がある。
プログラムとその正当性引数を手作業で開発する,というDijkstra氏の見解に触発されて,まず,この共有計画の下で実装と証明の足場を詳述する,LCMベースのエージェントワークフローである$P^3$を提案する。
実世界のソフトウェアリポジトリからコアAPIを抽出し、API間のリレーショナル仕様を含むそれらの要件をLeanタスクに変換することで構築された、レポジトリ由来のライブラリレベルのベンチマークであるLean4Commit0をさらに導入する。
4つのフロンティアLCMバックエンドを使用して、Verina、AlgoVeri、Lean4Commit0ベンチマークを評価し、ベンチマークモデル設定毎に最も高い解決率を達成する。より強力なベースラインと比較して、各ベンチマークの難易度サブセットに対して、タスクごとのAPIコストを最大40倍、壁時計あたりのコストを最大37倍に削減する。
対象とするアブレーションにより、実装のみの計画よりも3.3～8.3ポイントの利益が得られ、プログラムと証明を共同で計画するメリットが分離される。
関連論文リスト
- Inferring Code Correctness from Specification [0.0]
大規模言語モデル(LLM)は現代のソフトウェア開発に不可欠なものとなり、大規模に自動コード生成を可能にしている。
提案するTRAILS(Targeted Reasoning Agreement via Inputs and Specifications)は,コンクリート(インプット,アウトプット)ペアによるLCM推論を基礎とする手法である。
TRAILSをLiveCodeBenchとCoCoClaNeLの2つのデータセット(Qwen3Coder-30B、Devstral-Small-24B、Olmo3.1-Instruct)で評価し、HoarePromptとZero-Shot Chain-of-Thoughtベースラインと比較した。
論文 参考訳（メタデータ） (2026-05-28T12:04:51Z) - SCDBench: A Benchmark for LLM-Based Smart Contract Decompilers [55.39407031861402]
本稿では,スマートコントラクトデコンパイルのためのデータセットとベンチマーク手法であるSCDBenchを紹介する。
データセットには600の現実のSolidityコントラクトと、ペア化されたバイトコード入力、地味なソースコード、再生可能なセマンティックチェックポイントが含まれている。
我々は,GLM-5の変種を含むゼロショット逆コンパイル設定において,Claude Opus 4.7,GPT-5.3-Codex,GLM-5を評価した。
論文 参考訳（メタデータ） (2026-05-27T20:08:47Z) - SPARC: Scenario Planning and Reasoning for Automated C Unit Test Generation [1.0010193170880752]
本稿では,高レベルのプログラム意図とポインタ演算と手動メモリ管理の厳密な構文制約とのギャップを埋める,ニューロシンボリックなシナリオベースのフレームワークを提案する。
我々は、59の現実世界およびアルゴリズムの被験者で評価し、バニラプロンプト生成ベースラインを31.36%、分岐カバレッジ26.01%、突然変異スコア20.78%で上回り、シンボリック実行ツールKLEEに適合または超えている。
論文 参考訳（メタデータ） (2026-02-18T18:09:03Z) - AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。
このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
論文 参考訳（メタデータ） (2026-02-10T06:58:26Z) - Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
LLM推論を改善するための実用的な方法として、推論時計算が再導入されている。
テスト時間スケーリング(TTS)アルゴリズムの多くは、自動回帰デコーディングに依存している。
そこで我々は,dLLM のための効率的な TTS フレームワーク Prism を提案する。
論文 参考訳（メタデータ） (2026-02-02T09:14:51Z) - Evaluating and Achieving Controllable Code Completion in Code LLM [89.64782747840225]
命令誘導型コード補完ベンチマークである制御可能コード補完ベンチマーク(C3-Bench)を提案する。
コード補完作業中に,オープンソースのプロプライエタリモデルと高度なプロプライエタリモデルの間に,命令追従機能にかなりのギャップがあることを明らかにする。
結果として得られたQwen2.5-Coder-C3は、C3-Bench上で最先端のパフォーマンスを達成する。
論文 参考訳（メタデータ） (2026-01-22T11:40:04Z) - Programming over Thinking: Efficient and Robust Multi-Constraint Planning [54.77940831026738]
SCOPEは、クエリ固有の推論をジェネリックコード実行から切り離すフレームワークである。
SCOPEは、コストとレイテンシを下げながら最先端のパフォーマンスを達成する。
論文 参考訳（メタデータ） (2026-01-14T02:58:07Z) - The 4/$δ$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee [5.345468714252351]
この研究は LLM-Verifier Convergence Theorem の開発によってギャップを埋める。
LLMと検証器の相互作用を離散時間マルコフ連鎖としてモデル化する。
われわれはこの予測を90,000件以上の治験を含む広範囲な実証キャンペーンでストレステストした。
論文 参考訳（メタデータ） (2025-11-30T22:19:09Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Learning to Reason via Program Generation, Emulation, and Search [33.11955431589091]
言語モデル(LM)によるプログラム合成は、多くの推論能力を解放した。
すべての推論タスクは、コードとして容易に表現できるわけではない。例えば、常識的推論、道徳的意思決定、皮肉な理解を含むタスクである。
我々は,プログラム合成スキルをこのようなタスクに拡張するために,コード生成とエミュレートされた実行(CoGEX)を提案する。
論文 参考訳（メタデータ） (2024-05-25T19:40:50Z) - LeTI: Learning to Generate from Textual Interactions [60.425769582343506]
本稿では,テキストインタラクション(LETI)から学習するLMの可能性を,バイナリラベルによる正当性をチェックするだけでなく,テキストフィードバックを通じて出力中のエラーをピンポイントし,説明する。
私たちの焦点はコード生成タスクであり、そこではモデルが自然言語命令に基づいてコードを生成する。
LETIは、目的のLMを用いて、自然言語命令、LM生成プログラム、テキストフィードバックの結合に基づいて、モデルを反復的に微調整する。
論文 参考訳（メタデータ） (2023-05-17T15:53:31Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。