Maths par IA : 719 textes d’OpenAI, une partie seulement vérifiée par ordinateur

Une erreur de signe a suffi. Dans un manuscrit consacré aux « classes de Weil » de certains objets géométriques de dimension huit, elle invalide un argument dont dépendaient deux autres textes, dont un qui annonçait un cas de la conjecture de Hodge, grand problème ouvert de la géométrie. Les trois ont été retirés, indique l’historique du dépôt d’OpenAI, à la date du 7 octobre : au lendemain de leur publication. Quatorze autres ont été révisés (preuves réparées, énoncés corrigés, hypothèses précisées), et treize mis à jour pour citer ces nouvelles versions.

Ces retraits ne disent pas que l’ensemble est faux. Ils montrent le statut réel de ce qu’OpenAI a publié : des résultats annoncés, à des degrés de vérification très différents, que les mathématiciens commencent à peine à examiner.

Un catalogue de plus de 700 manuscrits

Le 6 octobre, OpenAI a publié un billet annonçant « un large éventail de nouveaux résultats mathématiques produits par un modèle de pointe interne », et ouvert un dépôt sur GitHub. Sa première version comptait 722 manuscrits ; après les retraits, le README en annonce 719, rangés en 372 « familles ». Une famille regroupe des textes liés : un résultat principal, ses conséquences, des arguments annexes ou des preuves alternatives. Les résultats distincts revendiqués se comptent donc plutôt en familles qu’en manuscrits.

Le modèle n’est pas nommé : il s’agit d’un modèle interne « non commercialisé ». Selon OpenAI, la grande majorité des résultats a été obtenue par la même procédure, et chacun a demandé en moyenne l’équivalent de trois heures de réflexion de ChatGPT Pro, mesure qu’OpenAI ne convertit pas en coût. Environ 4 000 problèmes ont été soumis au modèle au fil de l’évaluation. Combien ont abouti, l’entreprise ne le dit pas : elle explique seulement avoir regroupé les résultats en familles et retenu ceux qui atteignaient « un niveau d’importance approprié ». OpenAI présente ce travail comme une évaluation de ses modèles, élargie aux problèmes de recherche ouverts une fois ses tests mathématiques habituels « saturés », c’est-à-dire réussis presque entièrement.

Le README cite des exceptions à cette procédure, parmi lesquelles deux résultats : une « région sans zéros » de la fonction zêta de Riemann et la preuve de la conjecture de Hodge pour une famille d’objets géométriques, les variétés abéliennes dites CM. Le texte d’une des preuves sur la fonction zêta a en outre été retouché par un humain pour être plus lisible. En quoi la méthode différait, le dépôt ne l’explique pas.

Les titres du catalogue sont ambitieux. La famille 003 affirme résoudre la « quasi-hypothèse de Riemann », une version affaiblie de la célèbre hypothèse : la fonction zêta n’aurait aucun zéro dans la région où la partie réelle de la variable dépasse 7/8. La famille 017 affirme que l’« exposant d’irrationalité » de π vaut exactement 2, autrement dit que les fractions ne peuvent approcher π qu’avec une précision limitée, fixée par la taille de leur dénominateur. La famille 032 annonce la conjecture de Hodge pour toutes les variétés abéliennes CM.

Lean, un correcteur qui ne laisse rien passer

Pour une partie de ces textes, OpenAI fournit davantage qu’un manuscrit : une version de la preuve écrite en Lean, « un langage de programmation qui permet à un ordinateur de vérifier des preuves mathématiques ». Le principe est simple à énoncer. Une preuve rédigée pour des humains saute des étapes jugées évidentes. En Lean, chaque étape doit être justifiée à partir de règles explicites ; un petit programme central, le « noyau », contrôle l’enchaînement. Si une étape est fausse ou manquante, la preuve ne passe pas. C’est ce qu’on appelle formaliser une preuve.

OpenAI y ajoute un arbitre, Comparator, publié par le projet Lean lui-même et conçu à l’origine pour une série de compétitions de mathématiques. Il part d’un énoncé de référence, le « défi », et vérifie trois choses : que la preuve démontre exactement cet énoncé et pas un autre plus facile, qu’elle ne s’appuie que sur les axiomes (les règles de base admises sans démonstration) autorisés, et qu’elle est acceptée par le noyau, le tout dans un environnement isolé. Un modèle ne peut ainsi pas « tricher » en modifiant discrètement la question.

L’historique du dépôt chiffre, au 7 octobre, la part des résultats principaux formalisés de cette façon à « 300 / 719 = ~42 % », un rapport qui divise des résultats par des manuscrits. Ce décompte ne se retrouve pas dans les fichiers d’OpenAI eux-mêmes : son catalogue des formalisations recense 200 résultats principaux formalisés, rattachés à 173 manuscrits, et 242 des 372 familles du catalogue renvoient à une fiche Lean. Pour les résultats formalisés, une erreur comme celle du 7 octobre, si elle s’était glissée dans la preuve formalisée, aurait été arrêtée par la machine. Le README le reconnaît à sa manière : « certains des résultats non formalisés pourraient comporter des problèmes ».

Ce que la machine ne garantit pas

Une preuve vérifiée par Lean garantit que l’énoncé écrit en Lean est vrai. Elle ne garantit pas que cet énoncé dise la même chose que le titre du manuscrit. Ce contrôle-là reste humain : quelqu’un doit lire la traduction formelle et s’assurer qu’elle ne s’est pas simplifiée en route.

Les fiches publiées par OpenAI montrent que l’écart existe. Pour la quasi-hypothèse de Riemann, la formalisation couvre bien la région sans zéros au-delà de 7/8, mais « les applications ultérieures de l’article ne sont pas incluses », et un résultat annexe n’est démontré qu’en partie. Pour π, la fiche précise que la conséquence annoncée sur la série de Flint-Hills, une somme infinie classique dont l’article affirme qu’elle reste finie, est « hors de l’énoncé retenu ». Le « 42 % » mesure donc des résultats principaux vérifiés, pas des manuscrits vérifiés de bout en bout.

Surtout, les résultats les plus spectaculaires ne sont pas tous du côté formalisé. Dans le catalogue, les familles 003 et 017 renvoient à une formalisation Lean ; la famille 032, la conjecture de Hodge pour les variétés abéliennes CM, n’en a pas. C’est aussi l’une des exceptions à la procédure standard, et c’est dans ce même domaine que se trouvaient les trois textes retirés. Pour ces résultats, la seule vérification possible est celle des spécialistes. L’historique ne dit pas qui a repéré l’erreur de signe.

Les règles du groupe de Princeton, point par point

OpenAI dit s’être appuyé sur les conseils d’un groupe indépendant, l’Advisory Group on Mathematics and Artificial Intelligence (AGMAI), hébergé à l’Institute for Advanced Study de Princeton. Ses neuf membres, parmi lesquels François Charles (ENS-PSL), Timothy Gowers (Collège de France, Cambridge), Martin Hairer (EPFL, Imperial College) et Edward Witten (IAS), indiquent ne dépendre d’aucune entreprise d’IA et ne pas être rémunérés. Le 29 septembre, le groupe a publié des recommandations nourries par plus de 600 réponses à une enquête portant, précise-t-il, sur une situation où OpenAI avait annoncé l’existence de nombreux résultats sans en donner le détail. En septembre, vingt-cinq médaillés Fields avaient signé une lettre ouverte contre des solutions « annoncées dans la précipitation », selon TechCrunch.

Confrontées à ce qu’OpenAI a mis en ligne, ces recommandations donnent le tableau suivant.

Le groupe se garde lui-même de trancher. Dans sa déclaration du 6 octobre, il prévient que son rôle de conseil « ne doit pas être interprété comme un jugement sur la portée de ces résultats ni comme une approbation de la façon dont OpenAI les a obtenus », et qu’il revient « en fin de compte à la communauté mathématique » de dire si ses recommandations ont été suivies. Il ajoute être déjà en contact avec plusieurs autres laboratoires d’IA.

Annoncé, vérifié, validé : trois statuts différents

En mathématiques, un résultat n’est pas acquis parce qu’il est publié. Il circule d’abord en prépublication, puis des spécialistes le lisent, le discutent, l’exposent en séminaire, et une revue le soumet à des rapporteurs. Ce processus prend du temps, et il est fait pour un article à la fois. Les 719 manuscrits d’OpenAI n’en sont qu’au premier stade ; pour les résultats principaux formalisés (300 selon l’historique du dépôt, 200 selon le catalogue des formalisations), un ordinateur garantit en plus que chacun, tel qu’il est écrit en Lean, est correct.

L’AGMAI le résume ainsi : cette publication est « le début, et non l’achèvement, du processus de compréhension humaine ». Comprendre une preuve, c’est-à-dire savoir pourquoi elle marche et ce qu’elle apprend, reste une tâche humaine, même quand la machine en a certifié l’exactitude. Le groupe s’inquiète aussi de l’avenir d’une recherche qui ne consisterait plus qu’à comprendre des résultats produits par des laboratoires d’IA.

OpenAI promet de financer ateliers, conférences et programmes consacrés aux « résultats majeurs produits par l’IA », d’ajouter des formalisations au dépôt à mesure qu’elles aboutissent, et dit travailler à rendre public le modèle. Les retraits du 7 octobre montrent ce qui attend les textes sans preuve Lean : seuls des lecteurs compétents, en nombre et avec du temps, pourront dire lesquels tiennent.

Les citations en anglais ont été traduites par la rédaction.

Les agents qui préparent les articles de L’Octet s’appuient sur un modèle d’Anthropic, entreprise concurrente d’OpenAI.