Une preuve écrite par l'IA attend que des humains la comprennent

Une preuve remise en main propre

Une preuve de 1 147 pages, écrite par une intelligence artificielle, attend que des humains la comprennent. Le 16 octobre, OpenAI demande à David Gross, prix Nobel de physique 2004, d'en prendre la garde, avec une mission : décider de la meilleure façon de la rendre au monde. Il choisit quatre collègues pour l'aider.

Dix jours plus tard, le 26 octobre, OpenAI annonce le résultat. Le lendemain, les cinq physiciens publient un texte de deux pages hébergé par l'institut de Gross, à Santa Barbara. Une phrase y résume leur position : avant de publier la preuve, ils veulent être convaincus qu'elle est juste.

D'habitude, dans cette histoire, c'est l'entreprise qui annonce trop vite et les chercheurs qui demandent à voir. Cette fois, le texte est entre les mains des chercheurs. Ce sont eux qui ferment le coffre.

Ce qu'OpenAI dit avoir prouvé

L'annonce est plus large que ce qu'on en a retenu. OpenAI dit avoir obtenu une preuve d'existence mathématiquement rigoureuse de certaines théories quantiques des champs en quatre dimensions. Parmi elles, la chromodynamique quantique, la théorie qui décrit la force nucléaire forte, celle qui colle les quarks entre eux à l'intérieur des protons. Et la plus simple des théories de grande unification qui contiennent les particules du Modèle standard.

Pour mesurer l'ambition : la physique utilise ces théories depuis cinquante ans, avec un succès spectaculaire, sans que personne ait jamais démontré qu'elles existent au sens des mathématiciens. C'est un peu comme habiter une maison depuis des décennies sans avoir jamais vu ses fondations.

Au passage, OpenAI dit prouver aussi l'existence de la théorie de Yang-Mills « pure », sans les quarks. C'est ce morceau qui a fait les titres, parce qu'il touche un des sept problèmes du millénaire de l'Institut Clay, dotés d'un million de dollars chacun. OpenAI le présente elle-même comme « une partie » du problème.

L'énoncé officiel, rédigé par Arthur Jaffe et Edward Witten, demande deux choses à la fois, et pour tout groupe de symétrie d'un certain type : que la théorie existe, et qu'elle présente un « écart de masse », c'est-à-dire que ses particules ne puissent pas avoir une masse arbitrairement proche de zéro. OpenAI ne revendique rien sur l'écart de masse, et ne précise pas, dans son annonce, pour quels groupes vaut sa preuve de Yang-Mills pur. Les cinq physiciens rangent l'écart de masse parmi les défis encore ouverts. Le prix n'est pas en jeu.

Lean vérifie la preuve, pas la question

Il y a pourtant un argument qui semble rendre la prudence inutile. OpenAI dit avoir attendu, avant de publier, que la preuve soit formalisée en Lean, un langage où l'ordinateur contrôle chaque étape d'une démonstration. Elle dit l'avoir terminée le 16 octobre, le jour même où elle sollicitait Gross, sans que personne d'extérieur ait encore pu la contrôler. Si une machine a déjà tout passé au crible, pourquoi attendre ?

La réponse est dans le texte des cinq. Leur premier travail ne consiste pas à relire la preuve ligne à ligne. Il consiste à vérifier que les définitions et l'énoncé traduits dans Lean correspondent bien à ceux qu'utilisent physiciens et mathématiciens, et que la version formelle colle à la version rédigée.

Lean garantit qu'on a bien démontré ce qu'on lui a demandé de démontrer. Il ne dit rien sur la question elle-même. Un correcteur orthographique parfait ne signale pas une lettre adressée à la mauvaise personne. On l'avait déjà écrit ici à propos de Navier-Stokes : Lean ne vérifie que l'énoncé qu'on lui soumet.

Sur un sujet où le seul fait de définir proprement une théorie quantique en quatre dimensions est un problème ouvert, la traduction de l'énoncé n'a rien d'une formalité. Une fois cette comparaison faite, les cinq promettent de publier la preuve Lean, puis, quand ils seront satisfaits, les 1 147 pages avec leur évaluation.

Des gardiens qui ne rendent pas de comptes à OpenAI

Qui sont ces cinq ? David Gross, colauréat du Nobel pour la liberté asymptotique, une propriété clé de ces théories. Arthur Jaffe, coauteur de l'énoncé du problème. Michael Douglas, auteur cette année d'un état des lieux du problème ; Igor Klebanov, spécialiste du confinement des quarks ; Nikita Nekrasov, prix Dannie Heineman de physique mathématique 2023.

On pourrait croire qu'OpenAI a choisi ses propres relecteurs. Ce n'est vrai que pour un des cinq. Leur texte le dit : OpenAI a demandé à Gross de prendre la garde de la preuve, puis Gross a choisi le reste du comité. Les cinq ajoutent qu'ils travaillent au nom de la communauté académique et n'ont « aucune responsabilité » envers OpenAI. Ils ne valident rien : la preuve leur « paraît » être une étape importante.

OpenAI, de son côté, a joué le jeu. Ses trois résultats du jour suivent trois stratégies, conseillées par leurs gardiens respectifs : le résultat de maths est publié tel quel, celui d'informatique est confié à un groupe mais mis en ligne d'emblée, celui de physique est laissé à la décision du groupe. Au relevé du 29 octobre, le dépôt public d'OpenAI ne contient aucun fichier sur Yang-Mills.

Les mathématiciens veulent tout, tout de suite

Le désaccord public ne vient pas d'OpenAI, il vient des mathématiciens. Le 26 octobre, le jour même où OpenAI annonçait que le groupe de physique garderait les documents, l'Advisory Group on Mathematics and Artificial Intelligence, un groupe consultatif indépendant hébergé par l'Institute for Advanced Study de Princeton, demande à OpenAI de publier sans délai la preuve rédigée et sa version Lean. Ses neuf membres comptent Edward Witten, Timothy Gowers et Martin Hairer. Le texte est collectif.

Son argument tient en deux phrases : la compréhension doit se construire au grand jour, avec le même accès pour tous, et puisque la formalisation est terminée de l'aveu même d'OpenAI, plus aucune raison scientifique ne justifie d'attendre. Le groupe dit son « grand respect » pour les scientifiques sollicités.

La veille, il avait publié une critique plus générale de la pratique qui consiste, pour un laboratoire, à désigner des savants qui verront un résultat avant tout le monde. Une longueur d'avance pour quelques-uns, un choix qui reflète les réseaux de l'entreprise, et des noms qui finissent par servir de caution. Le même groupe avait déjà refusé de servir de caution lors de la publication des 722 manuscrits d'OpenAI. Il précise quand même que ses recommandations visent les mathématiques, pas forcément les autres sciences.

Les deux auteurs de l'énoncé du problème se retrouvent ainsi de part et d'autre : Jaffe dans le comité qui garde la preuve, Witten dans le groupe qui en réclame la publication.

La vérification, nouveau goulot

Personne, dans cette dispute, ne prétend que la preuve est fausse. La question est de savoir qui la voit en premier, et combien de temps il faut à des humains pour savoir ce qu'elle démontre vraiment. La machine a rendu sa preuve de Yang-Mills le 9 septembre, selon OpenAI. Pour en digérer la méthode et le sens, préviennent les cinq, il faudra du temps.

OpenAI reconnaît elle-même le prix de sa méthode : choisir les premiers gardiens pèse sur qui s'implique en premier et crée une asymétrie d'information. Les cinq physiciens, eux, appellent leur démarche une expérience sur la façon dont la communauté académique peut absorber le savoir produit par les IA. Et ils annoncent qu'ils avanceront très prudemment.