Des mathématiciens s’interrogent sur la fiabilité des 719 manuscrits mathématiques générés par l’IA d’OpenAI, après la publication d’un article affirmant que la preuve de Navier-Stokes annoncée par l’entreprise ne correspond pas à sa version vérifiée par ordinateur.
Points clés :
- Le catalogue d’OpenAI est passé de 722 à 719 manuscrits après le retrait de trois articles en raison d’une erreur de signe.
- Trois mathématiciens basés au Royaume-Uni ont documenté deux divergences entre la preuve écrite de Navier-Stokes et son code Lean.
- Les auteurs ne qualifient pas la preuve de fausse, mais estiment que les vérifications automatiques ne remplacent pas l’évaluation par les pairs.
Publication des résultats mathématiques d’OpenAI
L’entreprise a mis en ligne cette collection le 6 octobre. Un rapport publié jeudi a conclu qu’OpenAI s’était écartée des lignes directrices rédigées par un panel indépendant de mathématiciens pour les laboratoires d’IA. Le catalogue comptait initialement 722 manuscrits. OpenAI en a retiré trois dès le lendemain, après la découverte d’une erreur de signe invalidant un argument, ainsi que deux articles qui s’appuyaient dessus.
Ces lignes directrices, publiées le 29 septembre par le Groupe consultatif sur les mathématiques et l’intelligence artificielle (neuf membres), commencent par demander aux laboratoires de cesser de tester des problèmes de mathématiques avancées sur des modèles propriétaires. Le dépôt d’OpenAI indique que les articles proviennent de l’évaluation d’un modèle interne non publié sur des problèmes de recherche ouverts.
Des résumés du raisonnement du modèle n’accompagnent que 10 résultats, et environ 42 % des théorèmes mis en avant ont été formalisés en Lean, un langage qui permet à un ordinateur de vérifier une démonstration.
À lire aussi : Combien gagne le PDG d’Anthropic ? Le dossier d’IPO apporte la réponse
Les zones d’ombre de la preuve de Navier-Stokes
Alexander Bastounis (King’s College London) ainsi que Fabian Circelli et Anders Hansen (Université de Cambridge) ont analysé la preuve de Navier-Stokes qu’OpenAI avait annoncée en septembre. Ils identifient deux endroits où l’argument écrit diverge du code Lean, dont un cas où le code établit une estimation plus faible que celle énoncée dans l’article.
Les auteurs précisent qu’ils ne se prononcent pas sur la validité de la preuve rédigée. Leur propos est plus ciblé : Lean confirme que le théorème final est vrai, écrivent-ils, mais il ne garantit pas que les étapes intermédiaires, celles que lit un humain, soient toutes correctes. De telles démonstrations nécessitent donc toujours un examen par les pairs.
Le médaille Fields Terence Tao a écrit, le 6 octobre, que des problèmes sont désormais résolus par des « prompteurs d’IA » qui ne comprennent pas suffisamment les sorties pour répondre aux questions ou présenter les travaux. La professeure de Harvard Melanie Matchett Wood, membre du groupe consultatif, souligne qu’aucun humain ne maîtrise ces résultats au moment de leur publication : « et c’est maintenant que le vrai travail commence ».
La controverse autour des preuves d’OpenAI
Le groupe consultatif rappelle que seule la communauté mathématique au sens large peut juger du degré de conformité d’OpenAI à ses recommandations. Ce contrôle intervient après un mois tendu. OpenAI a annoncé le résultat sur Navier-Stokes le 8 septembre, déclenchant un différend sur l’attribution avec le mathématicien de l’université de New York Tristan Buckmaster. Trois jours plus tard, 25 médaillés Fields publiaient une déclaration alertant sur les risques que des résultats produits à la chaîne par l’IA font peser sur la discipline.
À suivre : Les 722 articles de mathématiques d’OpenAI sont publics, aux mathématiciens de les juger
