# LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction

### 저자

Suozhi Huang, Peiyang Song, Robert Joseph George, Anima Anandkumar

### 개요

본 논문은 대규모 언어 모델(LLM)이 수학적 추론에서 겪는 어려움, 특히 환각(hallucination) 문제를 해결하기 위해 Lean과 같은 형식적 증명 보조기를 활용하는 방법을 제시합니다.  Lean과 LLM을 결합하면 신뢰할 수 있는 정리 증명이 가능하지만, 긴 증명과 복잡한 수학적 형식화에는 여전히 어려움을 겪습니다.  본 논문에서는 LeanProgress라는 방법을 제시하여 증명 과정의 진행 상황을 예측합니다. Lean Workbook Plus와 Mathlib4의 대규모 Lean 증명 데이터셋을 사용하여 모델을 학습 및 평가하였으며, 증명 길이의 불균형 분포를 해결하기 위해 데이터 전처리 및 균형 조정 기법을 적용했습니다. 실험 결과, LeanProgress는 증명 진행 상황 및 남은 단계 수 예측에서 75.1%의 정확도를 달성하였으며, Reprover를 사용한 최선우선탐색 프레임워크에 통합하여 Mathlib4에서 기준 성능(41.2%) 대비 3.8% 향상된 성능을 보였습니다. 특히 긴 증명에서 효과적임을 확인했습니다.

### 시사점, 한계점

- **시사점:**

    - LLM 기반 자동 정리 증명 시스템의 효율성 향상: 증명 진행 상황 예측을 통해 사용자는 증명 전략에 대한 더욱 정보에 입각한 결정을 내릴 수 있습니다.

    - 자동 및 대화형 정리 증명 모두에 적용 가능성 제시:  LeanProgress는 자동화된 시스템과 사용자 상호작용 시스템 모두에서 효과적으로 활용될 수 있습니다.

    - 긴 증명 문제 해결에 대한 실질적인 해결책 제시:  특히 긴 증명에서 기존 방식 대비 성능 향상을 보임으로써 실제 문제 해결에 기여합니다.

- **한계점:**

    - 75.1%의 예측 정확도는 완벽하지 않으며, 더 높은 정확도를 위한 추가 연구가 필요합니다.

    - 특정 데이터셋(Lean Workbook Plus, Mathlib4)에 대한 학습 결과이므로, 다른 데이터셋으로의 일반화 가능성에 대한 추가 검증이 필요합니다.

    - 복잡한 수학적 형식화에 대한 증명 진행 예측의 정확도는 추가 연구를 통해 검증되어야 합니다.

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

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

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