MPS-Prover: Усовершенствование пошагового доказательства теорем с помощью многоперспективного поиска и курирования данных

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

May 16, 2025

Авторы: Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, Dong Yu

cs.AI

Аннотация

Автоматическое доказательство теорем (ATP) в формальных языках остается серьезной проблемой в области ИИ, требующей строгого логического вывода и навигации в обширных пространствах поиска. Хотя крупные языковые модели (LLM) продемонстрировали многообещающие результаты, существующие пошаговые системы доказательств часто страдают от предвзятого управления поиском, что приводит к неэффективности и субоптимальным стратегиям доказательства. В данной статье представлен Multi-Perspective Search Prover (MPS-Prover) — новая пошаговая система ATP, разработанная для преодоления этих ограничений. MPS-Prover включает два ключевых нововведения: высокоэффективную стратегию посттренировочной обработки данных, которая сокращает около 40% избыточных обучающих данных без ущерба для производительности, и механизм поиска с использованием множественных перспектив. Этот поиск интегрирует обученную модель-критика с стратегически разработанными эвристическими правилами для диверсификации выбора тактик, предотвращения застревания в непродуктивных состояниях и повышения устойчивости поиска. Обширные оценки показывают, что MPS-Prover достигает наилучших результатов на нескольких сложных тестовых наборах, включая miniF2F и ProofNet, превосходя предыдущие модели с 7 миллиардами параметров. Кроме того, наши анализы показывают, что MPS-Prover генерирует значительно более короткие и разнообразные доказательства по сравнению с существующими пошаговыми и целостными методами, подчеркивая его эффективность и результативность. Наша работа расширяет возможности формального рассуждения на основе LLM и предлагает надежную структуру и всесторонний анализ для разработки более мощных систем доказательства теорем.

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.