MPS-Prover: Avanzare nella dimostrazione di teoremi passo-passo attraverso la ricerca multi-prospettica e la cura dei dati

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

May 16, 2025

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

cs.AI

Abstract

Il ragionamento automatico (Automated Theorem Proving, ATP) nei linguaggi formali rimane una sfida formidabile nell'ambito dell'IA, richiedendo deduzione logica rigorosa e la navigazione in vasti spazi di ricerca. Sebbene i grandi modelli linguistici (Large Language Models, LLMs) abbiano mostrato prestazioni promettenti, i dimostratori passo-passo esistenti spesso soffrono di una guida di ricerca distorta, portando a inefficienze e strategie di dimostrazione subottimali. Questo articolo introduce il Multi-Perspective Search Prover (MPS-Prover), un innovativo sistema ATP passo-passo progettato per superare questi limiti. MPS-Prover incorpora due innovazioni chiave: una strategia di curatela dei dati post-addestramento altamente efficace che elimina circa il 40% dei dati di addestramento ridondanti senza compromettere le prestazioni, e un meccanismo di ricerca ad albero multi-prospettica. Questa ricerca integra un modello critico appreso con regole euristiche progettate strategicamente per diversificare la selezione delle tattiche, prevenire il blocco in stati improduttivi e migliorare la robustezza della ricerca. Valutazioni estensive dimostrano che MPS-Prover raggiunge prestazioni all'avanguardia su molteplici benchmark impegnativi, tra cui miniF2F e ProofNet, superando i precedenti modelli con 7 miliardi di parametri. Inoltre, le nostre analisi rivelano che MPS-Prover genera dimostrazioni significativamente più brevi e diversificate rispetto ai metodi passo-passo e a dimostrazione completa esistenti, evidenziandone l'efficienza e l'efficacia. Il nostro lavoro avanza le capacità del ragionamento formale basato su LLM e offre un framework robusto e un'analisi completa per lo sviluppo di dimostratori di teoremi più potenti.

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.