論文の概要: Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification

• arxiv url: http://arxiv.org/abs/2603.19329v1
• Date: Wed, 18 Mar 2026 18:42:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-23 19:48:38.802455
• Title: Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification
• Title（参考訳）: Goedel-Code-Prover: オープンステート・オブ・ザ・アートコードの検証のための階層的証明検索
• Authors: Zenan Li, Ziran Yang, Deyuan, He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, Chi Jin,
• Abstract要約: 大規模言語モデル(LLM)は可塑性コードを生成することができるが、正確性には限界がある。 本稿では,Lean4における自動コード検証のための階層的証明検索フレームワークを提案する。 Goedel-Code-Prover-8Bは、分解と完了の両方のための単一の統一ポリシーです。
• 参考スコア（独自算出の注目度）: 34.98335927187393
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) can generate plausible code but offer limited guarantees of correctness. Formally verifying that implementations satisfy specifications requires constructing machine-checkable proofs, a task that remains beyond current automation. We propose a hierarchical proof search framework for automated code verification in Lean~4 that decomposes complex verification goals into structurally simpler subgoals before attempting tactic-level proving. Central to our approach is a principled decomposition score that combines constructive justification with structural effectiveness. Crucially, this score serves as both the training reward and the inference-time ranking criterion, ensuring strict alignment between optimization and deployment. We train Goedel-Code-Prover-8B, a single unified policy for both decomposition and completion, via supervised initialization followed by hybrid reinforcement learning, where a continuous decomposition reward drives planning exploration while supervised replay stabilizes proof generation. On three Lean-based code verification benchmarks comprising 427 tasks, our 8B-parameter model achieves a 62.0\% prove success rate, a 2.6$\times$ improvement over the strongest baseline, surpassing neural provers up to 84$\times$ larger. We further observe consistent inference-time scaling: success rates improve monotonically with search iterations and sampling budget, with our trained model achieving greater efficiency than frontier off-the-shelf models of comparable scale.
• Abstract（参考訳）: 大規模言語モデル(LLM)は可塑性コードを生成することができるが、正確性には限界がある。 実装が仕様を満たすことを正式に検証するには、マシンチェック可能な証明を構築する必要がある。 戦術レベルの証明を試みる前に、複雑な検証目標を構造的に単純なサブゴールに分解する、Lean~4における自動コード検証のための階層的な証明検索フレームワークを提案する。 我々のアプローチの中心は、構成的正当化と構造的有効性を組み合わせた、原理化された分解スコアである。 重要な点として、このスコアはトレーニング報酬と推論時間ランキングの基準の両方として機能し、最適化とデプロイメントの厳格な整合性を保証する。 我々は、教師付き初期化とハイブリッド強化学習を併用し、教師付きリプレイによる証明生成の安定化を図りつつ、計画探索を継続分解報酬で進める、単一の統合ポリシであるGoedel-Code-Prover-8Bを訓練する。 427のタスクからなる3つのリーンベースのコード検証ベンチマークでは、私たちの8Bパラメーターモデルは、成功率を62.0\%達成し、最強のベースラインよりも2.6$\times$改善し、最大84$\times$以上のニューラルプロバーを上回ります。 成功率は探索反復とサンプリング予算によって単調に改善され、トレーニングされたモデルは、比較可能なスケールのフロンティアオフザシェルフモデルよりも高い効率を達成する。

関連論文リスト

• Distill and Align Decomposition for Enhanced Claim Verification [51.93960785128124]
  複雑なクレーム検証には、文を検証可能なサブ文に分解する必要がある。 本稿では,分解品質と検証器のアライメントを最適化する強化学習手法を提案する。 我々のフレームワークは、より小さな言語モデルで最先端のクレーム検証を実現できる。
  論文  参考訳（メタデータ） (2026-02-25T12:32:04Z)
• CVeDRL: An Efficient Code Verifier via Difficulty-aware Reinforcement Learning [57.24524263804788]
  コード検証は、LLMベースのコード生成の検証後において重要な役割を果たす。 既存の教師付き微調整手法は、データの不足、高い失敗率、推論効率の低下に悩まされている。 機能的な報酬しか持たない単純RLは、難しいブランチやサンプルに対して効果的な単体テストを生成することができないことを示す。
  論文  参考訳（メタデータ） (2026-01-30T10:33:29Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction [32.14733357890831]
  本稿では,高品質なSVAを自動的に生成する新しい統合フレームワークAssertCoderを提案する。 AssertCoderは、不均一な仕様フォーマットを解析するために、モダリティに敏感な事前処理を使用する。 このフレームワークは、アサーションの品質を評価するために、突然変異に基づく評価アプローチを取り入れている。
  論文  参考訳（メタデータ） (2025-07-14T14:43:14Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Reasoning Through Execution: Unifying Process and Outcome Rewards for Code Generation [27.484259938667776]
  大規模言語モデルはコード生成に優れていますが、推論を必要とする複雑なプログラミングタスクに苦労します。 本稿では,実行可能検証を活用することで,プロセスと結果の監視を統一するアウトカム・リフィニング・プロセス・スーパービジョンを紹介する。 5つのモデルと3つのベンチマークによる実験では、26.9%の精度でコード効率が42.2%向上した。
  論文  参考訳（メタデータ） (2024-12-19T17:59:42Z)
• Self-Evaluation Guided Beam Search for Reasoning [61.523627290397556]
  我々は,Large Language Model (LLM) の推論プロセスのガイドと校正を行うための段階的自己評価機構を導入する。 本稿では,ビームサーチによる自己評価ガイダンスを統合した復号アルゴリズムを提案する。 我々のアプローチは、GSM8K、AQuA、StrategyQAにおいて、対応するCodexバックボンドベースラインをわずかに精度6.34%、9.56%、および5.46%で上回る。
  論文  参考訳（メタデータ） (2023-05-01T02:37:59Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。