Un nouveau modèle de preuve a été lancé mercredi par DeepSeek, une entreprise d'intelligence artificielle (IA) basée à Hangzhou, en Chine. Ce modèle très spécialisé , appelé DeepSeek-Prover-V2, est dédié à la démonstration de théorèmes mathématiques formels . Le langage de programmation Lean 4 est utilisé par le modèle de langage étendu (LLM) pour analyser chaque étape séparément et déterminer la cohérence logique des preuves mathématiques . DeepSeek -Prover-V2 est un modèle open source , tout comme les versions précédentes de l' entreprise chinoise , et est disponible en téléchargement sur des dépôts réputés comme GitHub et Hugging Face.Sur sa page GitHub , l' entreprise d'IA décrit en détail son nouveau modèle . Il s'agit essentiellement d' un paradigme axé sur le raisonnement et doté d' une chaîne de pensée (CdP) visible , fonctionnant dans le domaine mathématique . Le modèle d' IA DeepSeek-V3 , publié en décembre 2024, en constitue le fondement et la source .
DeepSeek-Prover-V2 a de multiples applications. Il permet d'identifier et de corriger les erreurs dans les démonstrations de théorèmes mathématiques , ainsi que de résoudre des problèmes mathématiques du lycée à l' université . Il peut aider les mathématiciens et les chercheurs à étudier de nouveaux théorèmes et à démontrer leur validité. Il peut également servir d' outil pédagogique et fournir des explications détaillées pour les démonstrations.
Un modèle de sept milliards de paramètres et un modèle plus grand de 671 milliards de paramètres sont fournis. Le premier est basé sur DeepSeek-Prover-V1.5-Base et possède une longueur de contexte allant jusqu'à 32 000 jetons, tandis que le second est entraîné sur DeepSeek-V3- Base .
Concernant les procédures de pré-entraînement , les chercheurs ont demandé au modèle de base de décomposer des défis complexes afin d' établir un système d'entraînement à froid . Ces problèmes ont fonctionné comme une série d' objectifs plus petits . Ensuite, afin d' établir un démarrage à froid initial pour l' apprentissage par renforcement , le raisonnement du modèle de base a été fusionné avec les preuves des sous-objectifs résolus , qui ont été ajoutés au CoT .
Il est intéressant de noter que le modèle d'IA est également disponible en téléchargement via la liste Hugging Face de DeepSeek, en plus de GitHub. Le modèle Prover-V2 démontre comment des modifications itératives de l'entraînement des modèles d'IA peuvent considérablement améliorer leurs capacités spécialisées . Les détails concernant l' ensemble de données plus large ou l' architecture fondamentale sont inconnus, comme c'est le cas pour les précédentes versions de modèles open source .