Fugu-MT 論文翻訳(概要): MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving

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

arxiv url: http://arxiv.org/abs/2503.03205v3
Date: Tue, 27 May 2025 07:37:52 GMT
ステータス: 翻訳完了
システム内更新日: 2025-05-28 14:37:19.253591
Title: MA-LoT: Model-Collaboration 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要約: この問題を解決するために,我々はLean4定理の包括的なフレームワークを提案する。一般的なNLの認識タスクを完全防御生成と証明修正のための誤り解析に分離する。我々のフレームワークは、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 the mathematical and computer science communities. State-of-the-art methods utilize a single Large Language Model (LLM) to generate complete proof or perform tree search, but they fail to balance these tasks. We propose **MA-LoT**: *Model-CollAboration Lean-based Long Chain-of-Thought*, a comprehensive framework for Lean4 theorem proving to solve this issue. It separates the cognition tasks of general NL for whole-proof generation and error analysis for proof correction using the model-collaboration method. We achieve this by structured interaction of the LLM and Lean4 verifier in Long CoT. To implement the framework, we propose the novel *LoT-Transfer Learning* training-inference pipeline, which enables the Long CoT thinking capability to LLMs without special data annotation. Extensive experiment shows that our framework achieves a **61.07%** accuracy rate on the Lean4 version of the MiniF2F-Test dataset, largely outperforming DeepSeek-V3 (33.61%), single-model 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（参考訳）: リーンのようなコンピュータで検証可能な言語を使って数学的問題を解くことは、数学と計算機科学のコミュニティに大きな影響を与えた。 State-of-the-artメソッドは、ひとつのLarge Language Model (LLM)を使用して完全な証明を生成したり、ツリー検索を行うが、これらのタスクのバランスが取れない。我々は**MA-LoT*: *Model-CollAboration LeanベースのLong Chain-of-Thought*を提案します。モデルコラボレーション法を用いて, 総合的なNLの認識タスクと, 検証訂正のための誤り解析を分離する。我々はLong CoTにおけるLLMとLean4検証器の構造的相互作用によりこれを達成した。このフレームワークを実装するために,Long CoT思考機能を特別なデータアノテーションを使わずにLong CoT思考機能を実現する,新しい*LoT-Transfer Learning*トレーニング推論パイプラインを提案する。我々のフレームワークは、MiniF2F-TestデータセットのLean4バージョンにおいて***61.07%*の精度を実現しており、DeepSeek-V3(33.61%)、シングルモデルツリーサーチ(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)

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

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