DeepSeek-Prover-V2 : Faire progresser le raisonnement mathématique formel grâce à l'apprentissage par renforcement
DeepSeek-Prover-V2 est un grand modèle de langage open source conçu pour la démonstration formelle de théorèmes en Lean 4. Il utilise un pipeline de démonstration de théorèmes récursif alimenté par DeepSeek-V3 et l'apprentissage par renforcement pour intégrer le raisonnement mathématique informel et formel. Le modèle commence par décomposer les problèmes complexes en sous-objectifs à l'aide de DeepSeek-V3, synthétisant les preuves de ces sous-objectifs pour créer des données initiales pour l'apprentissage par renforcement. DeepSeek-Prover-V2-671B atteint des performances de pointe, atteignant un taux de réussite de 88,9 % sur MiniF2F-test et résolvant 49 problèmes de PutnamBench. Un nouvel ensemble de données de référence, ProverBench, contenant 325 problèmes formalisés issus de compétitions de lycée et de manuels scolaires, est également présenté.