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

TL;DR

Automated theorem proving with large language models remains challenged by biased search and inefficient exploration in stepwise provers. The authors introduce MPS-Prover, combining a post-training data-curation strategy that prunes about $40\%$ of redundant data with a multi-perspective tree search that blends a learned critic with heuristic rules to diversify tactic selection. This approach yields state-of-the-art results on miniF2F and ProofNet within the $7$B parameter class, and produces significantly shorter and more diverse proofs than both stepwise and whole-proof baselines. The work demonstrates the value of integrating targeted data curation with diversified search signals, offering a robust framework for developing more powerful, data-efficient theorem provers and guiding future hybrid systems that blend stepwise and global planning strategies.

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.

Figures (4)

• Figure 1: Common failure patterns in step-based theorem provers. (a) Repetitive steps caused by critique model over-preference for specific tactics. (b) Unprovable states resulting from incorrect tactic choices that overly simplify conditions. (c) Ineffective tactic applications that fail to make progress.
• Figure 2: Search‑strategy comparison in Lean‑based proving. (a) Best‑First Search follows the single branch favoured by a learned critic; when that critic’s inherent bias selects an unprovable state or an ineffective tactic, the entire proof attempt terminates in failure. (b) Multi‑Perspective Search (MPS) evaluates each expansion step from heuristics as well as the critic, preserving a more diverse set of promising Lean 4 states and steering the prover around dead ends and toward a successful proof.
• Figure 3: Performance comparison under equivalent computational budgets.
• Figure 4: Quantitative analysis of proof characteristics for commonly solved problems by BFS (pass@256) and MPS (pass@64).