論文の概要: MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving

• arxiv url: http://arxiv.org/abs/2503.03205v1
• Date: Wed, 05 Mar 2025 05:50:31 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-06 15:53:41.811837
• Title: MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
• Title（参考訳）: MA-LoT: マルチエージェントのリーンベースのLong Chain-of-Thought Reasoningが形式的定理証明を強化
• Authors: Ruida Wang, Rui Pan, Yuxin Li, Jipeng Zhang, Yizhen Jia, Shizhe Diao, Renjie Pi, Junjie Hu, Tong Zhang,
• Abstract要約: State-of-the-artメソッドは、単一の大規模言語モデル(LLM)をエージェントまたはプロバーとして使用し、完全な証明を生成するか、ツリー検索を実行する。 マルチエージェントリーンベースのLong Chain-of-ProvフレームワークであるMA-LoTを提案する。 我々のフレームワークはMiniF2F-TestデータセットのLean4バージョンで54.51%の精度を実現している。
• 参考スコア（独自算出の注目度）: 30.112351299773632
• License:
• Abstract: Solving mathematical problems using computer-verifiable languages like Lean has significantly impacted mathematical and computer science communities. State-of-the-art methods utilize single Large Language Models (LLMs) as agents or provers to either generate complete proof or perform tree searches. However, single-agent methods inherently lack a structured way to combine high-level reasoning in Natural Language (NL) with Formal Language (FL) verification feedback. To solve these issues, we propose MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought framework, (to the best of our knowledge), the first multi-agent framework for Lean4 theorem proving that balance high-level NL reasoning and FL verification in Long CoT. Using this structured interaction, our approach enables deeper insights and long-term coherence in proof generation, with which past methods struggle. We do this by leveraging emergent formal reasoning ability in Long CoT using our novel LoT-Transfer Learning training-inference pipeline. Extensive experiments show that our framework achieves 54.51% accuracy rate on the Lean4 version of MiniF2F-Test dataset, largely outperforming GPT-4 (22.95%), single-agent tree search (InternLM-Step-Prover, 50.70%), and whole-proof generation (DeepSeek-Prover-v1.5, 48.36%) baselines. Furthermore, our findings highlight the potential of combining Long CoT with formal verification for a more insightful generation in a broader perspective.
• Abstract（参考訳）: Leanのようなコンピュータで検証可能な言語を使って数学的問題を解くことは、数学と計算機科学のコミュニティに大きな影響を与えている。 State-of-the-artメソッドは、単一の大規模言語モデル(LLM)をエージェントまたはプロバーとして使用し、完全な証明を生成するか、ツリー検索を実行する。 しかし、単一エージェント法は、自然言語(NL)の高レベル推論と形式言語(FL)の検証フィードバックを結合する構造的手法を本質的に欠いている。 マルチエージェントなリーンベースのLong Chain-of-Thoughtフレームワーク(私たちの知る限りでは)は、Long CoTにおける高レベルのNL推論とFL検証のバランスを証明する最初のマルチエージェントフレームワークです。 この構造的相互作用を用いることで、過去の手法が苦労した証明生成において、より深い洞察と長期的なコヒーレンスを実現することができる。 我々は、Long CoTにおける創発的な公式推論能力を活用して、新しいLoT-Transfer Learningトレーニング推論パイプラインを使用します。 大規模な実験により、我々のフレームワークは、MiniF2F-TestデータセットのLean4バージョンで54.51%の精度で達成され、GPT-4(22.95%)、シングルエージェントツリーサーチ(InternLM-Step-Prover, 50.70%)、全防御生成(DeepSeek-Prover-v1.5, 48.36%)のベースラインを上回った。 さらに,より広い視点で,Long CoTと形式的検証を併用し,より洞察に富んだ世代を創出する可能性を強調した。

関連論文リスト

• Facilitating Long Context Understanding via Supervised Chain-of-Thought Reasoning [47.30231319060358]
  我々は,Large Language Models (LLMs) にChain-of-Thought推論を統合して,効果的な長文理解を容易にする。 既存の長文合成データとは異なり、LongFinanceQAは最終結論の前に中間的なCoT推論を含む。 我々は,LongベンチマークでGPT-4o-mini w/PAIを評価し,標準GPT-4o-miniを20.0%上回るPAIの推論能力を評価する。
  論文  参考訳（メタデータ） (2025-02-18T18:50:06Z)
• When More is Less: Understanding Chain-of-Thought Length in LLMs [53.77747102201451]
  CoT推論は大規模言語モデル(LLM)の多段階推論能力を高める しかし、ほとんどのモデルやタスクでは、CoT長の増加は一貫して推論精度の向上につながりますか? 本稿では, 推論ステップの数が増加するにつれて, 性能は向上するが, 最終的には低下する,というニュアンスな関係を観察する。
  論文  参考訳（メタデータ） (2025-02-11T05:28:59Z)
• Insight-V: Exploring Long-Chain Visual Reasoning with Multimodal Large Language Models [64.1799100754406]
  大きな言語モデル(LLM)は、さらなる推論によって拡張された能力と信頼性を示す。 LLM推論の改善へのさまざまな取り組みにもかかわらず、高品質な長鎖推論データと最適化されたトレーニングパイプラインは、まだビジョン言語タスクでは不十分である。 本稿では,1)複雑なマルチモーダルタスクに対する長大かつ堅牢な推論データを生成するための初期の取り組みであるInsight-Vと,2)MLLMの推論能力を高めるための効果的なトレーニングパイプラインを提案する。
  論文  参考訳（メタデータ） (2024-11-21T18:59:55Z)
• GIVE: Structured Reasoning of Large Language Models with Knowledge Graph Inspired Veracity Extrapolation [108.2008975785364]
  Graph Inspired Veracity Extrapolation (GIVE)は、パラメトリックメモリと非パラメトリックメモリを融合して、最小の外部入力で正確な推論を改善する新しい推論手法である。 GIVE は LLM エージェントをガイドして,最も関連する専門家データ (observe) を選択し,クエリ固有の発散思考 (reflect) に従事し,その情報を合成して最終的な出力 (speak) を生成する。
  論文  参考訳（メタデータ） (2024-10-11T03:05:06Z)
• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
  TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。 我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
  論文  参考訳（メタデータ） (2024-07-03T15:36:18Z)
• Self-Discover: Large Language Models Self-Compose Reasoning Structures [136.48389510481758]
  タスク固有の推論構造を自己発見するフレームワークであるSELF-DISCOVERを紹介する。 SELF-DISCOVERは、挑戦的推論ベンチマークにおいて、GPT-4とPaLM 2の性能を大幅に改善する。 自己発見推論構造は、モデルファミリー全体にわたって普遍的に適用可能であることを示す。
  論文  参考訳（メタデータ） (2024-02-06T01:13:53Z)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  NLPシステムの予測に関する因果的説明は、安全性を確保し、信頼を確立するために不可欠である。 既存の手法は、しばしばモデル予測を効果的または効率的に説明できない。 本稿では, 対物近似(CF)の2つの手法を提案する。
  論文  参考訳（メタデータ） (2023-10-01T07:31:04Z)
• Multimodal Chain-of-Thought Reasoning in Language Models [94.70184390935661]
  言語(テキスト)と視覚(画像)のモダリティを2段階のフレームワークに組み込んだマルチモーダルCoTを提案する。 その結果,ScienceQA と A-OKVQA のベンチマークは,提案手法の有効性を示した。
  論文  参考訳（メタデータ） (2023-02-02T07:51:19Z)

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

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