DeepSeekMath-V2 : l’IA qui prouve les maths d’olympiade avec auto-vérification

DeepSeek AI a lancé DeepSeekMath-V2, un large modèle de langage (LLM) de 685 milliards de paramètres conçu pour résoudre et prouver des problèmes mathématiques d’un niveau olympique en langage naturel, tout en s’auto-vérifiant. Basé sur DeepSeek-V3.2-Exp-Base, ce modèle open source sous licence Apache 2.0 est accessible sur Hugging Face. Il se distingue par sa capacité à générer des preuves rigoureuses et à contrôler la validité de son raisonnement, une avancée majeure dans le domaine de la démonstration automatique.

Une approche innovante centrée sur la qualité des preuves

Contrairement aux modèles précédents qui se focalisent sur la récompense du résultat final, DeepSeekMath-V2 optimise la qualité des preuves mathématiques. En effet, un résultat numérique correct ne garantit pas un raisonnement sans erreur, surtout dans les démonstrations complexes où une argumentation complète en langage naturel est requise. Pour pallier ce problème, l’équipe de recherche a développé un système de vérification en deux étapes : un vérificateur principal et un méta-vérificateur.

Le vérificateur, entraîné via une méthode appelée Group Relative Policy Optimization (GRPO), analyse les preuves proposées, attribuant un score discret (0, 0.5 ou 1) basé sur la rigueur et la complétude. Ce système a été initialement formé sur plus de 17 000 problèmes issus de concours d’olympiades et tests post-2010 nécessitant des démonstrations détaillées, avec des annotations humaines pour calibrer la qualité.

Le méta-vérificateur intervient pour contrôler la fiabilité des critiques émises par le vérificateur, détectant les hallucinations ou incohérences dans les analyses. Cette double couche de contrôle améliore significativement la confiance dans les évaluations, avec une qualité moyenne des analyses passant de 0,85 à 0,96 selon les tests internes.

Un générateur de preuves auto-vérifiant et affiné en plusieurs passes

Une fois le vérificateur robuste, DeepSeekMath-V2 entraîne un générateur de preuves qui produit à la fois la démonstration et une auto-analyse selon la même grille d’évaluation. La récompense combinée intègre le score du vérificateur, la concordance entre l’auto-évaluation et le vérificateur, ainsi que la note du méta-vérificateur sur l’analyse.

Le modèle exploite également un contexte étendu de 128 000 tokens, permettant des raffinements séquentiels : il génère une preuve, l’analyse, puis corrige les erreurs détectées en plusieurs itérations. Cette boucle améliore la qualité finale des démonstrations, notamment sur les problèmes les plus complexes.

Performances remarquables sur les concours mathématiques internationaux

DeepSeekMath-V2 a été évalué sur plusieurs benchmarks prestigieux. Il atteint un niveau médaille d’or aux Olympiades Internationales de Mathématiques (IMO) 2025 en résolvant 5 des 6 problèmes, ainsi qu’aux Concours Mathématiques de l’Ontario (CMO) 2024 avec 4 problèmes entièrement résolus et un partiellement. Sur le Putnam 2024, il obtient 118 points sur 120, surpassant largement le meilleur score humain de 90.

Comparé à d’autres modèles de pointe comme Gemini 2.5 Pro ou GPT-5 Thinking High, DeepSeekMath-V2 affiche la meilleure moyenne de scores de preuve sur un ensemble interne de 91 problèmes couvrant divers domaines mathématiques. Sur le benchmark IMO ProofBench, il surpasse DeepMind DeepThink IMO Gold sur les problèmes basiques et reste compétitif sur les plus avancés.