시드-프루버 1.5: 경험 학습을 통한 학부 수준 정리 증명 숙달

초록

최근 대규모 언어 모델이 엄밀한 수학적 증명을 생성하는 데 상당한 진전을 보였습니다. 이와 대조적으로, LLM을 형식 언어(예: Lean)에서의 정리 증명에 활용하는 것은 학부 수준 이상의 문제를 다룰 때 여전히 어렵고 계산 비용이 많이 듭니다. 본 연구에서는 대규모 에이전트 강화 학습을 통해 훈련된 형식 정리 증명 모델인 Seed-Prover 1.5와 효율적인 테스트 타임 스케일링(TTS) 워크플로를 제시합니다. Lean 및 기타 도구와의 광범위한 상호작용을 통해 모델은 RL 과정 동안 지속적으로 경험을 축적하여 형식 정리 증명의 능력과 효율성을 크게 향상시킵니다. 더 나아가, 자연어 증명 분야의 최근 발전을 활용한 우리의 TTS 워크플로는 자연어와 형식 언어 간의 격차를 효율적으로 연결합니다. 최첨단 방법론과 비교했을 때, Seed-Prover 1.5는 더 적은 계산 예산으로도 우수한 성능을 달성합니다. 이 모델은 PutnamBench(학부 수준) 문제의 88%, Fate-H(대학원 수준) 문제의 80%, Fate-X(박사 수준) 문제의 33%를 해결했습니다. 특히, 우리 시스템을 사용하여 2025년 Putnam 문제 12개 중 11개를 9시간 이내에 해결했습니다. 우리의 연구 결과는 고품질의 형식적 피드백에 의해 주도되는 경험 기반 학습의 확장이 형식적 수학적 추론의 미래에 막대한 잠재력을 지니고 있음을 시사합니다.

English

Large language models have recently made significant progress to generate rigorous mathematical proofs. In contrast, utilizing LLMs for theorem proving in formal languages (such as Lean) remains challenging and computationally expensive, particularly when addressing problems at the undergraduate level and beyond. In this work, we present Seed-Prover 1.5, a formal theorem-proving model trained via large-scale agentic reinforcement learning, alongside an efficient test-time scaling (TTS) workflow. Through extensive interactions with Lean and other tools, the model continuously accumulates experience during the RL process, substantially enhancing the capability and efficiency of formal theorem proving. Furthermore, leveraging recent advancements in natural language proving, our TTS workflow efficiently bridges the gap between natural and formal languages. Compared to state-of-the-art methods, Seed-Prover 1.5 achieves superior performance with a smaller compute budget. It solves 88\% of PutnamBench (undergraduate-level), 80\% of Fate-H (graduate-level), and 33\% of Fate-X (PhD-level) problems. Notably, using our system, we solved 11 out of 12 problems from Putnam 2025 within 9 hours. Our findings suggest that scaling learning from experience, driven by high-quality formal feedback, holds immense potential for the future of formal mathematical reasoning.

시드-프루버 1.5: 경험 학습을 통한 학부 수준 정리 증명 숙달

Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience

초록

Support