論文の概要: Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs

• arxiv url: http://arxiv.org/abs/2606.17981v1
• Date: Tue, 16 Jun 2026 14:33:15 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-17 17:15:32.482685
• Title: Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs
• Title（参考訳）: ハマー計画:Rocqの証明を自動化するための難易度の高い分解
• Authors: Ning Zhang, Nongyu Di, Zenan Li, Yuan Yao, Xiaoxing Ma,
• Abstract要約: 提案するQuarryは,証明計画と証明実行を分離した,計画に基づく証明合成フレームワークである。 特に、Quarry は LLM に対して、任意のサブレンマを持つ複数の証明分解を積極的に提案するよう求め、Rocq で一時的に承認されたサブレンマの下でそれらをタイプチェックし、証明状態に基づく困難モデルを用いて候補をランク付けする。 可解性を考慮した評価による計画ベース分解は,予測可能なコストを維持しつつ,自動化を大幅に改善することを示す。
• 参考スコア（独自算出の注目度）: 21.65389718022749
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: As AI-generated code proliferates, formal verification, particularly through interactive theorem provers such as Rocq and Isabelle, becomes increasingly important for ensuring software correctness. However, producing machine-checked proofs in such provers remains a bottleneck. Existing solutions bring complementary strengths to proof automation: large language models (LLMs) can propose high-level proof strategies but lack local rigor, while automated tactics such as CoqHammer can reliably discharge many local goals but lack long-range planning capabilities. To combine the best of both worlds, we present Quarry, a planning-based proof synthesis framework that separates proof planning from proof execution. Specifically, Quarry asks an LLM to actively propose multiple proof decompositions with arbitrary sublemmas, type-checks them in Rocq under temporarily admitted sublemmas, and ranks candidates using a proof-state-based difficulty model that estimates hammer solvability. It then recursively proves sublemmas within a bounded budget, effectively turning long proofs into sequences of hammer-solvable obligations. We implement Quarry on top of SerAPI and CoqHammer and evaluate it using multiple frontier LLMs across multiple benchmarks. The experimental results show that planning-based decomposition with solvability-aware ranking substantially improves automation while maintaining predictable cost. Under a uniform 10-minute wall-clock budget, Quarry improves over the strongest baseline by 7% to 13% in success rate across three Rocq benchmarks. These results demonstrate that reliable proof automation can be achieved by coordinating neural planning with symbolic execution rather than replacing either.
• Abstract（参考訳）: AI生成コードの普及に伴い、特にRocqやIsabelleのようなインタラクティブな定理プロバーによる形式的検証は、ソフトウェアの正しさを保証するためにますます重要になる。 しかし、そのようなプローバーでマシンチェックされた証明を生成することは依然としてボトルネックである。 大規模言語モデル(LLM)は高いレベルの証明戦略を提案できるが、局所的な厳密さは欠いている。 両世界の長所を組み合わせるために,実証計画と証明実行を分離した計画ベースの証明合成フレームワークであるQuarryを提案する。 特に、Quarry は LLM に任意の部分補題を用いて複数の証明分解を積極的に提案するよう求め、Rocq で一時的に承認された部分補題の下でそれらをタイプチェックし、ハンマーの可解性を推定する証明状態に基づく困難モデルを用いて候補をランク付けする。 その後、境界予算内で再帰的にサブレムマを証明し、長い証明を効果的にハンマー解決可能な義務の列に変換する。 我々は、SerAPIとCoqHammer上にQuarryを実装し、複数のベンチマークで複数のフロンティアLSMを用いて評価する。 実験結果から, 可溶性を考慮した分解処理は, 予測可能コストを維持しつつ, 自動化を著しく向上させることがわかった。 均一な10分間の壁時計予算の下で、Quarryは3つのRocqベンチマークで7%から13%の成功率で最強のベースラインを上回ります。 これらの結果から,ニューラルプランニングとシンボリック実行をコーディネートすることで,信頼性の高い証明自動化を実現することができた。

関連論文リスト

• PROMISE: Proof Automation as Structural Imitation of Human Reasoning [15.113069562646302]
  ProMISEは,証明状態遷移に対するステートフルな探索として,証明生成を再構成する構造認識フレームワークである。 複数のLLMバックエンドにまたがるSEL4ベンチマークのPROMISEを評価し,SeleneやRangoといった先行システムと比較した。
  論文  参考訳（メタデータ） (2026-04-07T03:49:12Z)
• Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification [21.423111823947867]
  本稿では,システムレベルの検証プロジェクトの証明検索の自動化を目的とした,ニューロシンボリックな証明生成フレームワークを提案する。 このフレームワークは、証明状態に対して最優先のツリー探索を行い、次の候補証明ステップのためにLLMを何度もクエリする。 さらなるベンチマークの結果は強力な一般化を示し、スケーラブルな自動ソフトウェア検証への道のりを示している。
  論文  参考訳（メタデータ） (2026-03-20T07:45:49Z)
• Test-Time Scaling with Diffusion Language Models via Reward-Guided Stitching [66.39914384073145]
  本稿では,安価な拡散サンプリング推論をステップレベル候補の再利用プールに変換する自己整合性フレームワークを提案する。 ステップレベルの再結合は、難しい問題に対して最も有益であることがわかった。 トレーニング不要のフレームワークは、6つの数学およびコーディングタスクの平均精度を最大2倍改善します。
  論文  参考訳（メタデータ） (2026-02-26T11:08:39Z)
• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。 多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。 自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
  論文  参考訳（メタデータ） (2026-02-02T17:42:53Z)
• Scaling Code-Assisted Chain-of-Thoughts and Instructions for Model Reasoning [65.20602712957725]
  Cacoは、高品質で検証可能な多様な命令-CoT推論データの合成を自動化する新しいフレームワークである。 我々の研究は、人間の介入なしに自己持続的で信頼できる推論システムを構築するためのパラダイムを確立します。
  論文  参考訳（メタデータ） (2025-10-05T07:59:24Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。 エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。 この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• Sample, Don't Search: Rethinking Test-Time Alignment for Language Models [55.2480439325792]
  新しいテストタイムアライメントアプローチであるQAlignを紹介します。 テスト時間計算をスケールする際、QAlignは各プロンプトの最適配向分布からのサンプリングに収束する。 マルコフ連鎖モンテカルロのテキスト生成における最近の進歩を取り入れることで、基礎となるモデルを変更したり、ロジットアクセスを必要とせずに、より良い整合出力を可能にする。
  論文  参考訳（メタデータ） (2025-04-04T00:41:40Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• 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)

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

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