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

초록

형식 언어에서의 자동 정리 증명(Automated Theorem Proving, ATP)은 여전히 AI 분야에서 해결해야 할 중요한 과제로, 엄격한 논리적 추론과 방대한 탐색 공간을 요구합니다. 대규모 언어 모델(LLMs)이 유망한 성능을 보여주고 있지만, 기존의 단계별 증명기는 편향된 탐색 지도로 인해 비효율적이고 최적이 아닌 증명 전략을 보이는 경우가 많습니다. 본 논문은 이러한 한계를 극복하기 위해 설계된 새로운 단계별 ATP 시스템인 다중 관점 탐색 증명기(Multi-Perspective Search Prover, MPS-Prover)를 소개합니다. MPS-Prover는 두 가지 주요 혁신을 도입했습니다: 첫째, 성능 저하 없이 약 40%의 중복 훈련 데이터를 제거하는 고효율의 사후 훈련 데이터 정제 전략, 둘째, 다중 관점 트리 탐색 메커니즘입니다. 이 탐색 메커니즘은 학습된 비평 모델과 전략적으로 설계된 휴리스틱 규칙을 통합하여 전술 선택을 다양화하고, 비생산적인 상태에 빠지는 것을 방지하며, 탐색의 견고성을 강화합니다. 광범위한 평가 결과, MPS-Prover는 miniF2F와 ProofNet을 포함한 여러 도전적인 벤치마크에서 최신 기술을 능가하는 성능을 달성하며, 기존의 7B 파라미터 모델들을 능가함을 보여줍니다. 또한, 분석 결과 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.