論文の概要: DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning

• arxiv url: http://arxiv.org/abs/2505.23754v1
• Date: Thu, 29 May 2025 17:59:39 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-30 18:14:08.08183
• Title: DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
• Title（参考訳）: DeepTheorem: 自然言語と強化学習による理論証明のためのLLM推論の改善
• Authors: Ziyin Zhang, Jiahao Xu, Zhiwei He, Tian Liang, Qiuzhi Liu, Yansi Li, Linfeng Song, Zhengwen Liang, Zhuosheng Zhang, Rui Wang, Zhaopeng Tu, Haitao Mi, Dong Yu,
• Abstract要約: DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
• 参考スコア（独自算出の注目度）: 63.05896558836976
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Theorem proving serves as a major testbed for evaluating complex reasoning abilities in large language models (LLMs). However, traditional automated theorem proving (ATP) approaches rely heavily on formal proof systems that poorly align with LLMs' strength derived from informal, natural language knowledge acquired during pre-training. In this work, we propose DeepTheorem, a comprehensive informal theorem-proving framework exploiting natural language to enhance LLM mathematical reasoning. DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs spanning diverse mathematical domains, rigorously annotated for correctness, difficulty, and topic categories, accompanied by systematically constructed verifiable theorem variants. We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference. Additionally, we propose comprehensive outcome and process evaluation metrics examining proof correctness and the quality of reasoning steps. Extensive experimental analyses demonstrate DeepTheorem significantly improves LLM theorem-proving performance compared to existing datasets and supervised fine-tuning protocols, achieving state-of-the-art accuracy and reasoning quality. Our findings highlight DeepTheorem's potential to fundamentally advance automated informal theorem proving and mathematical exploration.
• Abstract（参考訳）: 定理証明は、大規模言語モデル(LLM)における複雑な推論能力を評価するための主要なテストベッドとして機能する。 しかし、従来の自動定理証明(ATP)アプローチは、事前学習中に獲得した非公式な自然言語知識から得られるLLMの強みとよく一致しない形式的証明システムに大きく依存している。 本研究では,LLMの数学的推論を強化するために自然言語を利用した包括的な非公式な定理証明フレームワークであるDeepTheoremを提案する。 DeepTheoremは121Kの高品質なIMOレベルの非公式定理と様々な数学領域にまたがる証明からなる大規模なベンチマークデータセットを含み、正確性、難易度、トピックカテゴリに厳格に注釈付けされ、体系的に構築された検証済みの定理の変種が伴う。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。 さらに,検証の正しさと推論手順の質を検証した総合的な結果とプロセス評価指標を提案する。 大規模な実験分析により、DeepTheoremは既存のデータセットや教師付き微調整プロトコルと比較してLCMの定理証明性能を著しく改善し、最先端の精度と推論品質を実現している。 この結果から,DeepTheoremが自動定理の証明と数学的探索を根本的に進める可能性が示唆された。

関連論文リスト

• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• Measurability in the Fundamental Theorem of Statistical Learning [0.0]
  統計的学習の基本定理は、仮説空間がPAC学習可能であることと、そのVC次元が有限であることは同値である。 本稿では、実数 O-極小展開上で定義された仮説空間のPAC学習可能性について十分な条件を示す。 この仮説空間のクラスは、ReLUやシグモイド関数のようなよく用いられる活性化関数を使用する二項分類のためのすべての人工ニューラルネットワークをカバーする。
  論文  参考訳（メタデータ） (2024-10-14T08:03:06Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• A Survey on Deep Learning for Theorem Proving [16.28502772608166]
  定理証明は数学の基本的な側面であり、自然言語における非公式な推論から形式体系における厳密な導出にまで及ぶ。 ディープラーニング、特に大きな言語モデルの出現は、定理証明のプロセスを強化するためにこれらの技術を探究する研究の顕著な急増を引き起こした。
  論文  参考訳（メタデータ） (2024-04-15T17:07:55Z)
• Learning to Guide a Saturation-Based Theorem Prover [9.228237801323042]
  TRAILは、ニューラルネットワーク内で証明される飽和に基づく定理の中核要素を特徴付ける、深い学習に基づく定理証明のアプローチである。 我々の知る限りでは、TRAILは最先端の伝統的な定理証明器の性能を超える最初の強化学習に基づくアプローチである。
  論文  参考訳（メタデータ） (2021-06-07T18:35:57Z)

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

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