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

• arxiv url: http://arxiv.org/abs/2503.03205v2
• Date: Mon, 10 Mar 2025 17:39:42 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-11 15:50:06.68334
• 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-ProverフレームワークであるMA-LoTを提案する。 我々のフレームワークはMiniF2F-TestデータセットのLean4バージョンで61.07%の精度を実現している。
• 参考スコア（独自算出の注目度）: 30.112351299773632
• License: http://creativecommons.org/licenses/by/4.0/
• 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 a 61.07% accuracy rate on the Lean4 version of the MiniF2F-Test dataset, largely outperforming GPT-4 (22.95%), single-agent tree search (InternLM-Step-Prover, 50.70%), and whole-proof generation (Godel-Prover, 55.33%) 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バージョンで61.07%の精度を実現し、GPT-4(22.95%)、シングルエージェントツリーサーチ(InternLM-Step-Prover, 50.70%)、全防御生成(Godel-Prover, 55.33%)をほぼ上回りました。 さらに,より広い視点で,Long CoTと形式的検証を併用し,より洞察に富んだ世代を創出する可能性を強調した。

関連論文リスト

• Unlocking General Long Chain-of-Thought Reasoning Capabilities of Large Language Models via Representation Engineering [59.34894142132706]
  既存の作業では、いくつかの例だけをチューニングすることで、長いCoT推論の能力を効率的に引き出すことができる。 このことは、LLMの一般的な能力であるCoT推論の長さを調査する動機となっている。 LLMの一般的な長大CoT推論能力を解き放つ新しい表現工学手法であるGLoREを提案する。
  論文  参考訳（メタデータ） (2025-03-14T11:30:37Z)
• When More is Less: Understanding Chain-of-Thought Length in LLMs [53.77747102201451]
  CoT推論は大規模言語モデル(LLM)の多段階推論能力を高める しかし、ほとんどのモデルやタスクでは、CoT長の増加は一貫して推論精度の向上につながりますか? 本稿では, 推論ステップの数が増加するにつれて, 性能は向上するが, 最終的には低下する,というニュアンスな関係を観察する。
  論文  参考訳（メタデータ） (2025-02-11T05:28:59Z)
• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs [25.69931278771869]
  本稿では,形式的推論の即時適用シナリオである形式的検証に焦点を当てる。 我々は5つの形式仕様言語で18kの高品質な命令応答ペアを構築した。 フォーマルなデータによる微調整は、数学、推論、コーディング能力も強化する。
  論文  参考訳（メタデータ） (2025-01-27T17:00:56Z)
• 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)
• FLARE: Faithful Logic-Aided Reasoning and Exploration [50.9814063216852]
  タスク分解を用いて問題空間をトラバースする新しい手法を提案する。 我々はLarge Language Modelsを使ってソリューションを計画し、クエリを事実に軟式化し、論理プログラミングコードを使って述語する。 提案手法は,生成したコードに対する推論プロセスの忠実度を計算し,外部の解法に頼らずにマルチホップ探索のステップを解析する。
  論文  参考訳（メタデータ） (2024-10-14T19:39:11Z)
• 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)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  NLPシステムの予測に関する因果的説明は、安全性を確保し、信頼を確立するために不可欠である。 既存の手法は、しばしばモデル予測を効果的または効率的に説明できない。 本稿では, 対物近似(CF)の2つの手法を提案する。
  論文  参考訳（メタデータ） (2023-10-01T07:31:04Z)
• T-SciQ: Teaching Multimodal Chain-of-Thought Reasoning via Mixed Large Language Model Signals for Science Question Answering [59.63860993280275]
  大規模言語モデル(LLM)は、様々な自然言語処理(NLP)タスクにおいて例外的な性能を示した。 LLM信号を用いた科学質問応答の指導を目的とした,T-SciQと呼ばれる新しい手法を提案する。 提案手法は,ScienceQAベンチマークで96.18%の精度で,最先端のパフォーマンスを実現する。
  論文  参考訳（メタデータ） (2023-05-05T11:56:30Z)
• Multimodal Chain-of-Thought Reasoning in Language Models [94.70184390935661]
  言語(テキスト)と視覚(画像)のモダリティを2段階のフレームワークに組み込んだマルチモーダルCoTを提案する。 その結果,ScienceQA と A-OKVQA のベンチマークは,提案手法の有効性を示した。
  論文  参考訳（メタデータ） (2023-02-02T07:51:19Z)
• Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
  PACT(bf Proof bf Artifact bf Co-bf Training)は、カーネルレベルのコトレーニング用証明項から自己教師付きデータを抽出する一般的な手法である。 我々は、Transformer言語モデルによって駆動されるニューラル定理証明器でリーンを計測し、PACTがテスト定理の保留組における成功率を証明する定理を32%から48%に改善することを示す。
  論文  参考訳（メタデータ） (2021-02-11T18:59:24Z)

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

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