DeepSeek publie le modèle Prover-V2 : 671B Parameters Boost Mathematical Theorem Proving (en anglais)

Au cours de la journée du 1er mai, DeepSeek a une fois de plus apporté une grande nouvelle dans le domaine de l'IA en mettant en open-sourcing le nouveau modèle DeepSeek-Prover-V2. Malgré les récentes rumeurs circulant sur le web au sujet de la sortie imminente de DeepSeek-R2, DeepSeek est allé de l'avant et a publié ce puissant modèle axé sur la démonstration de théorèmes mathématiques, et continue de maintenir son esprit open source habituel.

Deux modèles puissants synchronisés avec l'open source

Cette fois, DeepSeek a mis à disposition deux versions du modèle DeepSeek-Prover-V2.

• DeepSeek-Prover-V2-671B: Construit sur DeepSeek-V3-Base avec 671 milliards de paramètres, il est actuellement le roi de la performance en matière de démonstration de théorèmes.
• DeepSeek-Prover-V2-7B: Construit sur DeepSeek-Prover-V1.5-Base, avec 7 milliards de paramètres, supportant des longueurs de contexte jusqu'à 32K tokens.

Les deux modèles ont été officiellement publiés sur Hugging Face :

• DeepSeek-Prover-V2-7B. https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B
• DeepSeek-Prover-V2-671B. https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

Qu'est-ce que DeepSeek-Prover-V2 ?

DeepSeek-Prover-V2 est un modèle open-source de grand langage pour le "langage de programmation mathématique de l'IA" Lean 4, qui se concentre sur la preuve formelle de théorèmes. En d'autres termes, il peut transformer des théorèmes mathématiques abstraits en preuves rigoureuses vérifiables par ordinateur, ce qui constitue un outil révolutionnaire pour la recherche mathématique.

Sa meilleure caractéristique est sa capacité à combiner de manière transparente le raisonnement mathématique non formel (c'est-à-dire couramment utilisé par les humains) avec des preuves formelles rigoureuses, ce qui permet au modèle de penser de manière aussi souple qu'un humain et d'argumenter de manière aussi rigoureuse qu'un ordinateur, réalisant ainsi un mélange intégré de raisonnement mathématique.

Des performances étonnantes : de nombreux records battus

DeepSeek-Prover-V2-671B fait preuve d'une force sans précédent dans divers benchmarks de démonstration de théorèmes :

• Obtention d'un taux de réussite record de 88,9% sur l'ensemble de tests MiniF2F
• A résolu avec succès 49 des 658 questions de l'ensemble de données PutnamBench
• Réussit également à résoudre des problèmes mathématiques difficiles tels que ceux des concours AIME 24 et 25.

De nombreux internautes ont testé le modèle et ont déclaré qu'il était encore plus capable de résoudre des problèmes mathématiques complexes que les meilleurs modèles tels que o4-mini d'OpenAI et Grok-3 de XAI. Certains élèves qui ont participé aux Olympiades de mathématiques se sont exclamés : "Les Olympiades n'ont jamais été aussi faciles !".

Innovation technologique : combinaison de l'apprentissage récursif et de l'apprentissage par renforcement

Dans le rapport technique, l'équipe DeepSeek révèle la méthodologie de formation de base de Prover-V2, qui est basée sur une combinaison innovante de l'apprentissage récursif et de l'apprentissage par renforcement. Le processus de formation des modèles est divisé en plusieurs étapes clés :

1) Recherche récursive de preuves par décomposition des sous-buts

DeepSeek-Prover-V2 utilise un mode de pensée similaire à celui d'un mathématicien humain - en décomposant des théorèmes complexes en une série de lemmes plus petits à prouver. Le processus de mise en œuvre spécifique comprend

• DeepSeek-V3 est d'abord invité à générer des esquisses de preuves en langage naturel et à les formaliser sous forme d'énoncés de théorèmes en langage Lean.
• Les sous-buts décomposés sont ensuite résolus de manière récursive à l'aide du modèle de preuve 7B
• Enfin, les preuves de ces sous-buts sont combinées pour construire une preuve formelle complète du problème complexe d'origine

Cette approche permet non seulement d'améliorer l'efficacité de la preuve, mais aussi d'étendre la gamme de théorèmes que le modèle peut traiter.

2. harmoniser le raisonnement non formel avec les preuves formelles

L'équipe de DeepSeek a habilement combiné le raisonnement en langage naturel de haut niveau avec des processus de preuve exacte de bas niveau :

• Choisissez des problèmes particulièrement difficiles à résoudre et divisez-les en objectifs plus petits.
• Lorsque les mini-objectifs sont tous prouvés, ils sont combinés pour former une preuve complète et rigoureuse.
• Ajoutez cette preuve complète à la "chaîne de pensée" générée par DeepSeek-V3 pour former des données d'entraînement qui combinent la pensée humaine et la vérification par la machine.

L'équipe a ainsi collecté des centaines de données d'entraînement de haute qualité, fournissant une base d'apprentissage solide pour le modèle.

3. l'apprentissage renforcé pour améliorer les capacités de raisonnement

Après une première mise au point, l'équipe a introduit l'algorithme d'apprentissage par renforcement GRPO (Group Relative Policy Optimization) :

• Échantillonnage de plusieurs preuves candidates pour chaque question et optimisation de la stratégie en fonction des récompenses relatives.
• Utilisation d'un mécanisme de récompense binaire : Lean obtient un score de 1 en cas de vérification réussie et un score de 0 en cas d'échec.
• La prime de cohérence structurelle est spécifiquement conçue pour garantir que les preuves générées par le modèle sont cohérentes avec les idées de décomposition de la chaîne de pensée

Cette méthode d'apprentissage améliore considérablement la précision du modèle dans la démonstration de théorèmes complexes.

ProverBench : un nouvel ensemble de tests mathématiques

Outre le modèle lui-même, DeepSeek a publié ProverBench, un ensemble de données de référence comprenant 325 questions :

• 15 questions sur la théorie des nombres et l'algèbre tirées des derniers concours de mathématiques tels que AIME 24 et 25
• 310 questions sélectionnées à partir d'exemples de manuels et de tutoriels, couvrant un large éventail de niveaux de difficulté et de domaines.

Cet ensemble de données est destiné à fournir une évaluation complète des modèles au niveau des concours de l'enseignement secondaire et des mathématiques de premier cycle, et à fournir une plate-forme de test plus systématique pour la recherche sur l'intelligence artificielle en mathématiques.

Lien ProverBench :https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench

Résultats expérimentaux et conclusions mises en évidence

Au cours de l'étude, l'équipe a découvert plusieurs phénomènes intéressants :

Modèles CoT et non-CoT

DeepSeek-Prover-V2 supporte deux modes complémentaires de génération de preuves :

• Modèle non-CoT (non-Chain of Thought) très efficaceGénération rapide de code Lean sans étapes d'inférence intermédiaires
• Modèle de chaîne de pensée (CoT) de haute précisionreprésentation systématique du processus de raisonnement et construction progressive de preuves logiquement claires

Les expériences montrent un avantage significatif du modèle CoT par rapport au modèle non-CoT dans le raisonnement mathématique formel, confirmant l'efficacité de l'indice de la chaîne de pensée dans le domaine de la démonstration de théorèmes.

Capacités inattendues des petits modèles

De manière surprenante, DeepSeek-Prover-V2-7B a dépassé les attentes lors de l'utilisation du modèle non-CoT sur l'ensemble de données PutnamBench. Il a même résolu 13 questions que le modèle 671B n'avait pas réussi à résoudre !

L'analyse a révélé que le modèle 7B a acquis une technique unique - l'utilisation fréquente de Cardinal.toNat et Cardinal.natCast_inj pour les problèmes impliquant des bases finies, une technique rare dans le modèle 671B. Ce résultat suggère que l'apprentissage par renforcement n'améliore pas seulement les performances globales, mais permet également au modèle de développer des techniques spécialisées de résolution de problèmes.

Guide de démarrage rapide

Vous voulez essayer DeepSeek-Prover-V2 ? Voici un exemple simple montrant comment utiliser la bibliothèque Transformers de Hugging Face pour l'inférence de modèles :

from transformers import AutoModelForCausalLM, AutoTokenizer
import torch

torch.manual_seed(30)
model_id = "deepseek-ai/DeepSeek-Prover-V2-7B" # ou deepseek-ai/DeepSeek-Prover-V2-671B
tokenizer = AutoTokenizer.from_pretrained(model_id)

formal_statement = """
import Mathlib
import Aesop
set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat
/-- Quelle est la différence positive entre $120\%$ de 30 et $130\%$ de 20 ? Montrez qu'elle est de 10.-/
théorème mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := par
    désolé
""".strip()

prompt = """
Complétez le code Lean 4 suivant.
 ``lean4
{}

perspectives d'avenir

L'équipe de DeepSeek indique que les travaux futurs porteront sur l'extension de ce cadre à des systèmes de type AlphaProof. L'objectif ultime est de résoudre des énigmes mathématiques de niveau IMO qui représentent la pointe du domaine de la démonstration automatisée de théorèmes. Avec la sortie de DeepSeek-Prover-V2, nous sommes peut-être en train d'assister à un changement majeur dans la manière d'étudier les mathématiques. Plus qu'une simple avancée technologique, ce modèle représente un nouveau paradigme permettant aux humains de collaborer avec l'IA pour résoudre des problèmes complexes.

Entre-temps, l'attente de DeepSeek-R2 s'est intensifiée. Comme l'a dit un internaute, "Tapez sur cette petite baleine bleue, quand diable R2 sera-t-il envoyé !".

Si vous souhaitez utiliser les comptes exclusifs officiels GPT Plus, Claude Pro, Grok Super, vous pouvez contacter notre équipe professionnelle (wx : abch891) si vous ne savez pas comment recharger votre compte.