論文の概要: 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 17:18:40.805817
• 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: 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 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と形式的検証を併用し,より洞察に富んだ世代を創出する可能性を強調した。

関連論文リスト

• Solving Formal Math Problems by Decomposition and Iterative Reflection [30.54275542622631]
  textbfDelta Proverは汎用LLMとLean 4の実証環境とのインタラクションを編成します。 bftextDelta Proverは、miniF2F-testベンチマークで、最先端の95.9%の成功率を達成した。
  論文  参考訳（メタデータ） (2025-07-21T03:56:35Z)
• MiCoTA: Bridging the Learnability Gap with Intermediate CoT and Teacher Assistants [25.45861816665351]
  textbfMid-textbfCoT textbfTeacher textbfAssistant Distillation (MiCoTAl)を紹介する。 MiCoTAlは、小型言語モデル(SLM)のための長いCoT蒸留を改善するためのフレームワークである
  論文  参考訳（メタデータ） (2025-07-02T16:57:01Z)
• SELT: Self-Evaluation Tree Search for LLMs with Task Decomposition [5.5688696788198975]
  外部報酬モデルに頼らずにLSM推論を強化する新しいフレームワークであるSELT(Self-Evaluation LLM Tree Search)を紹介する。 知識に基づくMMLUとツール学習データセットSeal-Toolsを含む,挑戦的なベンチマークに対するアプローチを検証する。
  論文  参考訳（メタデータ） (2025-06-09T08:52:27Z)
• Mind the Gap: Bridging Thought Leap for Improved Chain-of-Thought Tuning [54.65050470296886]
  本研究では,跳躍を自動的に検出し,中間的推論ステップを欠くことを目的としたCoT Thought Leap Bridge Taskを提案する。 ブリッジされたデータセットに微調整されたモデルが、元のデータセットでトレーニングされたモデルよりも一貫して優れていることを示す。 提案手法は, 蒸留データを効果的に向上させ, 強化学習の出発点として優れたものを提供する。
  論文  参考訳（メタデータ） (2025-05-20T17:59:31Z)
• Model Utility Law: Evaluating LLMs beyond Performance through Mechanism Interpretable Metric [99.56567010306807]
  大規模言語モデル(LLM)は、学術、産業、そして日々のアプリケーションに欠かせないものになっている。 大規模言語モデル (LLM) 時代における評価の課題の1つは一般化問題である。 従来の性能スコアを補完するメカニズムの解釈可能性向上指標であるモデル利用指数(MUI)を提案する。
  論文  参考訳（メタデータ） (2025-04-10T04:09:47Z)
• 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)
• LLMs Can Easily Learn to Reason from Demonstrations Structure, not content, is what matters! [53.84130385074551]
  大推論モデル(LRM)は、長いチェーン・オブ・シント(Long CoT)に従うことによって複雑な推論問題に取り組む また,Large Language Model (LLM) は,データ効率の教師付き微調整 (SFT) とパラメータ効率の低い低ランク適応 (LoRA) により,Long CoT推論を効果的に学習できることを見出した。 たった17kのCoTトレーニングサンプルで、Qwen2.5-32B-Instructモデルは、幅広い数学およびコーディングベンチマークで大幅に改善されている。
  論文  参考訳（メタデータ） (2025-02-11T08:48:48Z)
• 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)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  NLPシステムの予測に関する因果的説明は、安全性を確保し、信頼を確立するために不可欠である。 既存の手法は、しばしばモデル予測を効果的または効率的に説明できない。 本稿では, 対物近似(CF)の2つの手法を提案する。
  論文  参考訳（メタデータ） (2023-10-01T07:31:04Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• LLM-Pruner: On the Structural Pruning of Large Language Models [65.02607075556742]
  大規模言語モデル(LLM)は、言語理解と生成において顕著な能力を示している。 タスク非依存であり、元のトレーニングデータセットへの依存を最小限に抑えるという2つの制約の範囲内でLLMの圧縮に取り組む。 LLM-Prunerという名前のこの手法は、非臨界結合構造を選択的に除去する構造プルーニングを採用する。
  論文  参考訳（メタデータ） (2023-05-19T12:10:53Z)
• 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)

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

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