Présentation de DeepSeekMath-V2 - vers un raisonnement mathématique auto-vérifiable

• Dans le but d’améliorer les capacités de raisonnement mathématique des grands modèles de langage, ce modèle renforce la vérifiabilité du processus de raisonnement au-delà de la simple précision de la réponse.
• En corrigeant les limites de l’approche basée sur l’apprentissage par renforcement centrée sur la récompense de la réponse finale, il introduit un mécanisme d’auto-vérification (self-verification).
• Pour les problèmes exigeant une progression logique étape par étape comme la démonstration de théorèmes (theorem proving), le modèle génératif est conçu pour s’auto-détecter et corriger ses erreurs.
• Le vérificateur (verifier) est utilisé comme modèle de récompense, et l’on étend la quantité de calcul de vérification pour étiqueter automatiquement des données de preuve plus complexes, permettant une amélioration continue des performances.
• IMO 2025, CMO 2024, Putnam 2024 : DeepSeekMath-V2 a atteint des scores de très haut niveau, démontrant la faisabilité d’une IA de raisonnement mathématique auto-vérifiable.

---

1. Introduction

• Les grands modèles de langage (LLM) ont réalisé de grands progrès en raisonnement mathématique, jouant un rôle majeur de banc d’essai pour la recherche en IA.
  • Grâce à l’apprentissage par renforcement et à un entraînement basé sur la récompense de la réponse finale, ils ont atteint en un an des performances de haut niveau sur des concours comme AIME et HMMT.
• Cependant, l’approche visant simplement à améliorer la précision de la réponse finale montre ses limites.
  • Même si la réponse est correcte, la cohérence du processus de raisonnement n’est pas garantie, et elle est difficilement applicable aux problèmes nécessitant une élaboration logique étape par étape comme les démonstrations de théorèmes.
• Pour remédier à cela, le concept d’auto-vérification (self-verification) est introduit afin d’évaluer l’exhaustivité et la rigueur du raisonnement.
  • En particulier, il est présenté comme un élément essentiel pour le scaling du calcul lors de l’inférence sur des problèmes ouverts (open problems), où les réponses ne sont pas connues à l’avance.
• L’équipe de recherche a entraîné un vérificateur fiable basé sur les LLM et l’a utilisé comme modèle de récompense pour entraîner le générateur de preuves (generator).
  • Cela incite le générateur à trouver et corriger lui-même les erreurs présentes dans les preuves.
• À mesure que les performances du générateur s’améliorent, la difficulté de la vérification augmente également. Le calcul dédié à la vérification est donc étendu (scale verification compute) pour annoter automatiquement de nouvelles preuves plus difficiles.
  • Cela permet d’améliorer en continu les performances du vérificateur.
• Le modèle final DeepSeekMath-V2 a atteint un niveau de médailles d’or à IMO 2025 et CMO 2024, avec 118/120 points à Putnam 2024.
  • Ces résultats montrent que le raisonnement mathématique auto-vérifiable est une direction de recherche réalisable.

2. Résultats d’évaluation (Evaluation Results)

• L’évaluation utilise l’IMO-ProofBench, développé par l’équipe DeepThink IMO-Gold de DeepMind, ainsi que les récents concours mathématiques (IMO 2025, CMO 2024, Putnam 2024).
  • Les chiffres précis ou détails des résultats ne sont pas indiqués dans le texte.

3. Architecture du modèle et base

• DeepSeekMath-V2 est construit sur le modèle DeepSeek-V3.2-Exp-Base.
  • Les détails d’inférence sont disponibles dans le dépôt GitHub de DeepSeek-V3.2-Exp.

4. Licence (License)

• Le modèle et ses poids sont distribués sous licence Apache License 2.0.

5. Référence (Citation)

• Les auteurs du travail et les informations bibliographiques sont indiqués, le titre étant : “DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning” (2025)

6. Informations supplémentaires

• Nombre de téléchargements le mois dernier : 4 434.
• Lors de la construction de l’arbre du modèle, le modèle de base forme une boucle d’auto-référence, ce qui empêche la génération de l’arbre.

[GN⁺]

Avis sur Hacker News

• Le modèle publié cette fois a rendu ses poids open source sous licence Apache 2.0
  Les modèles médaillés d’or à l’IMO d’OpenAI et de DeepMind restent toujours fermés

  • Je pense que, de la même façon que les entreprises d’IA traitent le droit d’auteur des données d’entraînement, nous devrions aussi traiter ainsi le droit d’auteur sur les poids
  • Mais si seuls les poids sont publiés sans le code d’entraînement ni les données, cela reste un modèle fermé

• La discussion précédente est à ce lien

  • J’avais raté ce lien, merci de l’avoir partagé

• Il est impressionnant de voir les modèles à poids ouverts rattraper rapidement leur retard dans des domaines spécialisés comme les mathématiques ou le raisonnement
  Je me demande si quelqu’un l’a aussi testé sur de la logique complexe ou du code. Les modèles performants en mathématiques sont souvent aussi bons en débogage ou en génération d’algorithmes

  • C’est un phénomène naturel, car les modèles spécialisés dans un domaine précis ont moins de valeur commerciale, tandis que l’entraînement de grands LLM privilégie la polyvalence
  • kimi-k2 est plutôt correct pour le code, mais n’atteint pas le niveau des modèles SOTA d’Anthropic, OpenAI ou Google

• Je pense qu’il faut aussi garder une certaine dose de scepticisme sur les performances de ce modèle
  Il est indiqué qu’il a appris directement à partir de problèmes collectés sur Internet, mais il n’est pas précisé si une décontamination des benchmarks a été effectuée ni si les problèmes de 2024/2025 ont été exclus
  OpenAI et Google ont testé leurs modèles expérimentaux sans accès préalable aux problèmes de 2025

• Je me demande pourquoi le modèle médaillé d’or d’OpenAI n’a toujours pas été publié

  • C’était simplement un coup de communication. Les enseignements tirés seront intégrés dans le prochain modèle généraliste

• Il est important de noter que ce modèle n’est pas un modèle généraliste. Les modèles de Google et d’OpenAI étaient généralistes

  • En réalité, OpenAI comme Google ont tous deux utilisé des modèles de recherche spécialisés pour l’IMO
    • OpenAI a annoncé la sortie de GPT-5 dans ce tweet, en précisant que le modèle IMO était expérimental et qu’il n’était pas prévu de le publier pour l’instant
    • DeepMind explique dans son blog officiel avoir entraîné Gemini avec un raisonnement en plusieurs étapes fondé sur l’apprentissage par renforcement et des données de démonstration de théorèmes
  • Le post officiel de DeepSeek a aussi été partagé

• Je me demande comment faire tourner ce modèle chez soi
  La question est de savoir si c’est possible avec un CPU et environ 1 To de RAM

  • Rien que les données à télécharger font 690 Go, donc il faudrait probablement 1 To de RAM. Même avec mes deux machines Strix Halo, c’est impossible
  • Avec ik_llama.cpp, suffisamment de RAM et un GPU, on peut le faire tourner lentement. Le llama.cpp classique fonctionne aussi, mais le fork ik est plus efficace
  • Apparemment, c’est aussi possible avec deux Mac Studio de 512 Go reliés en Thunderbolt 5

• Je me demande si ce modèle n’a pas été distillé directement à partir des sorties d’OpenAI ou de Google

• Je me demande si ce modèle est prévu sur OpenRouter

• Si OpenAI ajoute de la publicité dans ChatGPT, est-ce que les gens ne passeront pas immédiatement à d’autres modèles ?

  • Je pense au contraire qu’il serait préférable d’avoir plusieurs fournisseurs proposant des modèles généralistes en concurrence au prix du marché
  • Publicité ou non, je ne fais pas confiance à OpenAI. Difficile d’y croire avant qu’ils ne changent leur nom en CloseAI
  • ChatGPT n’est qu’un site web. Voir de la publicité sur un site web n’a rien d’étrange. Instagram aussi fonctionne ainsi
  • Ils ont déjà un modèle économique via les data centers GPU et les API. Même si la concurrence augmente, cela restera sans doute le choix n°1 pendant encore un moment
  • Google fait de la publicité depuis des décennies, et pourtant personne n’est parti vers un autre moteur de recherche