論文の概要: InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems
- arxiv url: http://arxiv.org/abs/2410.15700v1
- Date: Mon, 21 Oct 2024 07:18:23 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-11-28 17:07:38.288542
- Title: InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems
- Title（参考訳）: InternLM2.5-StepProver:大規模LEAN問題に対するエキスパートイテレーションによる自動定理証明の改善
- Authors: Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, Kai Chen,
- Abstract要約: InternLM2.5-SteperはMiniF2F、Lean-Workbook-Plus、ProofNet、Patnamベンチマークのオープンソースステート・オブ・ザ・アートを実現している。
MiniF2Fテストでは65.9%をパスし、Lean-Workbook-Plusの17.0%の問題を証明(あるいは否定)している。
- 参考スコア（独自算出の注目度）: 47.93470713879515
- 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. The major learning paradigm is expert iteration, which necessitates a pre-defined dataset comprising numerous mathematical problems. In this process, LLMs attempt to prove problems within the dataset and iteratively refine their capabilities through self-training on the proofs they discover. We propose to use large scale LEAN problem datasets Lean-workbook for expert iteration with more than 20,000 CPU days. During expert iteration, we found log-linear trends between solved problem amount with proof length and CPU usage. We train a critic model to select relatively easy problems for policy models to make trials and guide the model to search for deeper proofs. InternLM2.5-StepProver achieves open-source state-of-the-art on MiniF2F, Lean-Workbook-Plus, ProofNet, and Putnam benchmarks. Specifically, it achieves a pass of 65.9% on the MiniF2F-test and proves (or disproves) 17.0% of problems in Lean-Workbook-Plus which shows a significant improvement compared to only 9.5% of problems proved when Lean-Workbook-Plus was released. 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はデータセット内の問題を証明しようと試み、発見する証明の自己学習を通じて、その能力を反復的に洗練する。
大規模なLEAN問題データセットを2万日以上のCPUで専門家のイテレーションに使用することを提案する。
専門的なイテレーションでは,問題量と証明時間,CPU使用量との間にログ線形傾向が認められた。
我々は、ポリシーモデルに対して比較的簡単な問題を選択して試行錯誤を行い、より深い証明を求めるようモデルに誘導するように批評家モデルを訓練する。
InternLM2.5-StepProverは、MiniF2F、Lean-Workbook-Plus、ProofNet、Patnamベンチマーク上で、最先端のオープンソースを実現する。
特に、MiniF2Fテストで65.9%のパスを達成し、Lean-Workbook-Plusで17.0%の問題を証明(あるいは否定)している。
我々は、我々のモデルをオープンソース化し、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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。