DeepSeek lance DeepSeek-Prover-V2-671B : un modèle de nouvelle génération pour la démonstration automatique de théorèmes, basé sur une architecture MoE de 671 milliards de paramètres 62

DeepSeek ai a publié le 30 avril 2025 DeepSeek-Prover-V2-671B, un modèle de démonstration automatique de théorèmes de nouvelle génération basé sur une architecture MoE de 671 milliards de paramètres, qui génère et vérifie des preuves dans le cadre de Lean 4. Ses avantages incluent l'élévation des mathématiques formelles à une échelle de « niveau GPT-4 », des gains d'efficacité apportés par le MoE, l'open source et l'autorisation d'usage commercial. Par rapport à la version V1.5, il présente des améliorations significatives en termes de nombre de paramètres, de longueur de contexte, de taux de réussite, etc. Il devrait obtenir d'excellents résultats sur des benchmarks tels que miniF2F et peut être utilisé dans des domaines tels que la vérification formelle et l'accélération de la recherche mathématique. Lors de son utilisation, il est nécessaire de télécharger les poids depuis Hugging Face et de procéder à la configuration correspondante.

Caractéristiques techniques

• Nombre de paramètres et architecture : le nombre total de paramètres du modèle est de 671 milliards, avec une architecture MoE qui active environ 37 milliards de paramètres par token. Cette architecture réduit considérablement les besoins en mémoire tout en maintenant une capacité de raisonnement puissante.

• Longueur du contexte : prend en charge un contexte ultra-long, avec un embedding positionnel maximal de 163 840, capable de gérer des preuves mathématiques complexes.

• Précision de calcul : prend en charge plusieurs précisions de calcul telles que BF16, FP8 et F32, facilitant un entraînement et un déploiement plus rapides et plus économes en ressources du modèle.

• Format de fichier : utilise le format de fichier safetensors, plus efficace.

• Technique de quantification : adopte la quantification FP8, qui réduit la taille du modèle et améliore l'efficacité de l'inférence grâce aux techniques de quantification.

Avantages clés

• Échelle et complexité : un nombre énorme de paramètres et une longue fenêtre de contexte (environ 128k tokens) permettent de gérer des chaînes logiques de preuves mathématiques plus longues et plus complexes.

• Optimisation de l'efficacité : grâce à l'architecture MoE, par rapport à un modèle entièrement connecté de 671 milliards de paramètres, les besoins en mémoire sont considérablement réduits et la vitesse d'inférence est améliorée.

• Open source et licence : le modèle est open source, les poids sont disponibles sur Hugging Face, et un usage commercial devrait être autorisé.

Scénarios d'application

• Vérification formelle : réaliser des vérifications rigoureuses dans les preuves de sécurité cryptographique ou les preuves de correction de conception de puces.

• Accélération de la recherche mathématique : aider les mathématiciens à formaliser des théorèmes existants, explorer de nouvelles conjectures et résoudre des problèmes mathématiques de niveau olympique.

• Outil pédagogique avancé : créer des systèmes de tutorat interactifs pour guider les étudiants dans la réalisation de preuves formelles.

• Systèmes critiques pour la sécurité : vérifier les propriétés critiques et les invariants des logiciels via l'intégration de Lean avant le déploiement du code.

Étapes de démarrage rapide

1. Obtenir le modèle : télécharger les poids depuis Hugging Face : deepseek-ai/DeepSeek-Prover-V2-671B.

2. Configurer Lean : installer Lean 4 (version recommandée ≥ 4.5) et la bibliothèque mathlib4.

3. Vérifier le matériel : s'assurer que la configuration matérielle répond aux exigences minimales (une configuration haute performance est recommandée).

4. Installer le moteur d'inférence : configurer par exemple vLLM ou tout autre cadre compatible MoE.

5. Explorer les exemples : examiner les scripts d'évaluation ou les notebooks d'exemple dans le dépôt du modèle.

Questions fréquentes

Est-il open source ? Peut-il être utilisé à des fins commerciales ?

Oui, DeepSeek-Prover-V2-671B est open source (les poids sont disponibles sur Hugging Face) et sa licence devrait autoriser les usages académiques et commerciaux.

Peut-il fonctionner sur un NVIDIA 4090 ?

Selon les rapports préliminaires, grâce aux optimisations telles que MoE, MLA et la quantification, le modèle peut fonctionner sur un seul GPU NVIDIA 4090, notamment lorsqu'il est associé à suffisamment de RAM et à un NVMe SSD rapide pour le chargement dynamique. Les performances varient selon la configuration spécifique.

Liens associés

Hugging Face :https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

Github :https://github.com/deepseek-ai/DeepSeek-Prover-V1.5

Présentation détaillée :https://deepseeksai.com/prover-v2-671b/

Article :https://arxiv.org/pdf/2408.08152