論文の概要: InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search
- arxiv url: http://arxiv.org/abs/2410.15700v2
- Date: Tue, 21 Oct 2025 15:39:04 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-25 03:08:02.649989
- Title: InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search
- Title（参考訳）: InternLM2.5-StepProver:批判ガイド検索による自動定理証明の強化
- Authors: Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Zheng Yuan, Wenwei Zhang, Dahua Lin, Kai Chen,
- Abstract要約: 代表的な証明法は、証明手法を戦術によって反復的に構築することであり、典型的には最優先の探索スキームに従う。
本稿では,評価モデルを用いて選好情報を抽出する直感的かつ効果的な手法を提案する。
2万日以上のCPUを持つ大規模なエキスパートイテレーションが、証明者と批判者をさらに微調整するために適用される。
- 参考スコア（独自算出の注目度）: 65.05674971652776
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large Language Models (LLMs) have emerged as powerful tools in mathematical theorem proving, particularly when utilizing formal languages such as LEAN. A prevalent proof method involves the LLM prover iteratively constructing the proof tactic by tactic, typically following a best-first search scheme. However, this method often ignores the critical preference information inside the existing tactic trajectories, hindering the search for deeper proofs. We propose an intuitive yet effective method, which utilizes a critic model to capture the preference information and to guide the search of the prover model at runtime. Given the prover-critic framework, a large-scale expert iteration with more than 20,000 CPU days is then applied to further fine-tune the prover and the critic. The trained InternLM2.5-StepProver critic significantly boosts the performance of the prover model (59.4% to 65.9%). We also analyze the impact of the critic on various aspects of the theorem proving process during expert iteration, providing insights into its effectiveness. We open-source our models and searched proofs at https://github.com/InternLM/InternLM-Math and https://huggingface.co/datasets/internlm/Lean-Workbook.
- Abstract（参考訳）: 大規模言語モデル (LLM) は数学の定理証明において強力なツールとして登場しており、特にLEANのような形式言語を利用する場合である。
一般的な証明法では、LLM証明器が戦術による証明戦術を反復的に構築する。
しかし、この手法は既存の戦術軌跡内の批判的嗜好情報を無視することが多く、より深い証明の探索を妨げている。
本稿では,評価モデルを用いて選好情報を抽出し,実行時の証明者モデルの探索を誘導する直感的かつ効果的な手法を提案する。
証明批判的なフレームワークを考えると、2万日以上のCPUを持つ大規模な専門家のイテレーションが、証明者および批判者をさらに微調整するために適用される。
トレーニングされたInternLM2.5-StepProverは、証明モデルの性能を著しく向上させる(59.4%から65.9%)。
また、専門家の反復における定理証明過程の様々な側面に対する批評家の影響を分析し、その効果について考察する。
我々は我々のモデルをオープンソース化し、https://github.com/InternLM/InternLM-Math and https://huggingface.co/datasets/internlm/Lean-Workbookで証明を検索した。
関連論文リスト
- Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs [6.65877320351217]
我々はLeanNavigatorを開発した。これはリーンの定理と証明の大規模なデータセットを生成する新しい方法だ。
我々は10億のトークンを合計470万の定理で生成し、以前のデータセットを桁違いに上回った。
この広範なデータセットを使用して、我々は、定理証明タスクにおいて最先端のReProverモデルより優れたAIモデルを訓練した。
論文 参考訳（メタデータ） (2025-02-16T06:20:39Z) - Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。
まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。
次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。
最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z) - STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving [33.61458249318183]
セルフプレイ・セオレム・プロバー(STP)は、予想と証明という2つの役割を担っている。
STPは同時に、予想と証明という2つの役割を担っている。
私たちはLeanとIsabelleの2つの形式的検証ツールで評価します。
論文 参考訳（メタデータ） (2025-01-31T23:01:48Z) - 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) - Leveraging Online Olympiad-Level Math Problems for LLMs Training and Contamination-Resistant Evaluation [55.21013307734612]
AoPS-Instructは60,000以上の高品質QAペアのデータセットである。
LiveAoPSBenchは、最新のフォーラムデータから派生したタイムスタンプによる進化的評価セットである。
我々の研究は、高度な数学推論のための大規模で高品質なデータセットの作成と維持にスケーラブルなアプローチを提示している。
論文 参考訳（メタデータ） (2025-01-24T06:39:38Z) - A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems [0.0]
リーンの残りのIMO問題に対する完全な、オリジナルの公式な証明を書いています。
この取り組みは,5,880行のリーン証明を作成することで,現在パブリックドメインにある証明の可用性を拡大するものだ。
論文 参考訳（メタデータ） (2024-11-28T02:50:42Z) - One Thousand and One Pairs: A "novel" challenge for long-context language models [56.60667988954638]
NoChaは、67冊の架空の書籍に関する1,001対の真偽の主張のデータセットである。
当社のアノテータは、NoChaにおけるペアの最大シェアは、本全体に対するグローバルな推論を必要としていることを確認しています。
平均的なモデルでは、文レベルの検索しか必要としないペアの方が、グローバルな推論よりもはるかに優れています。
論文 参考訳（メタデータ） (2024-06-24T02:03:57Z) - Lean Workbook: A large-scale Lean problem set formalized from natural language math problems [50.22847430754973]
大規模な言語モデルは、リーンのような形式言語を使って証明する数学の定理が得意ではありません。
この領域で重要な課題は、これらの形式言語で利用可能なトレーニングデータの不足である。
本稿では,自然言語の数学的問題をリーン4文に変換するために,合成データを反復的に生成・フィルタリングするパイプラインを提案する。
論文 参考訳（メタデータ） (2024-06-06T08:25:43Z) - Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。
証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。
実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
論文 参考訳（メタデータ） (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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。