MPS-Prover: Avanzando en la demostración de teoremas paso a paso mediante búsqueda multiperspectiva y curación de datos

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

May 16, 2025

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

cs.AI

Resumen

La Demostración Automática de Teoremas (ATP) en lenguajes formales sigue siendo un desafío formidable en la IA, que exige deducción lógica rigurosa y la navegación por vastos espacios de búsqueda. Si bien los modelos de lenguaje de gran escala (LLMs) han mostrado un rendimiento prometedor, los demostradores paso a paso existentes a menudo sufren de una guía de búsqueda sesgada, lo que conduce a ineficiencias y estrategias de demostración subóptimas. Este artículo presenta el Multi-Perspective Search Prover (MPS-Prover), un novedoso sistema de ATP paso a paso diseñado para superar estas limitaciones. MPS-Prover incorpora dos innovaciones clave: una estrategia altamente efectiva de curación de datos post-entrenamiento que elimina aproximadamente el 40% de los datos de entrenamiento redundantes sin sacrificar el rendimiento, y un mecanismo de búsqueda en árbol multi-perspectiva. Esta búsqueda integra un modelo crítico aprendido con reglas heurísticas estratégicamente diseñadas para diversificar la selección de tácticas, evitar quedar atrapado en estados improductivos y mejorar la robustez de la búsqueda. Evaluaciones exhaustivas demuestran que MPS-Prover alcanza un rendimiento de vanguardia en múltiples benchmarks desafiantes, incluyendo miniF2F y ProofNet, superando a modelos previos de 7B parámetros. Además, nuestros análisis revelan que MPS-Prover genera demostraciones significativamente más cortas y diversas en comparación con los métodos paso a paso y de demostración completa existentes, destacando su eficiencia y eficacia. Nuestro trabajo avanza las capacidades del razonamiento formal basado en LLMs y ofrece un marco robusto y un análisis exhaustivo para desarrollar demostradores de teoremas más potentes.

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.