Les grands modèles linguistiques ont fait des progrès significatifs en raisonnement mathématique, domaine qui constitue un terrain d’expérimentation essentiel pour l’intelligence artificielle et pourrait avoir un impact important sur la recherche scientifique si ces avancées se poursuivent. En faisant évoluer le raisonnement grâce à un apprentissage par renforcement qui récompense uniquement les réponses finales correctes, les grands modèles linguistiques sont passés d’une performance médiocre à une saturation dans des compétitions quantitatives comme l’AIME et le HMMT en seulement un an. Toutefois, cette approche présente des limites fondamentales : une meilleure précision des réponses finales ne résout pas un problème clé — une réponse correcte ne garantit pas un raisonnement correct. En outre, de nombreuses tâches mathématiques, telles que la démonstration de théorèmes, exigent une dérivation rigoureuse étape par étape, plutôt que simplement une réponse numérique, rendant ainsi les récompenses basées sur la réponse finale inadaptées. Pour pousser les limites du raisonnement profond, nous pensons qu’il est nécessaire de vérifier la complétude et la rigueur du raisonnement mathématique. La vérification auto-suffisante est particulièrement cruciale pour exploiter efficacement les ressources de calcul disponibles au moment de l’évaluation (test-time compute), notamment dans le cas de problèmes ouverts pour lesquels aucune solution connue n’existe. Dans cette optique, nous étudions comment entraîner un vérificateur basé sur un grand modèle linguistique, précis et fiable, pour la démonstration de théorèmes. Nous entraînons ensuite un générateur de preuves en utilisant ce vérificateur comme modèle de récompense, en incitant ce générateur à identifier et à corriger autant d’erreurs que possible dans ses propres preuves avant de les finaliser. Afin de maintenir un écart entre génération et vérification même lorsque le générateur s’améliore, nous proposons d’augmenter la puissance de calcul dédiée à la vérification, afin d’étiqueter automatiquement de nouvelles preuves difficiles à vérifier, créant ainsi des données d’entraînement pour améliorer continuellement le vérificateur. Le modèle résultant, DeepSeekMath-V2, démontre des capacités remarquables en démonstration de théorèmes, obtenant des résultats de niveau « or » aux Olympiades internationales de mathématiques (IMO) 2025 et aux Olympiades chinoises de mathématiques (CMO) 2024, ainsi qu’un score quasi parfait de 118/120 à l’examens Putnam 2024, grâce à une utilisation élargie du calcul au moment de l’évaluation. Bien qu’un travail considérable reste à accomplir, ces résultats suggèrent que le raisonnement mathématique auto-vérifiable constitue une voie de recherche viable, susceptible d’aider à développer des systèmes d’intelligence artificielle mathématique plus performants.