論文の概要: Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem

• arxiv url: http://arxiv.org/abs/2509.06809v1
• Date: Mon, 08 Sep 2025 15:43:29 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-09 14:07:04.22184
• Title: Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem
• Title（参考訳）: TPTP生態系におけるLLM数学的推論のための飽和駆動型データセット生成
• Authors: Valentin Quesnel, Damien Sileo,
• Abstract要約: 巨大なTPTP公理ライブラリ上のEプローサの飽和能力は、定理の巨大で保証された有価なコーパスを導出するために使用される。 私たちのパイプラインは原則的かつ単純で、公理は飽和し、"興味深い"定理のフィルタを行い、タスクを生成する。 この純粋に象徴的なデータは、エンテーメント検証、前提選択、証明再構成という3つの難易度制御された課題に変換される。
• 参考スコア（独自算出の注目度）: 2.9458822941489387
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The scarcity of high-quality, logically sound data is a critical bottleneck for advancing the mathematical reasoning of Large Language Models (LLMs). Our work confronts this challenge by turning decades of automated theorem proving research into a scalable data engine. Rather than relying on error-prone LLMs or complex proof-assistant syntax like Lean and Isabelle, our framework leverages E-prover's saturation capabilities on the vast TPTP axiom library to derive a massive, guaranteed-valid corpus of theorems. Our pipeline is principled and simple: saturate axioms, filter for "interesting" theorems, and generate tasks. With no LLMs in the loop, we eliminate factual errors by construction. This purely symbolic data is then transformed into three difficulty-controlled challenges: entailment verification, premise selection, and proof reconstruction. Our zero-shot experiments on frontier models reveal a clear weakness: performance collapses on tasks requiring deep, structural reasoning. Our framework provides both the diagnostic tool to measure this gap and a scalable source of symbolic training data to address it. We make the code and data publicly available. https://github.com/sileod/reasoning_core https://hf.co/datasets/reasoning-core/rc1
• Abstract（参考訳）: 高品質で論理的な音声データの不足は、Large Language Models (LLMs) の数学的推論を進める上で重要なボトルネックとなる。 私たちの研究は、何十年にもわたって自動化された定理を、研究をスケーラブルなデータエンジンに変えることで、この課題に直面しています。 LeanやIsabelleのようなエラーを起こしやすいLLMや複雑な証明補助構文に頼るのではなく、我々のフレームワークは、巨大なTPTP公理ライブラリ上のE-proverの飽和機能を活用して、巨大な、保証された検証可能な定理のコーパスを導出します。 我々のパイプラインは原理的で単純で、公理を飽和させ、「興味深い」定理のフィルタを行い、タスクを生成する。 ループにLLMがなければ、構築による実ミスを排除できる。 この純粋に象徴的なデータは、エンテーメント検証、前提選択、証明再構成という3つの難易度制御された課題に変換される。 私たちのフロンティアモデルにおけるゼロショット実験は明らかな弱点を明らかにします。 我々のフレームワークは、このギャップを測定するための診断ツールと、それに対応するためのシンボリックトレーニングデータのスケーラブルなソースの両方を提供します。 コードとデータを公開しています。 https://github.com/sileod/reasoning_core https://hf.co/datasets/reasoning-core/rc1

関連論文リスト

• Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs [6.65877320351217]
  我々はLeanNavigatorを開発した。これはリーンの定理と証明の大規模なデータセットを生成する新しい方法だ。 我々は10億のトークンを合計470万の定理で生成し、以前のデータセットを桁違いに上回った。 この広範なデータセットを使用して、我々は、定理証明タスクにおいて最先端のReProverモデルより優れたAIモデルを訓練した。
  論文  参考訳（メタデータ） (2025-02-16T06:20:39Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

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

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