Seed-Prover 1.5: Padroneggiare la Dimostrazione di Teoremi a Livello Universitario attraverso l'Apprendimento dall'Esperienza

Abstract

I modelli linguistici di grandi dimensioni hanno recentemente compiuto progressi significativi nella generazione di dimostrazioni matematiche rigorose. Al contrario, l'utilizzo di LLM per la dimostrazione di teoremi in linguaggi formali (come Lean) rimane impegnativo e computazionalmente costoso, in particolare quando si affrontano problemi di livello universitario e superiori. In questo lavoro, presentiamo Seed-Prover 1.5, un modello per la dimostrazione formale di teoremi addestrato tramite apprendimento per rinforzo agente su larga scala, affiancato da un flusso di lavoro efficiente di scalatura al tempo di test (TTS). Attraverso interazioni estensive con Lean e altri strumenti, il modello accumula continuamente esperienza durante il processo di RL, migliorando sostanzialmente la capacità e l'efficienza della dimostrazione formale di teoremi. Inoltre, sfruttando i recenti progressi nella dimostrazione in linguaggio naturale, il nostro flusso di lavoro TTS colma efficientemente il divario tra linguaggi naturali e formali. Rispetto ai metodi all'avanguardia, Seed-Prover 1.5 raggiunge prestazioni superiori con un budget computazionale inferiore. Risolve l'88% dei problemi di PutnamBench (livello universitario), l'80% di Fate-H (livello magistrale) e il 33% di Fate-X (livello dottorale). Notevolmente, utilizzando il nostro sistema, abbiamo risolto 11 dei 12 problemi del Putnam 2025 in meno di 9 ore. I nostri risultati suggeriscono che la scalabilità dell'apprendimento dall'esperienza, guidato da feedback formale di alta qualità, detiene un immenso potenziale per il futuro del ragionamento matematico formale.

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: Padroneggiare la Dimostrazione di Teoremi a Livello Universitario attraverso l'Apprendimento dall'Esperienza

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

Abstract

Support