DeepSeek-Prover-V2-7B est un modèle de langage open source de grande taille conçu pour le langage de programmation d'IA mathématique Lean 4, publié par l'équipe DeepSeek le 1er mai 2025. Sa caractéristique la plus importante est sa capacité à combiner de manière transparente le raisonnement mathématique informel (c'est-à-dire la méthode de raisonnement couramment utilisée par les humains) avec des preuves formelles rigoureuses, permettant au modèle de penser aussi flexiblement que les humains et d'argumenter aussi rigoureusement que les ordinateurs, réalisant ainsi une fusion intégrée du raisonnement mathématique. Les résultats pertinents de l'article sontDeepSeek-Prover-V2 : Amélioration du raisonnement mathématique formel par apprentissage par renforcement pour la décomposition des sous-objectifs".
Ce tutoriel utilise une seule carte A6000 comme ressource. Ce modèle ne prend en charge que les problèmes de raisonnement mathématique.
2. Exemples de projets
3. Étapes de l'opération
1. Après avoir démarré le conteneur, cliquez sur l'adresse API pour accéder à l'interface Web
Si « Modèle » n'est pas affiché, cela signifie que le modèle est en cours d'initialisation. Étant donné que le modèle est grand, veuillez patienter environ 1 à 2 minutes et actualiser la page.
2. Après être entré sur la page Web, vous pouvez démarrer une conversation avec le modèle
Comment utiliser
4. Discussion
🖌️ Si vous voyez un projet de haute qualité, veuillez laisser un message en arrière-plan pour le recommander ! De plus, nous avons également créé un groupe d’échange de tutoriels. Bienvenue aux amis pour scanner le code QR et commenter [Tutoriel SD] pour rejoindre le groupe pour discuter de divers problèmes techniques et partager les résultats de l'application↓
Soutien au projet
Merci à l'utilisateur Github xxxjjjyyy1 Déploiement de ce tutoriel.
