MPS-Prover : Faire progresser la démonstration de théorèmes pas à pas grâce à une recherche multiperspective et à une curation des données

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

Résumé

La démonstration automatique de théorèmes (ATP) dans les langages formels reste un défi majeur en IA, nécessitant une déduction logique rigoureuse et la navigation dans des espaces de recherche vastes. Bien que les grands modèles de langage (LLM) aient montré des performances prometteuses, les prouveurs pas à pas existants souffrent souvent d'un guidage de recherche biaisé, entraînant des inefficacités et des stratégies de preuve sous-optimales. Cet article présente le Multi-Perspective Search Prover (MPS-Prover), un nouveau système ATP pas à pas conçu pour surmonter ces limitations. MPS-Prover intègre deux innovations clés : une stratégie de curation de données post-entraînement très efficace qui élimine environ 40 % des données d'entraînement redondantes sans compromettre les performances, et un mécanisme de recherche arborescente multi-perspectives. Cette recherche intègre un modèle critique appris avec des règles heuristiques stratégiquement conçues pour diversifier la sélection de tactiques, éviter de rester bloqué dans des états improductifs et renforcer la robustesse de la recherche. Des évaluations approfondies démontrent que MPS-Prover atteint des performances de pointe sur plusieurs benchmarks exigeants, notamment miniF2F et ProofNet, surpassant les modèles précédents à 7 milliards de paramètres. De plus, nos analyses révèlent que MPS-Prover génère des preuves significativement plus courtes et plus diversifiées par rapport aux méthodes pas à pas et de preuve complète existantes, mettant en évidence son efficacité et son efficience. Notre travail fait progresser les capacités du raisonnement formel basé sur les LLM et propose un cadre robuste ainsi qu'une analyse complète pour développer des prouveurs de théorèmes plus puissants.

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.