L'ESSENTIEL EN 30 SECONDES

  • Physical Superintelligence (PSI) a annoncé le 6 novembre que son système de recherche, qui aurait fonctionné selon elle avec un modèle non public d'Anthropic, a trouvé une démonstration de la conjecture d'Aaronson-Ambainis.
  • Le code Lean 4 publié ne contient ni preuve laissée en suspens ni axiome ajouté, mais la fidélité de l'énoncé formel à la conjecture d'origine reste à confirmer par des lecteurs humains.
  • Aucune relecture dans une revue n'a été signalée ; quatre chercheurs cités par PSI étudient la démonstration complète et préparent une présentation plus courte.

Physical Superintelligence (PSI), une jeune entreprise qui applique l'IA à la recherche en physique, a annoncé le 6 novembre que son système de recherche interne avait produit une démonstration complète de la conjecture d'Aaronson-Ambainis. D'après Unite.AI et Silicon Report, PSI indique que ce système faisait tourner des instances d'un modèle non public d'Anthropic et qu'il a abouti au troisième jour d'exécution, avant d'être relancé pour obtenir deux améliorations supplémentaires. Le dépôt public attribue à des « modèles d'IA » les énoncés, le premier jet et le code Lean, sans nommer de fournisseur : le lien avec Anthropic repose donc sur l'annonce de PSI.

Que dit la conjecture ?

Les ordinateurs quantiques offrent des accélérations spectaculaires sur certains problèmes dotés d'une structure cachée, comme la factorisation. La conjecture, formulée en 2008 par Scott Aaronson et Andris Ambainis, porte sur le cas inverse. En termes mathématiques, elle affirme que tout polynôme borné et de faible degré sur des entrées booléennes possède au moins une variable ayant une influence notable sur sa valeur. Les deux chercheurs ont montré qu'il en découlerait qu'un algorithme quantique effectuant un certain nombre de requêtes peut être imité, sur la plupart des entrées, par un algorithme classique n'en demandant que polynomialement plus. Autrement dit : pas d'avantage quantique exponentiel sur des données aléatoires et sans structure. Le problème est réputé difficile : une prépublication de 2019 qui revendiquait une démonstration a été retirée après la découverte d'une faille, comme l'avait signalé Aaronson sur son blog.

Ce qui a été vérifié, et ce qui ne l'est pas

Le dépôt, qui fixe la version 4.33.0 de Lean et de Mathlib, précise que la bibliothèque n'utilise aucun « sorry » ni axiome supplémentaire et que la relecture par le noyau a été validée par des vérificateurs indépendants. Le README détaille aussi les limites : il revient au lecteur de confirmer que l'énoncé formel, baptisé PrintedConjecture, traduit fidèlement la conjecture, et l'article destiné aux humains n'est pas vérifié par la machine. Une variante donnant une constante plus fine s'appuie sur un résultat extérieur non formalisé ; selon le README, les théorèmes principaux n'en dépendent pas.

David Turturean, de PSI, a conçu le système et se déclare responsable de l'exactitude de l'article. Les documents de PSI citent Guy Blanc, Jordan Docter, Carmen Strassle et Li-Yang Tan, auteurs en août d'un résultat sur un cas particulier, qui y voient « un énorme résultat » ; ils préparent une version condensée. Aucune relecture par une revue ni réaction publique d'Aaronson ou d'Ambainis n'avait été signalée au moment de la rédaction. Le raisonnement s'appuie sur une stratégie de Shachar Lovett et Jiapeng Zhang, en remplaçant une inégalité que leur plan laissait non démontrée.