論文の概要: MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation

• arxiv url: http://arxiv.org/abs/2505.10962v1
• Date: Fri, 16 May 2025 07:56:03 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-19 14:36:14.287827
• Title: MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
• Title（参考訳）: MPS-Prover:マルチパースペクティブ検索とデータキュレーションによるステップワイズ理論の証明
• Authors: Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, Dong Yu,
• Abstract要約: 本稿では,制限を克服する新しいATPシステムであるMPS-Proverを紹介する。 MPS-Proverには、パフォーマンスを犠牲にすることなく、冗長なトレーニングデータの約40%を産み出す、非常に効果的なポストトレーニングデータキュレーション戦略と、多目的のツリーサーチメカニズムの2つの重要なイノベーションが含まれている。 大規模な評価では、MPS-Proverは、miniF2FやProofNetなど、複数の挑戦的なベンチマークで最先端のパフォーマンスを達成している。
• 参考スコア（独自算出の注目度）: 48.22540519786074
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated Theorem Proving (ATP) in formal languages remains a formidable challenge in AI, demanding rigorous logical deduction and navigating vast search spaces. While large language models (LLMs) have shown promising performance, existing stepwise provers often suffer from biased search guidance, leading to inefficiencies and suboptimal proof strategies. This paper introduces the Multi-Perspective Search Prover (MPS-Prover), a novel stepwise ATP system designed to overcome these limitations. MPS-Prover incorporates two key innovations: a highly effective post-training data curation strategy that prunes approximately 40% of redundant training data without sacrificing performance, and a multi-perspective tree search mechanism. This search integrates a learned critic model with strategically designed heuristic rules to diversify tactic selection, prevent getting trapped in unproductive states, and enhance search robustness. Extensive evaluations demonstrate that MPS-Prover achieves state-of-the-art performance on multiple challenging benchmarks, including miniF2F and ProofNet, outperforming prior 7B parameter models. Furthermore, our analyses reveal that MPS-Prover generates significantly shorter and more diverse proofs compared to existing stepwise and whole-proof methods, highlighting its efficiency and efficacy. Our work advances the capabilities of LLM-based formal reasoning and offers a robust framework and a comprehensive analysis for developing more powerful theorem provers.
• Abstract（参考訳）: 形式言語におけるATP(Automated Theorem Proving)は、厳格な論理的推論と膨大な検索空間のナビゲートを要求するAIにおいて、依然として深刻な課題である。 大規模言語モデル(LLM)は有望な性能を示したが、既存の段階的証明者はしばしばバイアス付き検索誘導に悩まされ、非効率性や準最適証明戦略に繋がる。 本稿では,MPS-Prover(Multi-Perspective Search Prover)を提案する。 MPS-Proverには、パフォーマンスを犠牲にすることなく、冗長なトレーニングデータの約40%を産み出す、非常に効果的なポストトレーニングデータキュレーション戦略と、多面的なツリー検索メカニズムの2つの重要なイノベーションが含まれている。 このサーチは、学習した批評家モデルと戦略的に設計されたヒューリスティックなルールを統合し、戦術選択を多様化し、非生産的な状態に閉じ込められないようにし、検索の堅牢性を高める。 大規模な評価では、MPS-Proverは、miniF2FやProofNetなど、複数の挑戦的なベンチマークで最先端のパフォーマンスを達成し、以前の7Bパラメータモデルを上回っている。 さらに,MPS-Proverは,既存のステップワイド法や全防法に比べて有意に短く,多彩な証明が得られ,その効率と有効性を強調した。 我々の研究は、LLMに基づく形式推論の能力を前進させ、より強力な定理証明器を開発するための堅牢なフレームワークと包括的な分析を提供する。

関連論文リスト

• Do We Truly Need So Many Samples? Multi-LLM Repeated Sampling Efficiently Scales Test-Time Compute [54.22256089592864]
  本稿では,テスト時間計算のスケールアップによるLCM性能向上のための,シンプルで効果的で費用効率のよい手法を提案する。 当社の戦略は,複数のモデルを組み込んで,補完的な強みを活用するという,新たなツイストによって,繰り返しサンプリングされる投票フレームワークを基盤としています。
  論文  参考訳（メタデータ） (2025-04-01T13:13:43Z)
• Progressive Multimodal Reasoning via Active Retrieval [64.74746997923967]
  多段階多モーダル推論タスクは、大規模言語モデル(MLLM)に重大な課題をもたらす 本稿では,MLLMの推論能力の向上を目的とした汎用フレームワークAR-MCTSを提案する。 我々は,AR-MCTSがサンプリングの多様性と精度を最適化し,信頼性の高いマルチモーダル推論を実現することを示す。
  論文  参考訳（メタデータ） (2024-12-19T13:25:39Z)
• Enhancing Multi-Step Reasoning Abilities of Language Models through Direct Q-Function Optimization [49.362750475706235]
  強化学習(Reinforcement Learning, RL)は、大規模言語モデルを人間の好みと整合させ、複雑なタスクを遂行する能力を向上させる上で重要な役割を担っている。 反応生成過程をマルコフ決定プロセス(MDP)として定式化し,ソフトアクター・クリティック(SAC)フレームワークを用いて,言語モデルによって直接パラメータ化されたQ関数を最適化する,直接Q関数最適化(DQO)を提案する。 GSM8KとMATHという2つの数学問題解決データセットの実験結果から、DQOは従来の手法よりも優れており、言語モデルを整合させるための有望なオフライン強化学習手法として確立されている。
  論文  参考訳（メタデータ） (2024-10-11T23:29:20Z)
• Strategic Chain-of-Thought: Guiding Accurate Reasoning in LLMs through Strategy Elicitation [16.350747493026432]
  CoT(Chain-of-Thought)パラダイムは,大規模言語モデル(LLM)の推論能力向上のための重要なアプローチとして登場した。 中間的推論ステップを生成する前に戦略的知識を統合することでLCM性能を向上するための textbfStrategic Chain-of-Thought (SCoT) を提案する。 SCoTは1つのプロンプトの中で2段階のアプローチを採用し、まず効果的な問題解決戦略を導き、次に高品質なCoTパスと最終回答の生成を導くのに使用される。
  論文  参考訳（メタデータ） (2024-09-05T06:28:05Z)

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

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