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

초록

LLM(대형 언어 모델)은 장기 사고 체인(long chain-of-thought)을 활용한 강화 학습을 통해 강력한 수학적 추론 능력을 보여주었으나, 자연어만을 사용할 때 명확한 감독 신호가 부족하여 정리 증명(theorem proving)에는 여전히 어려움을 겪고 있습니다. Lean과 같은 전용 도메인 특화 언어는 형식적 검증을 통해 명확한 감독을 제공하며, 이를 통해 강화 학습을 통한 효과적인 훈련이 가능합니다. 본 연구에서는 Seed-Prover라는 보조 정리(lemma) 스타일의 전체 증명 추론 모델을 제안합니다. Seed-Prover는 Lean의 피드백, 증명된 보조 정리, 그리고 자기 요약(self-summarization)을 기반으로 반복적으로 증명을 개선할 수 있습니다. IMO(국제 수학 올림피아드) 수준의 문제를 해결하기 위해, 우리는 깊고 넓은 추론을 가능하게 하는 세 가지 테스트 시 추론 전략을 설계했습니다. Seed-Prover는 형식화된 과거 IMO 문제의 78.1%를 증명하고, MiniF2F를 포화시키며, PutnamBench에서 50% 이상의 성적을 달성하여 기존 최신 기술을 크게 능가합니다. Lean에서 기하학 지원이 부족한 문제를 해결하기 위해, 우리는 Seed-Geometry라는 기하학 추론 엔진을 도입했으며, 이는 기존의 형식적 기하학 엔진을 능가하는 성능을 보여줍니다. 우리는 이 두 시스템을 사용하여 IMO 2025에 참가하여 6문제 중 5문제를 완전히 증명했습니다. 이 연구는 자동화된 수학적 추론에서의 중요한 진전을 나타내며, 장기 사고 체인 추론과 형식적 검증의 효과를 입증합니다.

English

LLMs have demonstrated strong mathematical reasoning abilities by leveraging reinforcement learning with long chain-of-thought, yet they continue to struggle with theorem proving due to the lack of clear supervision signals when solely using natural language. Dedicated domain-specific languages like Lean provide clear supervision via formal verification of proofs, enabling effective training through reinforcement learning. In this work, we propose Seed-Prover, a lemma-style whole-proof reasoning model. Seed-Prover can iteratively refine its proof based on Lean feedback, proved lemmas, and self-summarization. To solve IMO-level contest problems, we design three test-time inference strategies that enable both deep and broad reasoning. Seed-Prover proves 78.1% of formalized past IMO problems, saturates MiniF2F, and achieves over 50\% on PutnamBench, outperforming the previous state-of-the-art by a large margin. To address the lack of geometry support in Lean, we introduce a geometry reasoning engine Seed-Geometry, which outperforms previous formal geometry engines. We use these two systems to participate in IMO 2025 and fully prove 5 out of 6 problems. This work represents a significant advancement in automated mathematical reasoning, demonstrating the effectiveness of formal verification with long chain-of-thought reasoning.

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

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

초록

Support