시드-프로버: 자동 정리 증명을 위한 깊이 있고 광범위한 추론

대규모 언어모델(LLM)은 긴 사고 과정(chain-of-thought)을 활용한 강화학습을 통해 강력한 수학적 추론 능력을 보여왔으나, 자연어만을 사용할 경우 명확한 감독 신호가 부족하여 정리 증명 측면에서는 여전히 어려움을 겪고 있다. 리언(Lean)과 같은 전용 도메인 특화 언어는 증명의 형식적 검증을 통해 명확한 감독 신호를 제공함으로써, 강화학습을 통한 효과적인 학습을 가능하게 한다. 본 연구에서는 증명 단위의 전체 증명 추론 모델인 Seed-Prover를 제안한다. Seed-Prover는 리언의 피드백, 이미 증명된 보조정리, 그리고 자기 요약을 기반으로 반복적으로 증명을 개선할 수 있다. IMO 수준의 대회 문제를 해결하기 위해, 깊이 있는 추론과 넓은 범위의 추론을 동시에 가능하게 하는 세 가지 테스트 시점 추론 전략을 설계하였다. Seed-Prover는 형식화된 과거 IMO 문제의 78.1%를 증명하였으며, MiniF2F 데이터셋에서 포화 상태(saturation)를 달성하고, PutnamBench에서 50% 이상의 성능을 기록하며 기존 최고 성능 모델을 크게 능가하였다. 또한 리언이 기하학적 지원이 부족한 문제를 해결하기 위해, 기하학적 추론 엔진인 Seed-Geometry를 도입하였으며, 이는 기존의 형식적 기하학 엔진보다 우수한 성능을 보였다. 본 연구에서 제안한 두 시스템을 활용하여 2025년 IMO에 참가하였으며, 6문제 중 5문제를 완전히 증명하였다. 본 연구는 자동화된 수학적 추론 분야에서 중요한 진전을 보여주며, 긴 사고 과정과 함께 형식적 검증을 활용한 추론의 효과성을 입증하였다.