MPS-Prover：多視点探索とデータキュレーションによる段階的定理証明の進展

MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation

May 16, 2025

著者: Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, Dong Yu

cs.AI

要旨

形式言語における自動定理証明（Automated Theorem Proving, ATP）は、AI分野において依然として大きな課題であり、厳密な論理的推論と広大な探索空間のナビゲーションを要求します。大規模言語モデル（LLMs）は有望な性能を示していますが、既存の段階的証明器はしばしば偏った探索ガイダンスに悩まされ、非効率性や最適でない証明戦略を引き起こしています。本論文では、これらの制限を克服するために設計された新しい段階的ATPシステムであるMulti-Perspective Search Prover（MPS-Prover）を紹介します。MPS-Proverは、2つの重要な革新を組み込んでいます。1つ目は、性能を損なうことなく冗長なトレーニングデータの約40%を削減する非常に効果的なポストトレーニングデータキュレーション戦略です。2つ目は、多視点木探索メカニズムです。この探索は、学習された批評モデルと戦略的に設計されたヒューリスティックルールを統合し、戦略選択を多様化し、非生産的な状態に陥るのを防ぎ、探索の堅牢性を向上させます。広範な評価により、MPS-ProverがminiF2FやProofNetを含む複数の挑戦的なベンチマークで最先端の性能を達成し、従来の7Bパラメータモデルを上回ることが示されています。さらに、我々の分析により、MPS-Proverが既存の段階的および全体証明法と比較して、大幅に短く多様な証明を生成することが明らかになり、その効率性と有効性が強調されています。我々の研究は、LLMベースの形式的推論の能力を向上させ、より強力な定理証明器を開発するための堅牢なフレームワークと包括的な分析を提供します。

English

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.