DeepSeek -Prover-V2 est un modèle open source , tout comme les versions précédentes de l' entreprise chinoise

DeepSeek -Prover-V2 est un modèle open source , tout comme les versions précédentes de l' entreprise chinoise

DeepSeek-Prover-V2 peut aider les mathématiciens à explorer de nouveaux théorèmes et à vérifier les preuves formelles

Points forts
  • DeepSeek-Prover-V1.5-Base avec un contexte allant jusqu'à 32 000 jetons
  • L'IA est dispo au téléchargement via Hugging Face, liste de DeepSeek
  • Il est dédié à la démonstration de théorèmes mathématiques formels
Publicité
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 .
 
Lecture complémentaire: DeepSeek, AI, Artificial Intelligence
Partager sur Facebook Gadgets360 Twitter ShareTweet Partager Snapchat Reddit

Publicité

Publicité

© Copyright Red Pixels Ventures Limited 2025. All rights reserved.
Trending Products »
Latest Tech News »