DeepSeek-Prover-V2 : Combler le fossé entre le raisonnement mathématique informel et formel

Alors que DeepSeek-R1 a considérablement amélioré les capacités de l’IA en matière de raisonnement informel, le raisonnement mathématique formel est resté une tâche difficile pour l’IA. C’est principalement parce que produire une preuve mathématique vérifiable nécessite à la fois une compréhension conceptuelle approfondie et la capacité de construire des arguments logiques précis et étape par étape. Récemment, cependant, une avancée significative a été réalisée dans cette direction, car les chercheurs de DeepSeek-AI ont introduit DeepSeek-Prover-V2, un modèle d’IA open-source capable de transformer l’intuition mathématique en preuves rigoureuses et vérifiables. Cet article se penchera sur les détails de DeepSeek-Prover-V2 et examinera son impact potentiel sur les découvertes scientifiques futures.

Le défi du raisonnement mathématique formel

Les mathématiciens résolvent souvent des problèmes en utilisant l’intuition, les heuristiques et le raisonnement de haut niveau. Cette approche leur permet de sauter des étapes qui semblent évidentes ou de se fier à des approximations qui sont suffisantes pour leurs besoins. Cependant, la démonstration de théorèmes formels exige une approche différente. Elle nécessite une précision totale, avec chaque étape explicitement énoncée et justifiée logiquement sans aucune ambiguïté.

Les progrès récents dans les grands modèles de langage (LLM) ont montré qu’ils peuvent résoudre des problèmes mathématiques complexes de niveau de concours en utilisant le raisonnement de langage naturel. Malgré ces progrès, cependant, les LLM ont toujours du mal à convertir le raisonnement intuitif en preuves formelles que les machines peuvent vérifier. C’est principalement parce que le raisonnement informel inclut souvent des raccourcis et des étapes omises que les systèmes formels ne peuvent pas vérifier.

DeepSeek-Prover-V2 répond à ce problème en combinant les forces du raisonnement informel et formel. Il décompose les problèmes complexes en parties plus petites et gérables tout en maintenant la précision requise par la vérification formelle. Cette approche facilite le pont entre l’intuition humaine et les preuves vérifiées par machine.

Une nouvelle approche de la démonstration de théorèmes

En essence, DeepSeek-Prover-V2 utilise une chaîne de traitement de données unique qui implique à la fois le raisonnement informel et formel. La chaîne commence avec DeepSeek-V3, un LLM polyvalent, qui analyse les problèmes mathématiques en langage naturel, les décompose en étapes plus petites et les traduit en langage formel que les machines peuvent comprendre.

Plutôt que d’essayer de résoudre tout le problème à la fois, le système le décompose en une série de “sous-objectifs” – des lemmes intermédiaires qui servent de pierres d’achoppement vers la preuve finale. Cette approche reproduit la façon dont les mathématiciens humains abordent les problèmes difficiles, en travaillant sur des morceaux gérables plutôt que d’essayer de résoudre tout d’un coup.

Ce qui rend cette approche particulièrement innovante, c’est la façon dont elle synthétise les données de formation. Lorsque tous les sous-objectifs d’un problème complexe sont résolus avec succès, le système combine ces solutions en une preuve formelle complète. Cette preuve est ensuite associée à la chaîne de raisonnement de DeepSeek-V3 pour créer des données de formation de haute qualité pour l’entraînement du modèle.

Apprentissage par renforcement pour le raisonnement mathématique

Après une formation initiale sur des données synthétiques, DeepSeek-Prover-V2 utilise l’apprentissage par renforcement pour améliorer encore ses capacités. Le modèle reçoit des commentaires sur la justesse de ses solutions et utilise ces commentaires pour apprendre quelles approches fonctionnent le mieux.

L’un des défis ici est que la structure des preuves générées ne correspond pas toujours à la décomposition de lemme suggérée par la chaîne de pensée. Pour résoudre ce problème, les chercheurs ont inclus une récompense de cohérence lors des étapes de formation pour réduire la désalignement structurel et imposer l’inclusion de tous les lemmes décomposés dans les preuves finales. Cette approche d’alignement s’est avérée particulièrement efficace pour les théorèmes complexes nécessitant un raisonnement multi-étapes.

Performances et capacités dans le monde réel

Les performances de DeepSeek-Prover-V2 sur les benchmarks établis démontrent ses capacités exceptionnelles. Le modèle obtient des résultats impressionnants sur le benchmark MiniF2F-test et résout avec succès 49 des 658 problèmes du PutnamBench – une collection de problèmes de la prestigieuse compétition mathématique William Lowell Putnam.

Peut-être plus impressionnant encore, lorsqu’il est évalué sur 15 problèmes sélectionnés des récentes American Invitational Mathematics Examination (AIME) compétitions, le modèle résout avec succès 6 problèmes. Il est également intéressant de noter que, par rapport à DeepSeek-Prover-V2, DeepSeek-V3 a résolu 8 de ces problèmes en utilisant le vote majoritaire. Cela suggère que le fossé entre le raisonnement mathématique formel et informel se réduit rapidement dans les LLM. Cependant, les performances du modèle sur les problèmes combinatoires nécessitent encore une amélioration, mettant en évidence un domaine où la recherche future pourrait se concentrer.

ProverBench : Un nouveau benchmark pour l’IA en mathématiques

Les chercheurs de DeepSeek ont également introduit un nouveau jeu de données de benchmark pour évaluer la capacité de résolution de problèmes mathématiques des LLM. Ce benchmark, nommé ProverBench, se compose de 325 problèmes mathématiques formalisés, dont 15 problèmes des récentes compétitions AIME, ainsi que des problèmes de manuels scolaires et de tutoriels éducatifs. Ces problèmes couvrent des domaines tels que la théorie des nombres, l’algèbre, le calcul, l’analyse réelle, et plus encore. L’introduction de problèmes AIME est particulièrement vitale car elle évalue le modèle sur des problèmes qui nécessitent non seulement la mémorisation des connaissances mais aussi la résolution créative de problèmes.

Accès open-source et implications futures

DeepSeek-Prover-V2 offre une opportunité passionnante avec son accès open-source. Hébergé sur des plateformes comme Hugging Face, le modèle est accessible à un large éventail d’utilisateurs, y compris les chercheurs, les éducateurs et les développeurs. Avec à la fois une version plus légère de 7 milliards de paramètres et une version puissante de 671 milliards de paramètres, les chercheurs de DeepSeek assurent que les utilisateurs ayant des ressources computationnelles variées peuvent encore en bénéficier. Cet accès open-source encourage l’expérimentation et permet aux développeurs de créer des outils d’IA avancés pour la résolution de problèmes mathématiques. Par conséquent, ce modèle a le potentiel de stimuler l’innovation dans la recherche mathématique, permettant aux chercheurs de résoudre des problèmes complexes et de découvrir de nouvelles perspectives dans le domaine.

Implications pour l’IA et la recherche mathématique

Le développement de DeepSeek-Prover-V2 a des implications significatives non seulement pour la recherche mathématique mais également pour l’IA. La capacité du modèle à générer des preuves formelles pourrait aider les mathématiciens à résoudre des théorèmes difficiles, à automatiser les processus de vérification et même à suggérer de nouvelles conjectures. De plus, les techniques utilisées pour créer DeepSeek-Prover-V2 pourraient influencer le développement de futurs modèles d’IA dans d’autres domaines qui reposent sur un raisonnement logique rigoureux, tels que l’ingénierie logicielle et matérielle.

Les chercheurs visent à mettre à l’échelle le modèle pour résoudre des problèmes encore plus complexes, tels que ceux du niveau de l’Olympiade internationale de mathématiques (IMO). Cela pourrait encore améliorer les capacités de l’IA pour démontrer des théorèmes mathématiques. À mesure que des modèles comme DeepSeek-Prover-V2 continuent d’évoluer, ils pourraient redéfinir l’avenir à la fois des mathématiques et de l’IA, stimulant les progrès dans des domaines allant de la recherche théorique aux applications pratiques dans la technologie.

En résumé

DeepSeek-Prover-V2 est un développement important dans le raisonnement mathématique dirigé par l’IA. Il combine l’intuition informelle avec la logique formelle pour décomposer les problèmes complexes et générer des preuves vérifiables. Ses performances impressionnantes sur les benchmarks montrent son potentiel pour soutenir les mathématiciens, automatiser la vérification des preuves et même stimuler de nouvelles découvertes dans le domaine. En tant que modèle open-source, il est largement accessible, offrant des possibilités passionnantes pour l’innovation et de nouvelles applications dans l’IA et les mathématiques.