DeepSeek a lancé un modèle spécialisé dans le domaine de la démonstration de théorèmes mathématiques appelé Prover-V2, dont l'objectif est d'utiliser l'IA pour prouver automatiquement des théorèmes mathématiques dans le système de vérification formelle Lean 4.
Pourquoi cette direction est-elle importante ?
La démonstration de théorèmes mathématiques est un terrain d'essai extrême pour les capacités de l'IA. Car les mathématiques n'acceptent pas le « à peu près juste » – une preuve est soit totalement correcte, soit fausse. Il n'existe pas de « preuve correcte à 95 % ».
Les systèmes de vérification formelle (comme Lean 4) vérifient chaque étape du raisonnement logique de la même manière qu'un compilateur vérifie la syntaxe. Si une étape est incorrecte, l'ensemble de la preuve génère une erreur. C'est le test le plus rigoureux pour la capacité de raisonnement logique de l'IA.
Les performances de Prover-V2
Sur le benchmark miniF2F, Prover-V2 a obtenu des résultats proches ou égaux aux meilleurs résultats actuels. La méthode qu'il utilise est la décomposition en sous-objectifs – diviser une preuve complexe en une série de sous-objectifs plus petits, et les résoudre un par un.
Cela ressemble beaucoup à la façon de penser des mathématiciens humains : face à un problème difficile, ils pensent d'abord « pour prouver A, je dois d'abord prouver B et C, et pour prouver B, je dois d'abord confirmer D… »
Différence avec les modèles de raisonnement généralistes
Les modèles généralistes (GPT, Claude, Gemini) effectuent un raisonnement mathématique basé sur le Chain-of-Thought – essentiellement un « raisonnement pas à pas en langage naturel ». Cette approche fonctionne bien pour les problèmes simples, mais pour les preuves complexes, une faille logique peut facilement apparaître à une étape.
Prover-V2 suit la voie formelle, où chaque étape est vérifiée par Lean 4. L'avantage est qu'il n'y a pas d'« hallucinations » ; l'inconvénient est que le champ d'application est très restreint – il ne fonctionne qu'à l'intérieur de systèmes formels.
Signification
La démonstration de théorèmes mathématiques est une direction qui semble très de niche, mais qui a un impact profond. Si l'IA parvient réellement à prouver de manière fiable des théorèmes complexes dans des systèmes formels, elle pourrait être appliquée dans des domaines tels que la vérification de logiciels, la vérification de matériel, les preuves cryptographiques et une série d'autres domaines critiques.
L'investissement de DeepSeek dans cette direction montre qu'ils ne se contentent pas de rivaliser sur les benchmarks des grands modèles généralistes – ils construisent également sérieusement des outils scientifiques fondamentaux.
Source de référence : CocoLoop, article de DeepSeek Prover-V2