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

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Liang, Zhenwen, Song, Linfeng, Li, Yang, Yang, Tao, Zhang, Feng, Mi, Haitao, Yu, Dong
Format:	Preprint
Published:	2025
Subjects:	Artificial Intelligence
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

_version_	1866909612406472704
author	Liang, Zhenwen Song, Linfeng Li, Yang Yang, Tao Zhang, Feng Mi, Haitao Yu, Dong
author_facet	Liang, Zhenwen Song, Linfeng Li, Yang Yang, Tao Zhang, Feng Mi, Haitao Yu, Dong
contents	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.
format	Preprint
id	arxiv_https___arxiv_org_abs_2505_10962
institution	arXiv
publishDate	2025
record_format	arxiv
spellingShingle	MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation Liang, Zhenwen Song, Linfeng Li, Yang Yang, Tao Zhang, Feng Mi, Haitao Yu, Dong Artificial Intelligence 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.
title	MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
topic	Artificial Intelligence
url	https://arxiv.org/abs/2505.10962