DeepSeek Prover V2 renforce l’IA dédiée aux démonstrations mathématiques

Démontrer un théorème ne consiste pas seulement à trouver le bon résultat. Il faut aussi justifier chaque étape sans laisser place à l’ambiguïté. C’est sur ce terrain particulièrement exigeant que DeepSeek veut progresser avec DeepSeek-Prover-V2, une nouvelle version de son modèle consacré au raisonnement mathématique formel, publiée le 30 avril 2025 sur la plateforme Hugging Face.

Le laboratoire chinois, déjà remarqué pour ses modèles généralistes DeepSeek-V3 et de raisonnement DeepSeek-R1, s’attaque ici à une tâche plus étroite mais décisive pour la recherche : produire des démonstrations que des logiciels spécialisés peuvent contrôler ligne par ligne. Prover V2 ne remplace donc pas les mathématiciens. Il ambitionne plutôt d’automatiser une part laborieuse de la formalisation, de proposer des pistes de preuve et de réduire le temps nécessaire pour vérifier des raisonnements complexes.

Ce que DeepSeek a publié avec Prover V2

DeepSeek-Prover-V2 est un modèle conçu pour les preuves de théorèmes et le raisonnement mathématique. Sa diffusion publique constitue une évolution importante après les travaux précédents de DeepSeek dans ce domaine, dont la précédente version publique remontait à août 2024.

Le terme « preuve » mérite toutefois une précision. Dans une conversation ordinaire, une IA peut expliquer une solution de manière convaincante tout en commettant une erreur de calcul, en sautant une hypothèse ou en invoquant une propriété inadaptée. Une preuve formelle, elle, doit être exprimée dans un langage que comprend un vérificateur informatique. Chaque définition, chaque transformation et chaque conclusion doivent respecter des règles logiques explicites.

Prover V2 est notamment orienté vers Lean 4, un assistant de preuve largement utilisé dans la recherche en mathématiques formelles et en informatique théorique. Dans cet environnement, l’IA peut produire une proposition de démonstration, tandis que Lean contrôle ensuite si elle est valide au regard des axiomes, définitions et règles employés.

Démonstration formelle : pourquoi est-ce différent d’un problème de maths classique ?

Un modèle de langage classique est entraîné à prédire la suite la plus probable d’un texte. Cette méthode peut suffire à expliquer une équation de niveau scolaire ou à suggérer une stratégie de résolution. Mais elle devient fragile dès qu’il faut établir un raisonnement long, rigoureux et universel.

La démonstration formelle impose au contraire une discipline très stricte. Une phrase naturelle telle que « il est évident que » ne suffit pas. Le système doit traduire l’idée en instructions exploitables par un vérificateur. Une preuve peut ainsi échouer pour une raison qui paraît mineure à un humain : une variable mal typée, une condition oubliée ou un lemme invoqué dans un contexte où il ne s’applique pas.

C’est ce qui rend les assistants comme Lean précieux, mais aussi difficiles à utiliser. Écrire une preuve formelle demande souvent de maîtriser à la fois les mathématiques et les conventions d’un langage informatique. Un modèle spécialisé tel que Prover V2 cherche à réduire cet obstacle en générant du code de preuve, en décomposant le problème et en tentant plusieurs chemins de raisonnement.

Une base à 671 milliards de paramètres et un mélange d’experts

Prover V2 repose sur DeepSeek-V3-Base, la base du modèle généraliste DeepSeek-V3. Cette architecture totalise 671 milliards de paramètres. Les paramètres correspondent aux valeurs apprises lors de l’entraînement d’un modèle, qui influencent sa capacité à reconnaître des motifs dans les données et à générer des réponses.

Ce chiffre ne doit pas être interprété comme une mesure simple et directe de l’intelligence d’un modèle. Davantage de paramètres ne garantissent ni une réponse exacte ni une démonstration valide. La qualité des données d’entraînement, la méthode d’apprentissage, la capacité à vérifier les résultats et la spécialisation pour une tâche donnée comptent tout autant. Dans le cas de Prover V2, l’enjeu est précisément de transformer la puissance d’un grand modèle en raisonnements compatibles avec un cadre formel.

La particularité de DeepSeek-V3 est son architecture de mélange d’experts, ou MoE. Au lieu de mobiliser les mêmes composants pour toutes les requêtes, le système répartit le travail entre différents sous-modèles spécialisés, appelés experts. Un mécanisme d’aiguillage sélectionne les experts les plus pertinents pour les éléments du problème à traiter.

Cette organisation peut rendre plus efficace le traitement de tâches variées. Pour un problème de démonstration, l’IA doit par exemple interpréter l’énoncé, identifier les outils mathématiques disponibles, construire des sous-objectifs, écrire une preuve formelle et corriger ses essais lorsque le vérificateur les refuse. La décomposition en sous-tâches est donc au cœur de l’intérêt d’un modèle spécialisé.

Pourquoi la décomposition en sous-objectifs compte autant

Face à un théorème long, même un mathématicien ne cherche pas toujours immédiatement la démonstration complète. Il découpe généralement le problème : établir un lemme intermédiaire, prouver une propriété d’une fonction, puis utiliser ce résultat pour atteindre l’objectif principal. Dans un assistant de preuve, cette démarche prend la forme de sous-objectifs précis que le logiciel peut contrôler.

Prover V2 s’inscrit dans cette logique de raisonnement progressif. L’objectif n’est pas uniquement de produire une réponse finale, mais de générer un chemin de preuve qui puisse être testé. Lorsqu’une tentative échoue, le retour du vérificateur peut en principe aider le système à reformuler une étape ou à explorer une autre approche.

Cette association entre génération par IA et validation automatique est particulièrement intéressante, car elle limite l’un des défauts les plus connus des modèles de langage : les hallucinations. Un chatbot peut inventer une référence, un calcul ou une règle avec assurance. Dans le contexte d’une preuve Lean, une étape invalide est rejetée. Le contrôle ne rend pas le modèle infaillible, mais il crée un filtre objectif entre une proposition convaincante et une démonstration effectivement vérifiée.

DeepSeek-V3 et Prover V2 : deux modèles, deux usages

La numérotation peut prêter à confusion. DeepSeek-V3 désigne un modèle de langage généraliste qui sert de fondation technique. DeepSeek-Prover-V2 est la deuxième génération du modèle spécialisé dans les preuves formelles. Le chiffre associé à chacun ne désigne donc pas la même famille de produits ni la même fonction.

DeepSeek-V3 est destiné à des usages généraux de langage et de raisonnement : rédaction, programmation, analyse ou dialogue. Prover V2 en reprend la base, mais l’oriente vers un domaine beaucoup plus contraint. Cette spécialisation est essentielle : une IA qui traite bien du texte généraliste n’est pas nécessairement capable de produire du code Lean valide ou de conduire une démonstration abstraite jusqu’à son terme.

La publication sur Hugging Face s’inscrit aussi dans le positionnement de DeepSeek autour de modèles accessibles à la communauté. Chercheurs et développeurs peuvent étudier les fichiers diffusés, tester le système dans des environnements adaptés et évaluer ses résultats sur leurs propres problèmes formels.

Cette accessibilité ne signifie pas pour autant qu’un particulier pourra faire fonctionner facilement le modèle sur son ordinateur. Un système de cette taille nécessite des ressources de calcul, de mémoire et de stockage considérables. Pour le grand public, l’intérêt est surtout indirect : les améliorations obtenues dans la preuve formelle peuvent ensuite contribuer à de meilleurs outils pédagogiques, scientifiques et logiciels.

Quelles applications concrètes pour une IA de démonstration ?

Les premières personnes concernées sont les chercheurs travaillant sur les mathématiques, la logique et la vérification formelle. Un modèle tel que Prover V2 peut aider à chercher des pistes, à automatiser des étapes répétitives ou à convertir certains raisonnements vers un format vérifiable par machine. Il peut aussi servir à explorer les grandes bibliothèques de théorèmes déjà formalisés dans Lean.

En informatique, la preuve formelle ne concerne pas seulement les théorèmes abstraits. Elle peut être utilisée pour contrôler des propriétés de programmes, de protocoles cryptographiques ou de composants matériels. Un système est alors vérifié par rapport à une spécification rigoureuse : il ne s’agit pas simplement de constater qu’il fonctionne dans quelques tests, mais de chercher à établir qu’il respecte certaines règles dans tous les cas définis.

L’éducation pourrait également bénéficier, à terme, de ces progrès. Un assistant capable de détailler les étapes d’une démonstration et de signaler exactement où un raisonnement devient invalide serait utile aux étudiants. Mais il faut distinguer l’explication pédagogique de la preuve formelle : un code Lean valide peut être difficile à lire pour un débutant, tandis qu’une explication claire en français ne fournit pas nécessairement la rigueur exigée par un vérificateur.

Les limites restent importantes. Les systèmes de preuve formelle dépendent de bibliothèques de théorèmes, de définitions très précises et de problèmes correctement traduits. Une IA peut se heurter à des énoncés inédits, à une formalisation ambiguë ou à une démonstration dont la stratégie requiert une intuition mathématique difficile à reproduire. Surtout, le modèle ne remplace pas le jugement humain sur la pertinence d’une question scientifique ou sur le choix des hypothèses.

Une brique dans la stratégie plus large de DeepSeek

La sortie de Prover V2 intervient alors que DeepSeek poursuit le développement de plusieurs familles de modèles. Le laboratoire a récemment actualisé son modèle généraliste DeepSeek-V3. Une mise à jour de son modèle de raisonnement DeepSeek-R1 est également attendue, ce qui pourrait compléter sa gamme entre usages généralistes, raisonnement et applications spécialisées.

En février 2025, des informations de presse ont par ailleurs indiqué que DeepSeek envisageait une première levée de fonds externe. Une telle opération pourrait soutenir les coûts très élevés liés à l’entraînement, à l’inférence et à la recherche sur des modèles de grande taille. À la date de publication, il s’agit toutefois d’une perspective rapportée, et non d’une annonce financière formalisée par DeepSeek.

La stratégie est claire : dans un secteur où les grands modèles généralistes se rapprochent rapidement sur de nombreuses tâches, les capacités spécialisées peuvent devenir un facteur de différenciation. Les mathématiques formelles constituent un test particulièrement exigeant, car les réponses y sont moins évaluées sur leur fluidité que sur leur validité vérifiable.

Ce qu’il faut surveiller

La publication de Prover V2 pose d’abord une question de mesure : sur quels corpus de théorèmes le modèle progresse-t-il réellement, et à quel degré d’autonomie ? Les évaluations devront distinguer les problèmes proches des données d’entraînement de ceux qui exigent une généralisation authentique. La capacité à résoudre un exercice isolé ne prouve pas encore qu’une IA peut conduire seule une recherche mathématique originale.

Il faudra aussi observer l’adoption du modèle par la communauté Lean. Les retours des chercheurs sur la qualité des preuves proposées, le taux d’acceptation par le vérificateur et l’utilité dans des projets concrets compteront davantage que la seule taille du modèle. Les outils qui facilitent la correction, l’explication et la réutilisation des démonstrations pourraient être aussi importants que le modèle lui-même.

Enfin, Prover V2 illustre une direction plus large de l’intelligence artificielle : associer un modèle génératif à un système de vérification externe. Dans les domaines où l’erreur est coûteuse, comme les mathématiques, le code ou certaines applications scientifiques, la capacité à produire une réponse doit idéalement aller de pair avec un moyen fiable de la contrôler. C’est cette combinaison, plus que la seule éloquence des chatbots, qui pourrait faire franchir une nouvelle étape aux IA de raisonnement.