Seed-Prover 1.5 : Maîtriser la démonstration de théorèmes de niveau licence par l'apprentissage à partir de l'expérience

papers.abstract

Les grands modèles linguistiques ont récemment accompli des progrès significatifs dans la génération de preuves mathématiques rigoureuses. En revanche, l'utilisation des LLM pour la démonstration de théorèmes dans des langages formels (comme Lean) reste difficile et coûteuse en calcul, particulièrement pour des problèmes de niveau licence et au-delà. Dans ce travail, nous présentons Seed-Prover 1.5, un modèle de démonstration de théorèmes formels entraîné par apprentissage par renforcement agentique à grande échelle, ainsi qu'un flux de travail efficace de mise à l'échelle au moment du test (TTS). Grâce à des interactions approfondies avec Lean et d'autres outils, le modèle accumule continuellement de l'expérience durant le processus d'apprentissage par renforcement, améliorant substantiellement la capacité et l'efficacité de la démonstration formelle. De plus, en tirant parti des avancées récentes en démonstration en langage naturel, notre flux de travail TTS comble efficacement le fossé entre les langages naturels et formels. Comparé aux méthodes de l'état de l'art, Seed-Prover 1.5 obtient des performances supérieures avec un budget de calcul réduit. Il résout 88 % des problèmes de PutnamBench (niveau licence), 80 % de ceux de Fate-H (niveau master) et 33 % de ceux de Fate-X (niveau doctorat). Fait notable, en utilisant notre système, nous avons résolu 11 des 12 problèmes du Putnam 2025 en moins de 9 heures. Nos résultats suggèrent que la mise à l'échelle de l'apprentissage par l'expérience, guidée par un retour formel de haute qualité, recèle un immense potentiel pour l'avenir du raisonnement mathématique formel.

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.

Seed-Prover 1.5 : Maîtriser la démonstration de théorèmes de niveau licence par l'apprentissage à partir de l'expérience

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

papers.abstract

Support