DeepSeek a introduit DeepSeek-Prover-V2, un modèle de langage large (LLM) open source révolutionnaire méticuleusement conçu pour le domaine complexe de la preuve formelle de théorèmes au sein du framework Lean 4. Ce nouveau modèle exploite un pipeline récursif de preuve de théorèmes, exploitant la puissance du modèle de base DeepSeek-V3 de pointe de DeepSeek. Lean 4, la dernière itération du prouveur de théorèmes Lean, est un assistant interactif de preuve développé par Microsoft Research. Ce langage de programmation fonctionnel sophistiqué et système interactif de preuve de théorèmes permet aux mathématiciens et aux informaticiens de construire des preuves formelles avec une vérification machine inégalée.
Le projet représente un pas de géant vers la réduction de l’écart entre le raisonnement mathématique formel et informel. En capitalisant sur les capacités inhérentes des LLM à usage général, il cherche à aborder efficacement le domaine hautement structuré de la preuve formelle de théorèmes. L’équipe de recherche de DeepSeek postule que leur approche innovante reflète les processus cognitifs employés par les mathématiciens humains lors de la construction de preuves, disséquant méticuleusement des théorèmes complexes en composantes plus gérables et compréhensibles.
Extension du Framework d’Évaluation : Introduction de ProverBench
Dans une démarche significative visant à renforcer la rigueur de leurs recherches, l’équipe de DeepSeek a considérablement élargi son framework d’évaluation avec l’introduction de ProverBench, une toute nouvelle collection de benchmarks méticuleusement conçue spécifiquement pour l’évaluation complète des capacités de preuve formelle de théorèmes. Cette collection complète sert de ressource précieuse pour évaluer les performances des LLM dans le contexte des mathématiques formelles.
"Au-delà des benchmarks conventionnels, nous sommes fiers de présenter ProverBench, une collection méticuleusement organisée de 325 problèmes formalisés, pour enrichir notre processus d’évaluation. Cette collection comprend 15 problèmes soigneusement sélectionnés provenant directement des récentes compétitions de l’American Invitational Mathematics Examination (AIME), plus précisément des années 24-25," ont précisé les chercheurs.
L’inclusion des problèmes de l’AIME dans l’ensemble de données ProverBench est particulièrement remarquable, car elle introduit un ensemble de problèmes mathématiques stimulants et bien établis qui sont largement reconnus au sein de la communauté mathématique. Cela fournit une base standardisée et rigoureuse pour évaluer les performances de DeepSeek-Prover-V2 et la comparer à d’autres approches.
Résultats Initiaux Prometteurs : S’Attaquer aux Problèmes de l’AIME
Les résultats initiaux découlant de tests rigoureux sur ces problèmes stimulants de l’AIME ont révélé des performances exceptionnellement prometteuses de leur modèle spécialisé de preuve de théorèmes méticuleusement conçu. L’équipe de DeepSeek rapporte fièrement que DeepSeek-Prover-V2 a démontré ses prouesses en résolvant avec succès un nombre impressionnant de 6 des 15 problèmes de l’AIME qui lui ont été présentés. En comparaison, le modèle à usage général DeepSeek-V3, lors de l’utilisation de techniques de vote majoritaire, a réussi à résoudre 8 problèmes.
Ces résultats soulignent le potentiel des LLM spécialisés et à usage général pour résoudre des problèmes mathématiques complexes. Bien que le modèle à usage général ait présenté un taux de réussite légèrement supérieur dans ce benchmark particulier, le modèle spécialisé de preuve de théorèmes a démontré sa compétence dans le raisonnement mathématique formel.
Imitation de la Construction Humaine de Preuves : Une Approche de Chaîne de Pensée
"Étant donné les défis bien documentés que les modèles à usage général rencontrent souvent lorsqu’ils tentent de produire des preuves Lean complètes, nous avons stratégiquement demandé à DeepSeek-V3 de générer uniquement une esquisse de preuve de haut niveau, omettant délibérément les détails complexes. La chaîne de pensée résultante aboutit à un théorème Lean composé d’une séquence d’énoncés have, chacun étant méticuleusement conclu par un espace réservé sorry, indiquant efficacement un sous-objectif qui doit être résolu. Cette approche innovante reflète élégamment le style humain de construction de preuves, dans lequel un théorème complexe est progressivement réduit à une séquence de lemmes plus gérables," a expliqué l’équipe de DeepSeek.
Cette approche innovante consistant à générer des esquisses de preuves de haut niveau s’aligne sur la façon dont les mathématiciens abordent souvent les preuves complexes. En se concentrant sur la structure globale et les étapes clés, le modèle peut efficacement guider le raffinement et l’achèvement ultérieurs de la preuve.
Une Stratégie Méthodique : Aborder Chaque Composante de la Preuve Individuellement
Le système emploie ensuite méticuleusement une stratégie méthodique et structurée pour aborder chaque composante individuelle de la preuve. Cette approche systématique garantit que chaque aspect de la preuve est soigneusement examiné et abordé de manière logique et cohérente. Le système crée une approche hautement structurée de la preuve de théorèmes, s’appuyant sur les résultats précédemment établis pour assurer une base solide à chaque étape suivante.
"En tirant parti des sous-objectifs générés par DeepSeek-V3, nous adoptons une stratégie de résolution récursive pour résoudre systématiquement chaque étape de preuve intermédiaire. Nous extrayons les expressions de sous-objectifs des énoncés have pour les substituer aux objectifs originaux dans les problèmes donnés, puis nous incorporons les sous-objectifs précédents comme prémisses. Cette construction permet de résoudre les sous-objectifs suivants en utilisant les résultats intermédiaires des étapes précédentes, favorisant ainsi une structure de dépendance plus localisée et facilitant le développement de lemmes plus simples," ont détaillé les chercheurs.
La stratégie de résolution récursive est un aspect clé de la capacité du système à gérer les preuves complexes. En décomposant le problème en sous-objectifs plus petits et plus gérables, le système peut appliquer efficacement ses capacités de raisonnement à chaque composante individuelle.
Optimisation des Ressources de Calcul : Un Modèle Spécialisé de 7B Paramètres
Pour optimiser efficacement les ressources de calcul et assurer un traitement efficace, le système emploie stratégiquement un modèle plus petit et hautement spécialisé de 7B paramètres pour traiter les lemmes décomposés. Cette approche est cruciale pour gérer efficacement les demandes de calcul associées aux recherches de preuves approfondies, garantissant que le système peut fonctionner efficacement sans être submergé par la complexité de l’espace de recherche. L’approche aboutit finalement à une preuve complète dérivée automatiquement lorsque toutes les étapes décomposées sont résolues avec succès.
"Le framework algorithmique fonctionne en deux étapes distinctes, exploitant deux modèles complémentaires : DeepSeek-V3 pour la décomposition des lemmes et un modèle de prouveur de 7B pour compléter les détails de la preuve formelle correspondante," ont décrit les chercheurs.
Cette approche en deux étapes permet au système de tirer parti des forces d’un grand modèle à usage général et d’un modèle spécialisé plus petit. Le grand modèle est utilisé pour générer des esquisses de preuves de haut niveau, tandis que le petit modèle est utilisé pour remplir les détails et compléter la preuve formelle.
Synthétiser des Données de Raisonnement Formel : Un Chemin Naturel
Cette architecture méticuleusement conçue établit efficacement un chemin naturel et intuitif pour synthétiser des données de raisonnement formel, fusionnant de manière transparente le raisonnement mathématique de haut niveau avec les exigences strictes et rigoureuses de la vérification formelle. Cette intégration est essentielle pour assurer la fiabilité et la crédibilité des résultats du système.
"Nous sélectionnons un sous-ensemble de problèmes stimulants qui restent non résolus par le modèle de prouveur de 7B de bout en bout, mais pour lesquels tous les sous-objectifs décomposés ont été résolus avec succès. En composant les preuves de tous les sous-objectifs, nous construisons une preuve formelle complète pour le problème original," ont expliqué les chercheurs.
Cette approche permet au système d’apprendre de ses erreurs et d’améliorer sa capacité à résoudre des problèmes complexes. En identifiant les sous-objectifs spécifiques qui causent des difficultés, le système peut concentrer ses efforts sur l’amélioration de ses performances dans ces domaines.
Préoccupations et Défis : Les Détails de Mise en œuvre Sous Surveillance
Malgré les réalisations techniques indéniables démontrées par DeepSeek-Prover-V2, certains experts dans le domaine ont soulevé des préoccupations pertinentes concernant certains détails de mise en œuvre. Elliot Glazer, un mathématicien principal très respecté chez Epoch AI, a souligné des problèmes potentiels qui justifient une enquête plus approfondie.
Certaines préoccupations concernant l’article DeepSeek-Prover-V2. Exemples potentiellement mal formalisés, et la discussion sur le Lean zulip suggère que les preuves de PutnamBench sont absurdes et utilisent un sorry implicite (peut-être caché dans la tactique apply?) non rapporté dans leur boucle read-eval-print.
Ces préoccupations mettent en évidence les défis permanents inhérents à l’espace de la vérification formelle, où même les détails de mise en œuvre les plus minimes et apparemment insignifiants peuvent avoir un impact disproportionné sur la validité et la fiabilité globales des résultats. Le processus de vérification formelle exige une attention constante aux détails et un respect méticuleux des normes établies.
Le potentiel d’exemples mal formalisés et la possibilité de tactiques "sorry" cachées dans les preuves de PutnamBench soulèvent des questions importantes sur la rigueur et l’exhaustivité du processus de vérification. Ces préoccupations soulignent la nécessité d’un examen continu et d’une vérification indépendante des résultats.
Disponibilité et Ressources : Démocratiser l’Accès à la Preuve Formelle de Théorèmes
DeepSeek a rendu son Prover-V2 disponible en deux tailles de modèles distinctes, répondant à un éventail diversifié de ressources de calcul et d’objectifs de recherche. La première version est un modèle de 7B paramètres construit sur leur précédent Prover-V1.5-Base, avec une longueur de contexte étendue allant jusqu’à 32K tokens. La deuxième version est un modèle de 671B paramètres nettement plus grand, entraîné sur DeepSeek-V3-Base. Les deux modèles sont désormais facilement accessibles sur HuggingFace, une plateforme de premier plan pour le partage et la collaboration sur les modèles d’apprentissage automatique.
En plus des modèles eux-mêmes, DeepSeek a également mis à disposition sur HuggingFace l’ensemble de données ProverBench complet, contenant 325 problèmes méticuleusement formalisés à des fins d’évaluation. Cet ensemble de données complet fournit aux chercheurs et aux développeurs une ressource précieuse pour évaluer les performances de leurs modèles et les comparer à DeepSeek-Prover-V2.
En rendant ces ressources librement disponibles, DeepSeek démocratise l’accès à la technologie de preuve formelle de théorèmes et favorise la collaboration au sein de la communauté de recherche. Cette approche open source est susceptible d’accélérer les progrès dans le domaine et de conduire à de nouvelles percées dans le raisonnement et la vérification automatisés.
Cette publication donne aux chercheurs et aux développeurs les ressources nécessaires pour approfondir les capacités et les limites de cette technologie. En offrant un accès ouvert aux modèles et à l’ensemble de données ProverBench, DeepSeek encourage davantage d’exploration et d’efforts de collaboration pour répondre aux préoccupations soulevées par les experts dans le domaine. Cette approche collaborative détient la clé pour déchiffrer les complexités de la preuve formelle de théorèmes et consolider la fiabilité de ces avancées révolutionnaires.