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 parution d’un article affirmant que la preuve de Navier-Stokes publiée par la société 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 identifié deux divergences entre la preuve écrite de Navier-Stokes et son code Lean.
- Les auteurs ne jugent pas la preuve fausse, mais soulignent que la vérification automatique ne remplace pas l’évaluation par les pairs.
Publication des résultats d’OpenAI en mathématiques
Le 6 octobre, la société a mis en ligne une collection de manuscrits, et un rapport publié jeudi a montré qu’elle s’écartait 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 qui invalidait un argument, ainsi que deux articles qui en dépendaient.
Ces recommandations, publiées le 29 septembre par le Advisory Group on Mathematics and Artificial Intelligence, composé de 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. Selon le dépôt d’OpenAI, 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 accompagnent seulement 10 résultats, et environ 42 % des énoncés principaux ont été formalisés dans Lean, un langage de programmation qui permet à un ordinateur de vérifier une preuve.
À lire aussi : Combien gagne le CEO d’Anthropic ? Le dossier d’introduction en Bourse donne la réponse
Les failles de la preuve de Navier-Stokes
Alexander Bastounis du King’s College London, ainsi que Fabian Circelli et Anders Hansen de l’Université de Cambridge, ont examiné la preuve de Navier-Stokes qu’OpenAI avait annoncée en septembre. Ils y relèvent deux points de divergence entre l’argument écrit et le code Lean, dont un cas où le code ne démontre qu’une estimation plus faible que celle revendiquée dans l’article.
Les auteurs précisent qu’ils ne se prononcent pas sur la validité de la preuve écrite en tant que telle. Leur critique est plus ciblée : Lean confirme que le théorème final est bien démontré, écrivent-ils, mais il ne garantit pas la solidité des étapes intermédiaires lues par un humain. De telles preuves demeurent donc tributaires d’une relecture par les pairs.
Le médaillé Fields Terence Tao a écrit le 6 octobre que certains problèmes sont désormais « résolus » par des « prompteurs d’IA » qui comprennent trop peu les sorties du modèle pour répondre aux questions ou présenter les résultats. La professeure de Harvard Melanie Matchett Wood, membre du groupe consultatif, souligne que personne ne maîtrise pleinement ces résultats au moment de leur publication, « et c’est là que le vrai travail commence ».
Controverse autour des preuves d’OpenAI
Le groupe consultatif insiste sur le fait que seule la communauté mathématique au sens large peut juger du degré de conformité d’OpenAI à ses recommandations. Cet examen intervient au terme d’un mois tendu. OpenAI a annoncé son résultat sur Navier-Stokes le 8 septembre, déclenchant un différend de paternité avec le mathématicien de l’Université de New York Tristan Buckmaster. Trois jours plus tard, 25 médaillés Fields ont publié une déclaration mettant en garde contre le risque que des résultats produits à la chaîne par l’IA ne nuisent à la discipline.
À suivre : Les 722 articles de mathématiques par IA d’OpenAI sont publics, à la communauté de les évaluer
