DeepSeek-Prover-V2 est un modèle de langage open source à grande échelle conçu pour la démonstration formelle de théorèmes en Lean 4. Il est initialisé avec des données collectées via un pipeline de démonstration récursif de théorèmes basé sur DeepSeek-V3. Il effectue un apprentissage à froid en exploitant la capacité de DeepSeek-V3 à décomposer des problèmes complexes en plusieurs sous-objectifs. Les preuves des sous-objectifs résolus sont combinées aux inférences étape par étape de DeepSeek-V3 afin de générer des données initiales pour l'apprentissage par renforcement. Cela intègre le raisonnement mathématique formel et informel. Le modèle résultant, DeepSeek-Prover-V2-671B, atteint des performances de pointe en démonstration de théorèmes sur réseaux neuronaux, avec un taux de réussite de 88,9 % au test MiniF2F et la résolution de 49 problèmes PutnamBench sur 658. Nous introduisons une nouvelle métrique, ProverBench (325 problèmes formalisés), qui inclut 15 problèmes du récent concours AIME (24-25). Les résultats de l'évaluation montrent qu'elle résout 6 des 15 problèmes AIME, ce qui démontre que l'écart entre raisonnement mathématique formel et informel est significativement réduit par rapport à la méthode de vote majoritaire de DeepSeek-V3 (qui résout 8 problèmes).
