# OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving

### 저자

Chenyi Li, Yanchen Nie, Zhenyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen

### 💡 개요

본 연구는 올림피아드 수준의 수학 증명에서 훈련된 모델을 사용하여 머신러닝, 운영 연구 등 다양한 분야의 기초가 되는 최적화 문제 해결 능력을 향상시키는 OptProver를 제안합니다. 기존 방법론으로는 다루기 어려웠던 최적화의 특화된 형식주의로 인한 분포 이동 문제를 해결하기 위해, 대규모 최적화 관련 데이터 큐레이션과 탐색 효율성을 높이는 선호 학습 목표를 도입했습니다. 제안된 방법은 새로운 최적화 벤치마크에서 최첨단 성능을 달성했으며, 일반적인 정리 증명 능력 또한 유지함을 보여줍니다.

### 🔑 시사점 및 한계

- 인공지능 모델의 훈련 범위를 올림피아드 수학에서 실제 응용이 중요한 최적화 분야로 성공적으로 확장했습니다.

- 분포 이동 문제를 해결하고 효율적인 증명 탐색을 유도하는 두 가지 핵심 혁신(데이터 큐레이션 및 선호 학습)은 AI 모델의 일반화 및 성능 향상에 기여합니다.

- 향후 과제로는 더욱 복잡하고 다양한 최적화 문제를 다루기 위한 벤치마크 확장 및 모델 성능 고도화가 필요합니다.

---

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

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