Source: Xinzhiyuan
[New Zhiyuan Introduction] Tout à l'heure, le rapport technique Deepseek-Prover-V2 est également là! Le document de 34 pages révèle le cœur de la formation du modèle - Recursion + apprentissage en renforcement, qui améliore considérablement le raisonnement mathématique. Certaines personnes louent: Deepseek a trouvé le bon chemin vers AGI!
Tout à l'heure, Deepseek-Prover-V2 a été officiellement libéré.
Cette fois, Deepseek-Prover-V2 fournit deux tailles de modèle: les paramètres 7b et 671b.
Deepseek-Prover-V2-671B: Formation basée sur Deepseek-V3-base, la performance la plus inférieure.
Deepseek-Prover-v2-7b: construit basé sur Deepseek-Prover-v1.5-base, la longueur de contexte est étendue jusqu'à 32ktoken.
Face étreinte: https://huggingface.co/deepseek-ai/deepseek-prover-v2-671b
Github: https://github.com/deepseek-ai/deepseek-prover-v2/tree/main
Dans le même temps, le rapport technique a également été publié.
Lien papier: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/deepseek_prover_v2.pdf
Hier, Deepseek a soudainement ouvert le modèle 671b sur l'étreinte Face, et il y aura bientôt un suivi.
Les preuves mathématiques sont considérablement améliorées
Le cœur de la formation de Deepseek-Prover-V2 cette fois est de s'appuyer sur "Recursion + Renforcement Learning".
Premièrement, Deepseek-V3 démontera des théorèmes complexes et génèrera une série de sous-objectifs et d'idées d'inférence. L'algorithme GRPO apprend ensuite automatiquement à choisir la solution optimale parmi une variété de solutions candidates.
En ce qui concerne la technologie publiée cette fois, les internautes ont salué que cela conduira à une IA numérique qui dépasse les humains et favorise considérablement la recherche sur l'IA.
La méthode peut être résumé comme suit:
· Optimiser les algorithmes pour obtenir des modèles plus rapides et plus intelligents
· Révéler les informations sur le comportement de la "boîte noire" de l'IA
· Concevoir une meilleure architecture sans essais et erreurs sans fin
· Accélérer l'analyse des données pour réaliser des percées plus rapides
Par conséquent, cela nous amène à AGI et génère une super intelligence. En quelques années, l'IA produira des mathématiques avancées que les humains ne peuvent pas comprendre.
Plus précisément, Deepseek-Prover-V2 est spécifiquement utilisé pour la preuve formelle du théorème dans Lean 4.
Parmi eux, les données d'initialisation sont collectées via le processus de preuve récursif du théorème entraîné par Deepseek-V3.
Pendant la formation à froid de démarrage, Deepseek-V3 sera invité à décomposer des problèmes complexes en une série de sous-objectifs, puis la preuve de sous-objectifs résolus est synthétisée dans un processus de chaîne de réflexion, et combinée avec le raisonnement progressif de Deepseek-V3, il fournit un début initial à froid pour l'apprentissage du renforcement.
Grâce à ce processus, le raisonnement mathématique informel et formel peut être intégré dans un modèle unifié.
Pour résumer, les points forts sont les suivants.
Générer des données d'inférence de démarrage à froid: méthode de recherche de preuve récursive
Pour construire un ensemble de données de démarrage à froid, l'équipe a développé un processus de preuve récursif simple et efficace du théorème, en utilisant Deepseek-V3 comme outil unifié pour effectuer une décomposition et une formalisation de sous-objectif.
Deepseek-V3 sera invité à décomposer le théorème en croquis de haut niveau. Pendant ce temps, ces étapes de preuve sont officialisées dans Lean 4, résultant en une série de sous-objectifs.
Tout d'abord, un modèle 7B plus petit est utilisé pour traiter la recherche de preuve de chaque sous-cible pour réduire la charge de calcul.
Une fois que les étapes de décomposition des problèmes difficiles sont résolues, une preuve formelle complète étape par étape est combinée avec le processus de chaîne de réflexion correspondant généré par Deepseek-V3 pour générer des données d'inférence à démarrage à froid.
· Apprentissage du renforcement basé sur des données de démarrage à froid synthétiques
L'équipe a soigneusement sélectionné un sous-ensemble de problèmes difficile - il ne peut pas être résolu de bout en bout avec un prover 7B, mais tous les sous-cibles décomposées ont été résolues avec succès.
En intégrant la preuve de tous les sous-objectifs, l'équipe a construit une preuve formelle complète du problème d'origine.
Cette preuve est ensuite attachée à la chaîne de réflexion de Deepseek-V3, qui décrit la décomposition du lemme corresp...
[Courte citation de 8% de l'article original]