論文の概要: DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
- arxiv url: http://arxiv.org/abs/2505.23754v2
- Date: Tue, 03 Jun 2025 11:23:21 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-06-04 16:31:03.681431
- 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, Zhenwen Liang, Zhuosheng Zhang, Rui Wang, Zhaopeng Tu, Haitao Mi, Dong Yu,
- Abstract要約: DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。
DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。
我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
- 参考スコア(独自算出の注目度): 67.93945726549289
- 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が自動定理の証明と数学的探索を根本的に進める可能性が示唆された。
関連論文リスト
- LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving [6.220998637943786]
LeanConjecturerは、Large Language Models(LLMs)を使用して、Lean 4で大学レベルの数学予想を自動的に生成するパイプラインである。
反復生成と評価により、LeanConjecturerは40のMathlibシードファイルから12,289の予想を生成し、3,776は構文的に有効で非自明であると同定された。
論文 参考訳(メタデータ) (2025-06-27T08:17:18Z) - From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem [0.0]
我々は、選好完全性、推移性、連続性、独立性の古典的な公理を実践する。
我々の定式化は、宝くじに対する嗜好関係の数学的構造を捉えている。
この形式化は、経済モデリング、AIアライメント、管理決定システムにおける応用のための厳格な基盤を提供する。
論文 参考訳(メタデータ) (2025-06-08T10:09:54Z) - FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。
本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。
現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
論文 参考訳(メタデータ) (2025-05-05T15:37:00Z) - One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [57.48325300739872]
証明生成のための数学的大規模言語モデルを活用することは、LLM研究の基本的なトピックである。
現状のLCMが証明できる能力は、学習中に関連する証明プロセスに遭遇したかどうかに大きく依存していると論じる。
人間の数学教育で一般的に用いられる「反例による防御」の教育的手法に触発されて,我々の研究は,反例を通して数学的推論と証明を行うLLMの能力を高めることを目的としている。
論文 参考訳(メタデータ) (2025-02-12T02:01:10Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳(メタデータ) (2024-10-21T08:04:21Z) - 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) - Proving Theorems Recursively [80.42431358105482]
本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。
従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。
また,POETRYが検出した最大証明長は10~26。
論文 参考訳(メタデータ) (2024-05-23T10:35:08Z) - 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) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。