MPS-Prover: Vooruitgang in Stapsgewijs Bewijzen door Multi-Perspectief Zoeken en Dataverwerking

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

May 16, 2025

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

cs.AI

Samenvatting

Geautomatiseerd Bewijzen van Stellingen (Automated Theorem Proving, ATP) in formele talen blijft een formidabele uitdaging in AI, waarbij rigoureuze logische deductie en het navigeren door enorme zoekruimten vereist zijn. Hoewel grote taalmmodellen (Large Language Models, LLMs) veelbelovende prestaties hebben getoond, kampen bestaande stapsgewijze bewijssystemen vaak met bevooroordeelde zoekbegeleiding, wat leidt tot inefficiënties en suboptimale bewijsstrategieën. Dit artikel introduceert de Multi-Perspective Search Prover (MPS-Prover), een nieuw stapsgewijs ATP-systeem dat ontworpen is om deze beperkingen te overwinnen. MPS-Prover bevat twee belangrijke innovaties: een zeer effectieve strategie voor het cureren van post-trainingsdata die ongeveer 40% van de redundante trainingsdata verwijdert zonder prestaties te verliezen, en een multi-perspectief boomzoekmechanisme. Dit zoekmechanisme integreert een geleerd criticusmodel met strategisch ontworpen heuristische regels om de selectie van tactieken te diversifiëren, te voorkomen dat het systeem vastloopt in onproductieve staten, en de robuustheid van het zoeken te vergroten. Uitgebreide evaluaties tonen aan dat MPS-Prover state-of-the-art prestaties behaalt op meerdere uitdagende benchmarks, waaronder miniF2F en ProofNet, en daarbij eerdere modellen met 7B parameters overtreft. Bovendien laten onze analyses zien dat MPS-Prover aanzienlijk kortere en meer diverse bewijzen genereert in vergelijking met bestaande stapsgewijze en hele-bewijs methoden, wat de efficiëntie en effectiviteit ervan benadrukt. Ons werk bevordert de mogelijkheden van LLM-gebaseerd formeel redeneren en biedt een robuust raamwerk en een uitgebreide analyse voor het ontwikkelen van krachtigere bewijssystemen.

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.