論文の概要: LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction

• arxiv url: http://arxiv.org/abs/2502.17925v1
• Date: Tue, 25 Feb 2025 07:46:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-26 18:40:41.315877
• Title: LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
• Title（参考訳）: LeanProgress: プログレッシブ予測による神経理論の証明を導く
• Authors: Suozhi Huang, Peiyang Song, Robert Joseph George, Anima Anandkumar,
• Abstract要約: 証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
• 参考スコア（独自算出の注目度）: 74.79306773878955
• License:
• Abstract: Mathematical reasoning remains a significant challenge for Large Language Models (LLMs) due to hallucinations. When combined with formal proof assistants like Lean, these hallucinations can be eliminated through rigorous verification, making theorem proving reliable. However, even with formal verification, LLMs still struggle with long proofs and complex mathematical formalizations. While Lean with LLMs offers valuable assistance with retrieving lemmas, generating tactics, or even complete proofs, it lacks a crucial capability: providing a sense of proof progress. This limitation particularly impacts the overall development efficiency in large formalization projects. We introduce LeanProgress, a method that predicts the progress in the proof. Training and evaluating our models made on a large corpus of Lean proofs from Lean Workbook Plus and Mathlib4 and how many steps remain to complete it, we employ data preprocessing and balancing techniques to handle the skewed distribution of proof lengths. Our experiments show that LeanProgress achieves an overall prediction accuracy of 75.1\% in predicting the amount of progress and, hence, the remaining number of steps. When integrated into a best-first search framework using Reprover, our method shows a 3.8\% improvement on Mathlib4 compared to baseline performances of 41.2\%, particularly for longer proofs. These results demonstrate how proof progress prediction can enhance both automated and interactive theorem proving, enabling users to make more informed decisions about proof strategies.
• Abstract（参考訳）: 数学的推論は、幻覚のため、Large Language Models (LLMs) にとって重要な課題である。 Leanのような公式な証明アシスタントと組み合わせると、これらの幻覚は厳格な検証によって排除され、定理が信頼できることが証明される。 しかし、形式的検証でさえ、LLMは長い証明と複雑な数学的形式化に苦戦している。 Lean with LLMsは、レムマの回収、戦術の生成、あるいは完全な証明のための貴重な支援を提供するが、重要な能力、すなわち証明の進歩の感覚は欠如している。 この制限は、大規模な形式化プロジェクトの全体的な開発効率に特に影響を及ぼす。 証明の進捗を予測する手法であるLeanProgressを紹介します。 Lean Workbook PlusとMathlib4のリーン証明の大規模なコーパスに基づいて、モデルをトレーニングし、評価し、それを完了するためのステップがいくつあるかを確認します。 我々の実験によると、LeanProgressは進捗の予測において全体の予測精度が75.1\%に達しており、そのため残りのステップの数も増えています。 Reproverを用いたベストファースト検索フレームワークに組み込むと、特に長い証明において、ベースライン性能が41.2\%であるのに対し、Mathlib4は3.8\%改善している。 これらの結果は,証明進行予測が自動的および対話的定理証明の両立を図り,利用者が証明戦略についてより深い決定を下すことができることを示す。

関連論文リスト

• Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation [27.60611509339328]
  1つのトレーニングデータサンプルの最適順序は、特定の証明ステップの関連中間監督が、その証明ステップの左側に常に配置されているときに発生すると論じる。 証明が直感的に逐次順序にある場合、トレーニングが最も効果的であることを示す。
  論文  参考訳（メタデータ） (2024-10-30T18:00:04Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• 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)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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