論文の概要: Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving

• arxiv url: http://arxiv.org/abs/2506.17104v1
• Date: Fri, 20 Jun 2025 16:09:56 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-23 19:00:05.527369
• Title: Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving
• Title（参考訳）: 第一次論理理論証明によるLLMの高度な数学的推論に向けて
• Authors: Chuxue Cao, Mengze Li, Juntao Dai, Jinluan Yang, Zijian Zhao, Shengyu Zhang, Weijie Shi, Chengzhong Liu, Sirui Han, Yike Guo,
• Abstract要約: 大規模言語モデル(LLM)は、有望な一階述語論理(FOL)推論能力を示している。 しかし、多段階のFOL還元を含む複雑な数学的推論におけるそれらの効果はいまだ研究されていない。 LLMの生成戦略の多様性と再現性を向上する自己適応型ソリューションであるDREAMを提案する。
• 参考スコア（独自算出の注目度）: 14.569345246475509
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models (LLMs) have shown promising first-order logic (FOL) reasoning capabilities with applications in various areas. However, their effectiveness in complex mathematical reasoning involving multi-step FOL deductions is still under-researched. While LLMs perform competitively on established mathematical reasoning benchmarks, they struggle with multi-step FOL tasks, as demonstrated by Deepseek-Prover-V2-7B's low accuracy (4.2%) on our proposed theorem proving dataset. This issue arises from the limited exploration of diverse proof strategies and the potential for early reasoning mistakes to undermine entire proofs. To address these issues, we propose DREAM, a self-adaptive solution that enhances the Diversity and REAsonability of LLMs' generation strategies. DREAM incorporates an Axiom-Driven Strategy Diversification mechanism to promote varied strategic outcomes and a Sub-Proposition Error Feedback to help LLMs reflect on and correct their proofs. Our contributions include pioneering advancements in LLMs' mathematical reasoning through FOL theorem proving, introducing a novel inference stage solution that improves performance by 0.6% to 6.4%, and providing a curated dataset of 447 mathematical theorems in Lean 4 format for evaluation.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、様々な分野のアプリケーションで有望な一階述語論理(FOL)推論能力を示している。 しかし、多段階のFOL還元を含む複雑な数学的推論におけるそれらの効果はいまだ研究されていない。 LLMは確立された数学的推論ベンチマークで競合的に動作するが、Deepseek-Prover-V2-7Bの低精度(4.2%)が提案した定理証明データセットで示すように、多段階のFOLタスクと競合する。 この問題は、多様な証明戦略の限定的な探索と、証明全体を損なう早期の推論ミスの可能性から生じる。 これらの課題に対処するため,LLM 生成戦略の多様性と再現性を向上する自己適応型ソリューション DREAM を提案する。 DREAMには、さまざまな戦略的成果を促進するための軸駆動戦略の多様化メカニズムと、LCMが証明を反映し修正するのに役立つサブプロポーションエラーフィードバックが組み込まれている。 私たちの貢献には、FOL定理証明によるLLMの数学的推論の先駆的な進歩、パフォーマンスを0.6%から6.4%改善する新しい推論段階ソリューションの導入、Lean 4フォーマットで447の数学的定理をキュレートしたデータセットの提供などが含まれます。

関連論文リスト

• Teaching LLMs According to Their Aptitude: Adaptive Reasoning for Mathematical Problem Solving [55.895917967408586]
  大規模な言語モデルによる数学的推論への既存のアプローチは、一般化可能性(英語版)にはChain-of-Thought(英語版)(CoT)、正確な計算にはTool-Integrated Reasoning(英語版)(TIR)に依存している。 本稿では, LLM が自然に推論戦略をパーソナライズできる適応型フレームワークである TATA (Teaching LLMs according their Aptitude) を提案する。
  論文  参考訳（メタデータ） (2025-02-17T16:56:23Z)
• LLM2: Let Large Language Models Harness System 2 Reasoning [65.89293674479907]
  大規模言語モデル(LLM)は、無数のタスクにまたがって印象的な機能を示してきたが、時には望ましくない出力が得られる。 本稿では LLM とプロセスベースの検証器を組み合わせた新しいフレームワーク LLM2 を紹介する。 LLMs2は妥当な候補を生成するのに責任を持ち、検証者は望ましい出力と望ましくない出力を区別するためにタイムリーなプロセスベースのフィードバックを提供する。
  論文  参考訳（メタデータ） (2024-12-29T06:32:36Z)
• What Makes In-context Learning Effective for Mathematical Reasoning: A Theoretical Analysis [81.15503859645149]
  本稿では,大規模言語モデルの推論性能に及ぼす文脈内実演の影響を理論的に解析することを目的とする。 本稿では, LMS3 という, 単純で一般化可能な, 低複雑さな実演選択法を提案する。
  論文  参考訳（メタデータ） (2024-12-11T11:38:11Z)
• Large Language Models Struggle with Unreasonability in Math Problems [41.970853209666224]
  大規模言語モデル(LLM)は、幅広い数学と推論のベンチマークで顕著な成功を収めている。 我々は、不合理な数学問題に直面した時にしばしば苦労するのを観察する。 我々は,不合理な数学問題文を検出し,応答するLLMの能力を評価するために,textbfUnreasonable Math Problems (UMP)ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-03-28T12:04:28Z)
• Identifying Factual Inconsistencies in Summaries: Grounding LLM Inference via Task Taxonomy [48.29181662640212]
  事実的矛盾は、生成モデルによる忠実な要約にとって重要なハードルとなる。 我々は,要約中の不整合事実のキーエラータイプを集約し,ゼロショットと教師付きパラダイムの両方を容易にするためにそれらを組み込んだ。
  論文  参考訳（メタデータ） (2024-02-20T08:41:23Z)
• Fill in the Blank: Exploring and Enhancing LLM Capabilities for Backward Reasoning in Math Word Problems [17.80128896525717]
  後向きの推論は 比較的未調査です 後方推論は 前方推論の「逆」と見なすことができます 性能改善のための3つの異なる前方推論戦略のバリエーションを提案する。
  論文  参考訳（メタデータ） (2023-10-03T12:03:06Z)

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

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