MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
Created by
Haebom
저자
Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, Dong Yu
개요
본 논문은 자동 정리 증명(ATP)에서 대규모 언어 모델(LLM)의 한계를 극복하기 위해 다중 관점 탐색 증명기(MPS-Prover)를 제안한다. MPS-Prover는 훈련 데이터의 40%를 제거하는 데이터 정제 전략과 학습된 평가 모델과 휴리스틱 규칙을 통합한 다중 관점 트리 탐색 메커니즘을 통해 효율적인 정리 증명을 수행한다. miniF2F와 ProofNet 벤치마크에서 기존 7B 파라미터 모델들을 능가하는 성능을 보이며, 더 짧고 다양한 증명을 생성하는 것을 실험적으로 보였다.
시사점, 한계점
•
시사점:
◦
LLM 기반 형식적 추론의 성능 향상: MPS-Prover는 기존 방법보다 우수한 성능을 보이며, LLM 기반 ATP의 가능성을 보여준다.
◦
효율적인 훈련 데이터 관리 전략 제시: 중복 데이터 제거를 통한 효율적인 훈련 데이터 관리 방법을 제시한다.
◦
다양하고 짧은 증명 생성: 기존 방법보다 더 짧고 다양한 증명을 생성하여 증명의 효율성과 효과성을 높였다.
