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

### 저자

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의 가능성을 보여준다.

    - 효율적인 훈련 데이터 관리 전략 제시:  중복 데이터 제거를 통한 효율적인 훈련 데이터 관리 방법을 제시한다.

    - 다양하고 짧은 증명 생성: 기존 방법보다 더 짧고 다양한 증명을 생성하여 증명의 효율성과 효과성을 높였다.

    - 강력한 정리 증명기 개발을 위한 견고한 프레임워크 제공

- **한계점:**

    - 본 논문에서 제시된 방법의 일반화 가능성에 대한 추가적인 연구가 필요하다.

    - 다른 종류의 정리 증명 문제에 대한 성능 평가가 추가적으로 필요하다.

    - 사용된 휴리스틱 규칙의 일반성 및 적용 가능성에 대한 추가적인 분석이 필요하다.

[PDF 보기](https://arxiv.org/pdf/2505.10962)

![https://i.imgur.com/ZSwmDUt.jpeg](https://i.imgur.com/ZSwmDUt.jpeg)

For the site tree, see the [root Markdown](https://slashpage.com/haebom.md).