Des chercheurs signalent une incohérence dans la preuve de Navier-Stokes d’OpenAI

Les mathématiciens examinent actuellement un large lot de preuves générées par IA publiées par OpenAI le 6 octobre, et certaines de leurs découvertes soulèvent des doutes. Une équipe dirigée par des chercheurs de Cambridge affirme que les versions lisibles par l'homme et vérifiables par ordinateur de la précédente preuve de Navier-Stokes de l'entreprise ne correspondent pas.newscientist

La publication d'octobre comprenait 722 manuscrits, regroupés en 372 familles de résultats sur des problèmes ouverts de longue date. Tous ont été produits par un modèle interne non publié. OpenAI a déclaré que le modèle a consacré environ trois heures de temps de calcul, en moyenne, à chaque solution. Cette publication est intervenue quelques semaines après qu'OpenAI a annoncé avoir résolu le problème de Navier-Stokes, l'un des problèmes du prix du millénaire du Clay Mathematics Institute. L'entreprise affirme que ce nouveau lot permet de progresser sur trois autres problèmes du millénaire, sans toutefois les résoudre complètement.axios+1

Une incohérence dans Lean

OpenAI a publié sa preuve de Navier-Stokes sous deux formes. L'une est rédigée en "langage naturel", le mélange d'anglais et de symboles utilisé par les mathématiciens. L'autre est en Lean, un langage de programmation qui permet à un ordinateur de vérifier chaque étape logique. Selon New Scientist, Anders Hansen de l'Université de Cambridge et ses collègues ont découvert que les deux versions divergent au niveau du Lemme 8.6. La preuve écrite exige qu'une valeur reste inférieure à m + 4. La version Lean exige seulement qu'elle reste inférieure à m + 5, ce qui est une condition plus faible.newscientist

Les chercheurs n'ont pas affirmé que l'une ou l'autre preuve était fausse. Leur préoccupation est que, lorsque l'IA traduit une preuve en Lean et qu'une partie ne compile pas, elle peut modifier discrètement l'argument pour contourner le problème. Il a fallu environ deux semaines à l'équipe pour trouver la divergence. OpenAI a déclaré que ses agents ont passé 88 heures à produire les preuves.newscientist

"Ce qui doit être fait avec toutes ces preuves générées par des modèles de langage, c'est qu'elles devront être lues par des humains, et cela crée un fardeau supplémentaire énorme pour les mathématiciens", a déclaré Hansen.newscientist

OpenAI a déclaré à New Scientist qu'il était au courant de l'incohérence et que cela ne rendait aucune des preuves invalide. L'entreprise a indiqué qu'elle corrigerait les erreurs dans les preuves écrites au fur et à mesure qu'elles seraient découvertes et qu'elle continuerait à formaliser les nouveaux documents. Seuls certains documents sont accompagnés de preuves Lean, et ces preuves Lean n'ont pas été vérifiées manuellement. Kevin Buzzard de l'Imperial College London a déclaré : "Je suis convaincu que le problème de Navier-Stokes a été correctement résolu. Je suis beaucoup moins convaincu que la preuve décrite dans le PDF soit correcte."newscientist

Un domaine divisé

La nouvelle publication a suscité à la fois enthousiasme et inquiétude. Dan Litt de l'Université de Toronto a déclaré à Fortune que "c'est formidable pour les mathématiques", mais il a également averti que l'idée selon laquelle l'IA a "résolu les mathématiques" pourrait affaiblir le soutien à la recherche mathématique humaine. Tristan Buckmaster de l'Université de New York s'est demandé si OpenAI s'était assuré que son modèle ne s'appuyait pas sur des travaux non publiés de mathématiciens humains. Il a déclaré au New York Times : "Je ne pense pas qu'ils aient fait preuve de la diligence requise".fortune+1

Un groupe consultatif indépendant basé à l'Institute for Advanced Study avait émis des recommandations sur la manière dont les preuves générées par IA devraient être publiées. OpenAI en a suivi certaines, mais pas toutes. Le groupe avait également déclaré qu'il ne soutenait pas le fait que les entreprises d'IA testent leurs propres modèles sur des problèmes de recherche ouverts, et OpenAI semble avoir mis cette position de côté.smh+1

Terence Tao de l'UCLA a écrit sur Mastodon que cette publication marque la fin des "Mathématiques 1.0". Il a appelé à une nouvelle ère qui "décentrera le rôle de la résolution brute de problèmes et valorisera le progrès mathématique de manière plus holistique".fortune