OpenAI publie 719 preuves mathématiques, l'AGMAI juge les standards non atteints

OpenAI diffuse 719 manuscrits sans répondre à toutes les exigences de l'AGMAI

OpenAI a publié cette semaine des centaines de solutions présentées comme répondant à certains des problèmes mathématiques les plus difficiles au monde. Le laboratoire indique avoir consulté un groupe consultatif de mathématiciens de haut niveau pour éviter la controverse née de la dernière fois qu'un de ses modèles a résolu un problème ancien, selon TechCrunch.

L'Advisory Group on Mathematics and Artificial Intelligence (AGMAI), hébergé par l'Institute for Advanced Studies de l'université de Princeton, réunit neuf chercheurs de premier plan issus d'institutions internationales. Fin septembre, l'organisation a publié des lignes directrices à destination des laboratoires de pointe qui s'attaquent aux problèmes mathématiques.

Dans un communiqué sur ce nouvel ensemble de preuves, l'AGMAI rappelle qu'« il revient en dernier ressort à la communauté mathématique d'évaluer dans quelle mesure nos recommandations ont été suivies avec succès ».

La première demande de l'AGMAI non respectée

La première requête de l'organisation était « d'arrêter de tester des problèmes mathématiques avancés sur des modèles propriétaires ». Or OpenAI indique explicitement évaluer ses modèles propriétaires sur des problèmes de recherche ouverts en mathématiques.

Sollicité par TechCrunch pour une évaluation plus détaillée de cette publication, l'AGMAI n'a pas répondu. Le laboratoire a suivi certains principes, notamment la diffusion rapide des résultats et la fourniture d'informations sur la manière dont les modèles sont parvenus à leurs conclusions. Mais pas pour l'ensemble : seuls dix des 719 manuscrits comportaient la publication de la chaîne de raisonnement du modèle.

Pour les articles que le public ne comprend pas, les mathématiciens préconisent une formalisation des preuves. Or 42 % seulement des preuves diffusées par OpenAI n'avaient pas fait l'objet de ce processus.

Des écarts entre langage naturel et code Lean

En définitive, rien n'indique qu'OpenAI assume « la responsabilité de veiller à ce que la compréhension humaine suive », conformément aux principes de l'AGMAI. Le groupe suggère que le laboratoire finance le travail des mathématiciens qui seront nécessaires pour donner un sens concret à ses solutions.

« Les problèmes sont résolus de manière autonome par des opérateurs d'IA qui ne s'intéressent pas au domaine dans son ensemble une fois leur cible initiale “résolue”, et qui ne comprennent pas suffisamment la sortie de l'IA pour répondre à des questions sur le résultat, donner des exposés ou interagir avec le reste du domaine », a écrit sur les réseaux sociaux Terence Tao, mathématicien de premier plan qui a critiqué l'approche d'OpenAI, après la publication.

Cette difficulté est illustrée par un article diffusé cette semaine par des mathématiciens de l'université de Cambridge et du King's College de Londres, qui interroge la manière dont les laboratoires de pointe abordent ces défis. Lorsqu'un modèle d'IA résout un problème mathématique, il produit d'abord une explication en « langage naturel », puis tente d'exprimer ce résultat en Lean, un langage de programmation censé confirmer l'exactitude de la preuve en la compilant sous forme de code.

Des divergences documentées sur un problème issu de Navier-Stokes

La traduction des preuves en langage naturel vers le code peut toutefois poser problème. L'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 pour un problème dérivé des équations de Navier-Stokes, qui décrivent le comportement complexe des fluides.

Ces divergences n'invalident pas nécessairement l'une ou l'autre solution, mais elles posent la question de savoir si l'on peut se contenter de laisser les modèles formaliser seuls 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 le langage naturel et les artefacts formels », ce que le laboratoire n'a pas fait pour ces publications.

« En raison du phénomène de contresens — mis en évidence dans cet article —, la preuve en langage naturel d'OpenAI et les autres preuves Lean auto-formalisées ne devraient pas, à première vue, être tenues pour fiables sans le même processus de relecture par les pairs et le même examen que les autres preuves », concluent les auteurs de l'article intitulé « lost in translation ».

Les mathématiciens soulignent que lorsqu'un résultat nouveau est découvert par des humains, ceux-ci en assument la responsabilité et dialoguent avec la communauté au moyen d'articles, d'exposés et de séminaires. Ce processus accroît la compréhension des solutions, met au jour des stratégies réutilisables pour d'autres problèmes et permet d'appliquer ces connaissances à des domaines pratiques.

Lorsqu'un modèle est sollicité pour résoudre un problème difficile et livre une solution, « il n'y a pas de compréhension humaine de celle-ci au moment de sa diffusion, et c'est là que le travail commence », a déclaré à TechCrunch Melanie Wood, professeure de mathématiques à l'université Harvard.