MPS-Prover: Fortschritt im schrittweisen Theorembeweis durch Multi-Perspektiven-Suche und Datenkuratierung

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

May 16, 2025

papers.authors: Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, Dong Yu

cs.AI

papers.abstract

Das Automatisierte Theorembeweisen (ATP) in formalen Sprachen bleibt eine gewaltige Herausforderung in der KI, die strenge logische Deduktion und die Navigation durch riesige Suchräume erfordert. Während große Sprachmodelle (LLMs) vielversprechende Leistungen gezeigt haben, leiden bestehende schrittweise Beweiser oft unter voreingenommener Suchführung, was zu Ineffizienzen und suboptimalen Beweisstrategien führt. Dieses Papier stellt den Multi-Perspective Search Prover (MPS-Prover) vor, ein neuartiges schrittweises ATP-System, das entwickelt wurde, um diese Einschränkungen zu überwinden. MPS-Prover integriert zwei Schlüsselinnovationen: eine hocheffektive Strategie zur Nachbearbeitung von Trainingsdaten, die etwa 40 % der redundanten Trainingsdaten entfernt, ohne die Leistung zu beeinträchtigen, und einen mehrperspektivischen Baum-Suchmechanismus. Diese Suche kombiniert ein gelerntes Kritikermodell mit strategisch entworfenen heuristischen Regeln, um die Taktikauswahl zu diversifizieren, das Feststecken in unproduktiven Zuständen zu verhindern und die Robustheit der Suche zu erhöhen. Umfangreiche Auswertungen zeigen, dass MPS-Prover auf mehreren anspruchsvollen Benchmarks, einschließlich miniF2F und ProofNet, Spitzenleistungen erzielt und dabei frühere Modelle mit 7B Parametern übertrifft. Darüber hinaus zeigen unsere Analysen, dass MPS-Prover deutlich kürzere und vielfältigere Beweise im Vergleich zu bestehenden schrittweisen und gesamten Beweismethoden generiert, was seine Effizienz und Wirksamkeit unterstreicht. Unsere Arbeit erweitert die Fähigkeiten des formalen Denkens auf Basis von LLMs und bietet einen robusten Rahmen sowie eine umfassende Analyse für die Entwicklung leistungsfähigerer Theorembeweiser.

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.