Mathocalypse : OpenAI publie plus de 700 papiers censés résoudre des centaines de problèmes de maths

Bon courage pour la review — OpenAI vient d'ouvrir la plus grosse pull request de l'histoire des mathématiques.

Sur le dépôt openai/math, l'entreprise a déposé plus de 700 manuscrits produits par l'un de ses modèles internes, le tout sous licence Apache 2.0 (vous avez donc le droit de forker la conjecture des jeux uniques, si le cœur vous en dit).

Ils prétendent résoudre des centaines de problèmes ouverts, dont certains résistaient aux chercheurs depuis des décennies.

Scott Aaronson, chercheur en informatique théorique à l'université du Texas (passé lui-même par OpenAI), y voit l'un des plus grands jours de l'histoire des mathématiques et parle de Mathocalypse. Petit souci : personne n'a encore vraiment relu tout ça.

Moins de la moitié des résultats vérifiés

Le dépôt est rangé comme un vrai projet, jusqu'au bloc BibTeX prêt à copier pour citer chaque papier.

Son auteur, en revanche, n'a pas de nom : c'est un modèle interne d'OpenAI, jamais sorti, à qui l'entreprise a posé environ 4 000 problèmes avant de retenir ces manuscrits (719 à ce jour), répartis en 372 familles de résultats.

Chaque résultat retenu aurait coûté en moyenne l'équivalent de trois heures de réflexion de ChatGPT Pro, ce qui ne dit rien du prix des tentatives ratées.

Pour la fiabilité, OpenAI mise sur Lean, un langage de programmation dans lequel on écrit une démonstration comme du code : si le vérificateur l'accepte, chaque étape logique est valide. C'est l'équivalent mathématique d'une CI qui passe au vert, limites comprises, puisqu'une preuve Lean ne vaut que si l'énoncé a été correctement traduit (comme une suite de tests au vert qui vérifierait la mauvaise spec).

Environ 42 % des résultats principaux sont formalisés ainsi, soit 300 sur 719.

Le README prévient lui-même que certains résultats non formalisés pourraient poser problème, et le premier revert n'a pas traîné : une trentaine d'heures après la publication, l'historique du dépôt annonçait des réparations dans 14 manuscrits et le retrait de trois autres, plombés par une erreur de signe.

Parmi eux figure un papier que Scott Aaronson citait parmi les avancées partielles du lot. Celui-ci porte sur un cas particulier de la conjecture de Hodge, l'un des sept problèmes du millénaire que le Clay Mathematics Institute a mis à prix en 2000, à 1 million de dollars chacun.

Trois résultats qui sortent du lot

La pépite la plus commentée reste la conjecture des jeux uniques, formulée en 2002 par Subhash Khot.

Elle porte sur toute une série de problèmes d'optimisation trop durs pour être résolus parfaitement en temps raisonnable, où l'on se contente donc de solutions approchées. La conjecture affirme que pour ces problèmes, les meilleures approximations qu'on connaît déjà sont aussi les meilleures possibles.

En clair, inutile de chercher un algo plus malin : on aurait déjà trouvé les meilleurs (sauf si P = NP, mais c'est une autre histoire 👀).

Deux résultats parleront davantage aux devs, puisqu'ils touchent à des calculs qu'on croyait optimisés au maximum. Le premier concerne la transformée de Fourier discrète (celle de la FFT qui tourne dans vos codecs audio) : la vitesse atteinte en 1965 par l'algorithme de Cooley et Tukey n'avait jamais été battue.

Le second porte sur la multiplication de très grands nombres, dont Schönhage et Strassen avaient deviné la limite de vitesse dès 1971, une limite que David Harvey et Joris van der Hoeven n'ont atteinte qu'en 2019. Le modèle d'OpenAI prétend passer sous ces deux plafonds.

Le progrès reste microscopique : dans la formule de vitesse, un exposant qui valait 1 passerait à 0,9999999999999, à quelques 9 près selon Scott Aaronson.

Inutile de mettre à jour vos BigInt : l'algorithme de 2019 était déjà galactique, c'est-à-dire qu'il ne s'enclenche que sur des nombres comptant plus de chiffres qu'il n'y a d'atomes dans l'univers observable. Votre CPU ne verra jamais la différence, mais si le résultat tient, un record vieux de plus de 60 ans sera tombé, au moins sur le papier.

La communauté mathématique accuse le coup

La conjecture des jeux uniques, c'est aussi le problème sur lequel travaille depuis toujours Dana Moshkovitz, spécialiste de la théorie de la complexité à l'université du Texas et épouse de Scott Aaronson.

Son verdict sur la preuve publiée par OpenAI est sévère : le papier est mal écrit, ses citations tombent souvent à côté et il reste illisible sans l'aide d'une IA.

Le lendemain de la publication, elle commençait pourtant à comprendre... après avoir passé la journée à se faire expliquer la preuve par Astra, le dernier modèle phare d'OpenAI.

Sur Hacker News, un passionné de théorie des graphes qui a consacré 24 ans, par intermittence, à la conjecture de Barnette raconte une autre histoire.

Posée en 1969, cette conjecture affirme qu'une certaine famille de graphes admet toujours un circuit passant une fois et une seule par chaque sommet. Le lot d'OpenAI prétend l'avoir résolue, sans preuve Lean pour le confirmer. Ce passionné épluche désormais le papier, et à première vue, l'approche ressemble à une piste qu'il avait envisagée puis abandonnée il y a 24 ans.

Des recommandations à moitié suivies

Pour encadrer cette publication, OpenAI dit s'être appuyé sur les conseils d'un groupe consultatif sur les mathématiques et l'IA, réuni à l'Institute for Advanced Study et indépendant des entreprises d'IA, qui compte notamment trois médaillés Fields (Timothy Gowers, Edward Witten, Martin Hairer) et le Français François Charles, professeur à l'École normale supérieure.

Ce groupe avait publié le 29 septembre ses recommandations, sorte de CONTRIBUTING.md pour labos d'IA.

Il y demandait de déposer les résultats sur une archive qui n'appartient à aucun labo, de donner le nom du modèle, de citer les travaux antérieurs, de rédiger des articles lisibles et de ne pas en faire des opérations marketing. Et surtout, d'arrêter de tester des problèmes avancés sur des modèles propriétaires, inaccessibles au reste de la communauté.

OpenAI a coché une partie des cases, mais pour le reste, le dépôt lui appartient (l'entreprise dit chercher une solution d'hébergement gérée par la communauté), le modèle n'a pas de nom, et les papiers sont encore loin d'être lisibles.

Le labo de Sam Altman promet d'ailleurs de mieux soigner les citations et la présentation des résultats lors des prochaines itérations, et s'engage à financer des ateliers, des conférences et des programmes dédiés pour aider la communauté à digérer ces résultats.

Le jour même de la publication, le groupe consultatif a par ailleurs précisé que son rôle ne valait ni jugement sur la portée de ces résultats ni aval du processus qui les a produits, et qu'il revenait à la communauté de dire si ses conseils avaient été suivis (on a connu des LGTM plus enthousiastes).

Il faut dire que l'entreprise traîne déjà quelques casseroles dans le domaine : en août dernier, le mathématicien Stephen Miller parlait de manquement à l'intégrité scientifique après avoir retrouvé, sans citation, un argument tiré de l'un de ses articles de 2016 dans l'une des dix avancées attribuées à Astra.

En septembre, Tristan Buckmaster, mathématicien à l'université de New York, reprochait à OpenAI d'avoir profité de ses travaux non publiés pour annoncer la résolution d'un autre problème du millénaire (les équations de Navier-Stokes), ce que l'entreprise conteste.

Or c'est le modèle à l'origine de cette annonce qui a produit les centaines de papiers publiés cette semaine sur GitHub. Quant à la review, elle reste entièrement à la charge des mathématiciens (bon chance).