MPS-Prover: Avançando a Prova de Teoremas Passo a Passo por Meio de Busca Multi-Perspectiva e Curadoria de Dados

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

Resumo

A Prova Automática de Teoremas (ATP) em linguagens formais continua sendo um desafio formidável na IA, exigindo dedução lógica rigorosa e a navegação por vastos espaços de busca. Embora os grandes modelos de linguagem (LLMs) tenham demonstrado desempenho promissor, os provadores passo a passo existentes frequentemente sofrem com orientação de busca tendenciosa, levando a ineficiências e estratégias de prova subótimas. Este artigo apresenta o MPS-Prover, um novo sistema de ATP passo a passo projetado para superar essas limitações. O MPS-Prover incorpora duas inovações principais: uma estratégia altamente eficaz de curadoria de dados pós-treinamento que elimina aproximadamente 40% dos dados de treinamento redundantes sem sacrificar o desempenho, e um mecanismo de busca em árvore de múltiplas perspectivas. Essa busca integra um modelo crítico aprendido com regras heurísticas estrategicamente projetadas para diversificar a seleção de táticas, evitar ficar preso em estados improdutivos e aumentar a robustez da busca. Avaliações extensivas demonstram que o MPS-Prover alcança desempenho de ponta em vários benchmarks desafiadores, incluindo miniF2F e ProofNet, superando modelos anteriores com 7 bilhões de parâmetros. Além disso, nossas análises revelam que o MPS-Prover gera provas significativamente mais curtas e diversas em comparação com métodos passo a passo e de prova completa existentes, destacando sua eficiência e eficácia. Nosso trabalho avança as capacidades do raciocínio formal baseado em LLM e oferece uma estrutura robusta e uma análise abrangente para o desenvolvimento de provadores de teoremas mais poderosos.

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.