論文の概要: 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-10-22 13:21:20.084148
• 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:
• 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で証明を検索した。

関連論文リスト

• 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)

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

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