Quand OpenAI a publié des centaines de solutions revendiquées à certains des problèmes mathématiques les plus difficiles du monde cette semaine, le laboratoire de pointe a déclaré avoir consulté un groupe consultatif de mathématiciens d’élite afin d’éviter la controverse survenue la dernière fois que l’un de ses modèles a résolu un problème ancien du domaine.
Mais OpenAI n’a pas atteint ces normes, notamment là où les mathématiciens insistaient sur la nécessité d’une compréhension humaine d’un résultat mathématique. C’est d’autant plus préoccupant qu’un nouvel article a mis en évidence des écarts entre la solution en langage naturel et la solution formellement exprimée d’un problème à un million de dollars soi-disant résolu par les modèles d’OpenAI.
L’Advisory Group on Mathematics and Artificial Intelligence, hébergé par l’Institute for Advanced Studies de l’Université de Princeton, est composé de neuf chercheurs de renom issus d’institutions du monde entier.
L’organisation a publié des directives pour les laboratoires de pointe qui résolvent des problèmes mathématiques fin septembre. Dans un communiqué concernant ce dernier lot de preuves, l’AGMAI a déclaré que « il revient en fin de compte à la communauté mathématique d’évaluer dans quelle mesure nos recommandations ont été suivies avec succès. »
Cependant, la première demande de l’organisation était « de cesser de tester des problèmes mathématiques avancés sur des modèles propriétaires. » La publication d’OpenAI indique explicitement qu’elle évalue ses modèles propriétaires à l’aide de problèmes de recherche ouverts en mathématiques.
Le groupe consultatif n’a pas répondu lorsque TechCrunch lui a demandé une évaluation plus approfondie de la dernière publication de preuves d’OpenAI. Le laboratoire a manifestement suivi certains de ses principes, notamment la publication des résultats dès que possible et l’inclusion d’informations sur la manière dont les modèles sont parvenus à leurs conclusions. Mais pas pour tous : seulement dix des 719 manuscrits incluaient la publication de la chaîne de raisonnement du modèle.
Pour les articles que les gens ne comprennent pas, les mathématiciens ont suggéré que les preuves soient formalisées — mais seulement 42% des preuves publiées par OpenAI n’avaient pas subi ce processus.
En fin de compte, il n’est toujours pas certain qu’OpenAI assume « la responsabilité de garantir qu’une compréhension humaine suivra » lors de la publication de ses preuves, conformément aux principes de l’AGMAI. L’AGMAI a suggéré qu’OpenAI devrait contribuer à financer le travail des mathématiciens humains qui seront nécessaires pour rendre les solutions du laboratoire véritablement significatives.
« Des problèmes sont résolus de manière autonome par des提示eurs en IA qui n’ont aucun intérêt pour le domaine plus large lui-même une fois leur cible initiale “résolue”, et qui ne comprennent pas suffisamment les résultats de l’IA pour répondre à des questions sur le résultat, donner des conférences ou interagir autrement avec le reste du domaine », a écrit Terence Tao, un mathématicien de renom qui a critiqué l’approche d’OpenAI, sur les réseaux sociaux après la publication.
Ce problème est illustré par un article publié cette semaine par des mathématiciens de l’Université de Cambridge et du King’s College de Londres qui s’interroge sur la manière dont les laboratoires de pointe abordent ces défis.
Lorsque les modèles d’IA résolvent des problèmes mathématiques, ils créent d’abord une explication en « langage naturel », puis tentent d’exprimer ce résultat en Lean, un langage de programmation qui confirme en théorie l’exactitude de la preuve en la compilant sous forme de code.
Cependant, il peut y avoir des problèmes dans la manière dont les modèles traduisent leurs preuves en langage naturel en code ; cet article documente au moins deux divergences entre la preuve en langage naturel et le code Lean derrière la solution qu’OpenAI a proposée à un problème dérivé des équations de Navier-Stokes qui décrivent le comportement complexe des fluides.
Ces divergences ne réfutent pas nécessairement l’une ou l’autre solution, mais elles soulèvent des questions sur la possibilité de simplement se fier aux modèles pour formaliser leurs propres solutions sans intervention humaine. C’est l’une des raisons pour lesquelles l’AGMAI a demandé à OpenAI « d’inclure des métadonnées lisibles par machine corrélant les artefacts en langage naturel et formels », ce que le laboratoire de pointe n’a pas fait avec ces publications.
« En raison du phénomène de mauvaises traductions — mis en évidence dans cet article — les preuves NL d’OpenAI et
les autres preuves Lean autoformalisées ne devraient pas être a priori considérées comme fiables sans le même processus d’évaluation par les pairs et
l’examen auquel les autres preuves sont soumises », concluent les auteurs de l’article « lost in translation ».
Les mathématiciens soulignent que lorsque de nouveaux résultats sont découverts par des humains, ceux-ci en assument la responsabilité et s’engagent auprès de la communauté élargie par des articles, des conférences et des séminaires. Ce processus accroît la compréhension des solutions, identifie des stratégies pouvant servir à résoudre d’autres problèmes et permet d’appliquer les nouvelles connaissances dans des domaines pratiques.
Lorsqu’un modèle est sollicité pour résoudre un problème difficile et produit une solution, « il n’y a pas de compréhension humaine de ces solutions au moment de leur publication, et c’est alors que le travail commence », a déclaré à TechCrunch Melanie Wood, professeure de mathématiques à l’Université Harvard.