DeepSeekMath-V2 : Vers un raisonnement mathématique auto-vérifiable
DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning
November 27, 2025
papers.authors: Zhihong Shao, Yuxiang Luo, Chengda Lu, Z. Z. Ren, Jiewen Hu, Tian Ye, Zhibin Gou, Shirong Ma, Xiaokang Zhang
cs.AI
papers.abstract
Les grands modèles linguistiques ont réalisé des progrès significatifs en raisonnement mathématique, qui sert de banc d'essai important pour l'IA et pourrait impacter la recherche scientifique s'il est davantage perfectionné. En augmentant l'échelle du raisonnement grâce à l'apprentissage par renforcement qui récompense les réponses finales correctes, les LLM sont passés de faibles performances à une saturation des compétitions de raisonnement quantitatif comme l'AIME et le HMMT en un an. Cependant, cette approche rencontre des limitations fondamentales. La recherche d'une plus grande précision des réponses finales ne résout pas un problème clé : des réponses correctes ne garantissent pas un raisonnement valide. De plus, de nombreuses tâches mathématiques comme la démonstration de théorèmes nécessitent une dérivation rigoureuse étape par étape plutôt que des réponses numériques, rendant les récompenses sur les réponses finales inapplicables. Pour repousser les limites du raisonnement profond, nous estimons nécessaire de vérifier l'exhaustivité et la rigueur du raisonnement mathématique. L'auto-vérification est particulièrement importante pour intensifier le calcul au moment du test, surtout pour les problèmes ouverts sans solutions connues. Vers un raisonnement mathématique auto-vérifiable, nous étudions comment entraîner un vérificateur précis et fidèle basé sur les LLM pour la démonstration de théorèmes. Nous entraînons ensuite un générateur de preuves en utilisant le vérificateur comme modèle de récompense, et encourageons le générateur à identifier et résoudre autant de problèmes que possible dans ses propres preuves avant de les finaliser. Pour maintenir l'écart génération-vérification tandis que le générateur devient plus performant, nous proposons d'augmenter l'échelle du calcul de vérification pour étiqueter automatiquement de nouvelles preuves difficiles à vérifier, créant ainsi des données d'entraînement pour améliorer davantage le vérificateur. Notre modèle résultant, DeepSeekMath-V2, démontre de solides capacités en démonstration de théorèmes, atteignant des scores de niveau or aux OIM 2025 et OCM 2024 et un quasi-parfait 118/120 au Putnam 2024 avec un calcul intensifié au moment du test.
English
Large language models have made significant progress in mathematical reasoning, which serves as an important testbed for AI and could impact scientific research if further advanced. By scaling reasoning with reinforcement learning that rewards correct final answers, LLMs have improved from poor performance to saturating quantitative reasoning competitions like AIME and HMMT in one year. However, this approach faces fundamental limitations. Pursuing higher final answer accuracy doesn't address a key issue: correct answers don't guarantee correct reasoning. Moreover, many mathematical tasks like theorem proving require rigorous step-by-step derivation rather than numerical answers, making final answer rewards inapplicable. To push the limits of deep reasoning, we believe it is necessary to verify the comprehensiveness and rigor of mathematical reasoning. Self-verification is particularly important for scaling test-time compute, especially for open problems without known solutions. Towards self-verifiable mathematical reasoning, we investigate how to train an accurate and faithful LLM-based verifier for theorem proving. We then train a proof generator using the verifier as the reward model, and incentivize the generator to identify and resolve as many issues as possible in their own proofs before finalizing them. To maintain the generation-verification gap as the generator becomes stronger, we propose to scale verification compute to automatically label new hard-to-verify proofs, creating training data to further improve the verifier. Our resulting model, DeepSeekMath-V2, demonstrates strong theorem-proving capabilities, achieving gold-level scores on IMO 2025 and CMO 2024 and a near-perfect 118/120 on Putnam 2024 with scaled test-time compute.