En bref

  • OpenAI a publié 722 manuscrits mathématiques dans 372 familles de résultats sur GitHub, provenant d'un modèle interne non publié.
  • Seuls 162 des 722 articles ont un résultat principal formalisé en Lean, et OpenAI avertit que certains résultats non formalisés pourraient poser problème.
  • Andrew Sutherland, du MIT, affirme que l'affirmation d'un prompt unique et d'un agent unique n'est pas vérifiée tant que le modèle n'est pas publié, et que la publication omet les prompts qu'un groupe consultatif de l'Institute for Advanced Study a recommandé de divulguer.

OpenAI a publié 722 manuscrits mathématiques sur GitHub mardi, tous produits par un modèle interne que l'entreprise n'a pas publié. Un porte-parole d'OpenAI a déclaré que presque tout provenait d'un seul prompt confié à un seul agent d'IA, bien que certains aient pu nécessiter plusieurs tentatives.

C'est une affirmation audacieuse et une percée potentiellement importante dans le domaine des mathématiques. Mais tout le monde n'est pas convaincu, ni ne gobe cet enthousiasme.

Myriad : jusqu'où Nvidia va-t-il monter ? Cliquez pour faire votre prédiction.
Myriad : jusqu'où Nvidia va-t-il monter ? Cliquez pour faire votre prédiction.

« Jusqu'à ce qu'ils publient le modèle et que les gens puissent reproduire leurs résultats, et à moins que cela ne se produise, je pense que vous devriez considérer toute affirmation concernant la résolution de problèmes en une seule fois avec un seul agent comme non vérifiée », a déclaré Andrew Sutherland, mathématicien au MIT, à Scientific American. « Nous devrions demander des reçus », a-t-il dit.

Les articles sont regroupés en 372 « familles » de résultats connexes, et une famille peut regrouper un théorème principal avec des arguments d'accompagnement, des conséquences ou des preuves alternatives. Cela fait de 722 un décompte de manuscrits, et non de problèmes résolus. OpenAI affirme avoir soumis environ 4 000 problèmes au modèle et avoir conservé les résultats qu'il jugeait suffisamment significatifs pour être publiés.

Le résultat moyen a utilisé l'équivalent d'environ trois heures de calcul de réflexion de ChatGPT Pro, selon OpenAI. L'affirmation sur Navier-Stokes le mois dernier était très différente, avec 10 000 agents coordinateurs travaillant pendant 88 heures.

OpenAI a publié des résumés de raisonnement abrégés pour 10 des résultats. Cela dit, seuls 162 des 722 articles sont accompagnés d'un résultat principal vérifié par ordinateur, selon un catalogue de formalisation dans le dépôt. Cela représente environ 22 % de la collection, traduits en Lean, un logiciel qui vérifie mécaniquement chaque étape logique.

OpenAI lui-même déclare que tous les manuscrits n'ont pas de formalisations Lean et que « certains des résultats non formalisés pourraient poser problème ». En d'autres termes, une grande partie de ce qu'ils ont publié pourrait être erroné.

Une vérification Lean réussie confirme uniquement que la preuve découle de l'énoncé tel qu'écrit en Lean. Elle ne montre pas que l'énoncé correspond au problème original, ni que le résultat est nouveau ou important, ce qui est la partie que les mathématiciens doivent maintenant juger.

Et c'est là que les chercheurs haussent les sourcils.

« Il est désormais établi que l'IA peut produire des arguments mathématiques dans des situations où l'humain qui l'a sollicitée n'est pas capable de comprendre les arguments, de les vérifier ou d'en assumer la responsabilité », a déclaré dans un communiqué l'Institute for Advanced Study de Princeton, dans le New Jersey. « Nous croyons que la compréhension humaine des mathématiques reste d'une importance primordiale. Comment, dans cette nouvelle ère, pouvons-nous œuvrer pour un nouveau paradigme qui inclut la compréhension humaine des mathématiques comme partie intégrante d'une production savante responsable ? »

D'autres, cependant, comme le professeur Abhishek Saha, sont plutôt enthousiastes. « C'est un très grand jour pour les mathématiques », a-t-il écrit, mais il a noté que la plupart des problèmes relèvent des catégories « d'avancées exceptionnelles au sein d'un programme existant » ou de « percées surprenantes ».

Cela signifie que la plupart des problèmes de l'ensemble sont intéressants, mais pas impossibles ni révolutionnaires comme les problèmes du millénaire. Cette place est réservée à exactement un problème sur les 722 : l'hypothèse quasi-Riemann.

La publication est également en deçà de ce qu'un groupe consultatif de l'Institute for Advanced Study a recommandé le 29 septembre : le nom du modèle, les invites, une chaîne de pensée résumée, le temps pris et le coût de calcul pour chaque résultat. OpenAI a publié des chiffres moyens de calcul et 10 résumés de raisonnement, mais aucune invite, et affirme qu'elle travaille encore à publier le modèle de manière responsable.

Daniel Litt, un mathématicien de l'Université de Toronto, a adopté le point de vue opposé, soutenant qu'il n'y a aucune raison de demander à l'entreprise de garder secrètes les réponses à ces questions mathématiques.

Anthropic a emprunté une voie différente avec sa preuve du dernier théorème de Fermat vérifiée par Lean le mois dernier, publiant les 13 millions de lignes publiquement sur GitHub. Cette preuve formalisait un théorème qu'Andrew Wiles a publié en 1995, plutôt que de revendiquer de nouveaux résultats.

OpenAI affirme qu'elle ajoutera des formalisations Lean au fur et à mesure qu'elle les obtiendra ; pour l'instant, 162 des 722 manuscrits en ont une.