論文の概要: HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement

• arxiv url: http://arxiv.org/abs/2505.15740v1
• Date: Wed, 21 May 2025 16:45:43 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-22 15:42:59.783856
• Title: HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
• Title（参考訳）: HybridProver: LLM駆動の証明合成と精製による定理の強化
• Authors: Jilin Hu, Jianyu Zhang, Yongwang Zhao, Talia Ringer,
• Abstract要約: HybridProverは、戦術ベースの生成と全防御合成を組み合わせたデュアルモデル証明フレームワークである。 最適化されたデータセット上にIsabelle定理証明器とファインチューンLPMにHybridProverを実装した。
• 参考スコア（独自算出の注目度）: 7.702809989052384
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal methods is pivotal for verifying the reliability of critical systems through rigorous mathematical proofs. However, its adoption is hindered by labor-intensive manual proofs and the expertise required to use theorem provers. Recent advancements in large language models (LLMs) offer new opportunities for automated theorem proving. Two promising approaches are generating tactics step by step and generating a whole proof directly with an LLM. However, existing work makes no attempt to combine the two approaches. In this work, we introduce HybridProver, a dual-model proof synthesis framework that combines tactic-based generation and whole-proof synthesis to harness the benefits of both approaches. HybridProver generates whole proof candidates for evaluation directly, then extracts proof sketches from those candidates. It then uses a tactic-based generation model that integrates automated tools to complete the sketches via stepwise refinement. We implement HybridProver for the Isabelle theorem prover and fine-tune LLMs on our optimized Isabelle datasets. Evaluation on the miniF2F dataset illustrates HybridProver's effectiveness. We achieve a 59.4% success rate on miniF2F, where the previous SOTA is 56.1%. Our ablation studies show that this SOTA result is attributable to combining whole-proof and tactic-based generation. Additionally, we show how the dataset quality, training parameters, and sampling diversity affect the final result during automated theorem proving with LLMs. All of our code, datasets, and LLMs are open source.
• Abstract（参考訳）: 形式的手法は厳密な数学的証明を通じて臨界システムの信頼性を検証するために重要である。 しかし、その採用は労働集約的な手作業による証明や、定理プローバーの使用に必要な専門知識によって妨げられている。 大規模言語モデル(LLM)の最近の進歩は、自動定理証明の新しい機会を提供する。 2つの有望なアプローチは、段階的に戦術を生成し、LSMで直接証明を生成する。 しかし、既存の作業ではこの2つのアプローチを組み合わせようとはしない。 本稿では,戦術ベース生成と全防御合成を組み合わせた2モデル証明合成フレームワークであるHybridProverを紹介する。 HybridProverは、直接評価のためのすべての証明候補を生成し、それらの候補から証明スケッチを抽出する。 次に、戦術ベースの生成モデルを使用して、自動ツールを統合して、ステップワイズによるスケッチを完了します。 最適化したIsabelleデータセット上に,Isabelle定理証明器と微調整LDMに対してHybridProverを実装した。 miniF2Fデータセットの評価は、HybridProverの有効性を示している。 我々は、以前のSOTAが56.1%であるminiF2Fで59.4%の成功率を達成した。 我々のアブレーション研究は、このSOTA結果が、全体的な防御と戦術に基づく世代の組み合わせに起因することを示唆している。 さらに,LLMを用いた自動定理証明において,データセットの品質,トレーニングパラメータ,サンプリングの多様性が最終結果にどのように影響するかを示す。 コード、データセット、LLMはすべてオープンソースです。

関連論文リスト

• LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation [11.045086599038338]
  本研究では,幅広い中間的証明状態にまたがる多様な戦術を創出するために設計された,データ合成の訓練のための新しい実証状態探索手法を提案する。 また,データ合成手法を効果的に活用し,木探索における探索と利用のトレードオフを実現する適応ビームサイズ戦略を提案する。
  論文  参考訳（メタデータ） (2025-05-17T14:47:36Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [8.056359341994941]
  APOLLOは、Leanコンパイラの強みとLLMの推論能力を組み合わせた、モデルに依存しないパイプラインである。 miniF2Fベンチマークでは、新しい最先端精度75.0%が確立されている。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明のステップを提案し、証明の目標を完了し、関連する前提を選択するツールを構築します。 人間を助ける場合、Lean Copilotは平均3.86で手動で入力された証明ステップを2.08ステップしか必要としない。 定理証明プロセスを自動化する場合、Lean Copilotの74.2%の証明ステップは平均85%がエソップ(40.1%)より優れている。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method [1.8130068086063336]
  本稿では,定理証明のための新しい動的サンプリング手法であるDS-Proverを紹介する。 単純化と書き直しの戦術を複数の前提で1つの前提で戦術に分解することで、トレーニングデータセットを強化します。 ProofNetデータセットでは14.2%の最先端パフォーマンス(Pass@1)、MiniF2Fでは29.8%のパフォーマンスを実現しています。
  論文  参考訳（メタデータ） (2023-12-20T09:55:21Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

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

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