MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective
  Search and Data Curation
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.
682ab4fe7a9f1a7ec9779dd6
Zhenwen Liang
admin_assigned
2025-05-19T07:24:26.692Z
62ffa3f8311cad266f9af236
/avatars/203dac40bc546ee25a01d8715a4b3049.svg
Zhenwen Liang
user
invokerliang
682ab4fe7a9f1a7ec9779dd7
Linfeng Song
admin_assigned
2025-05-19T07:24:45.999Z
64c94eddcb2f1bf0e7db5a4d
/avatars/f7e2532d3c85d5e5b5a02c579ea68c3a.svg
Linfeng Song
user
freesunshine0316
682ab4fe7a9f1a7ec9779dd8
Yang Li
682ab4fe7a9f1a7ec9779dd9
Tao Yang
682ab4fe7a9f1a7ec9779dda
Feng Zhang
682ab4fe7a9f1a7ec9779ddb
Haitao Mi
admin_assigned
2025-05-19T07:24:56.781Z
65147a1426fbd558dbd08f1b
/avatars/86574ee2d5c22e940be1c4e50be88675.svg
Haitao Mi
user
haitaominlp
682ab4fe7a9f1a7ec9779ddc
Dong Yu
MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective
  Search and Data Curation
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.
MPS-Prover, a novel stepwise ATP system, improves proof efficiency and quality through data curation and a multi-perspective tree search mechanism combining learned critics and heuristic rules.
Automated Theorem Proving Large Language Models stepwise provers post-training data curation multi-perspective tree search learned critic model heuristic rules miniF2F ProofNet