MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving

要約

LEANのようなコンピューターで検証可能な言語を使用して数学的問題を解決することは、数学的およびコンピューターサイエンスコミュニティに大きな影響を与えてきました。
最先端の方法では、単一の大手言語モデル（LLMS）をエージェントまたはプローバーとして利用して、完全な証明を生成するか、ツリー検索を実行します。
ただし、単一エージェントの方法には、自然言語（NL）の高レベルの推論と正式な言語（FL）検証フィードバックを組み合わせるための構造化された方法が本質的に欠けています。
これらの問題を解決するために、Ma-lot：Multi-Agent Based Long-of-Thech of-Thech Framework（私たちの知る限り）を提案します。これは、LEAN4定理の最初のマルチエージェントフレームワークであり、長いCOTの高レベルのNLの推論とFL検証のバランスをとることを証明しています。
この構造化された相互作用を使用して、私たちのアプローチは、過去の方法が苦労している、より深い洞察と長期的な一貫性を証明生成において可能にします。
私たちは、私たちの新しいロットトランスファー学習トレーニング – 訓練 – 推論パイプラインを使用して、長いCOTで緊急の正式な推論能力を活用することにより、これを行います。
広範な実験では、私たちのフレームワークが、MINIF2F-TESTデータセットのLEAN4バージョンで61.07％の精度を達成し、GPT-4（22.95％）、シングルエージェントツリー検索（Internlm-Step-Prover、50.70％）、および全プルフジェネレーション（Godel-Prover、55.33％）を上回ることを示しています。
さらに、私たちの調査結果は、より広い視点でより洞察に満ちた世代のために、長いCOTと正式な検証を組み合わせる可能性を強調しています。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google