Une IA d'Anthropic aurait résolu une question d'informatique quantique ouverte depuis 2008

Le 6 novembre, une jeune entreprise de Cambridge, dans le Massachusetts, annonce qu'une question posée en 2008 en informatique quantique a trouvé sa réponse. Physical Superintelligence (PSI) affirme avoir démontré la conjecture d'Aaronson-Ambainis, qui porte le nom des chercheurs Scott Aaronson et Andris Ambainis.

Le plus inhabituel, c'est l'auteur de la preuve. Selon PSI, elle a été produite par un système de recherche maison qui faisait tourner plusieurs instances d'un modèle d'Anthropic non public. L'entreprise ne dit pas lequel. Le système aurait livré une preuve complète au troisième jour, acceptée par Lean, un logiciel qui vérifie une à une les étapes d'une démonstration. Il aurait ensuite amélioré deux fois le résultat. Aucune publication dans une revue à comité de lecture n'est annoncée à ce stade.

Les ordinateurs quantiques ont-ils besoin de structure ?

La question est la suivante : un ordinateur quantique peut-il être exponentiellement plus rapide qu'un ordinateur classique sur des données tirées au hasard, sans organisation particulière ? Les accélérations spectaculaires que l'on connaît s'appuient sur une structure du problème. C'est le cas de l'algorithme de factorisation de Peter Shor (1994), qui exploite une périodicité.

Aaronson et Ambainis avaient montré que la réponse dépendait d'un énoncé sur les polynômes : tout polynôme borné, non constant et de faible degré aurait au moins une variable d'entrée qui pèse nettement sur son résultat. Si cet énoncé est vrai, alors pour la plupart des entrées aléatoires, un algorithme classique peut approcher le résultat d'un algorithme quantique sans avoir à lire les données exponentiellement plus de fois. PSI dit avoir obtenu une borne qui ne décroît que polynomialement avec le degré. Les bornes générales connues jusqu'ici décroissaient exponentiellement.

La portée du résultat est précise. Selon The Quantum Insider, il porte sur le nombre de lectures des données, pas sur le temps de calcul. Il vaut pour la plupart des entrées, pas pour toutes. Et il ne signifie pas qu'un ordinateur classique peut reproduire n'importe quel calcul quantique. Pour qui suit la migration post-quantique, il ne concerne pas l'algorithme de Shor, qui menace le chiffrement RSA en s'appuyant justement sur une structure.

Une preuve vérifiée par la machine, mais pas de bout en bout

Le dépôt GitHub de PSI est plus prudent que les titres qu'il a suscités. Il annonce quatre théorèmes démontrés dans Lean, sans « espace réservé » ni « axiome ajouté », et contrôlés par deux vérificateurs indépendants. Mais il précise que c'est au lecteur de vérifier que l'énoncé formalisé correspond bien à la conjecture publiée. L'un des quatre théorèmes s'appuie sur un résultat d'autres chercheurs (Agarwal et Ben-David) qui n'a pas été formalisé. Enfin, l'article rédigé pour les humains n'a pas été vérifié par la machine.

Des humains ont aussi travaillé à cette preuve. David Turturean, de l'équipe technique de PSI, a conçu le système, cadré le problème, fait rédiger au modèle un premier jet de l'article, puis l'a relu. Il assume la responsabilité de son exactitude. Deux conseillers sont intervenus : Jim Halverson a audité la preuve et Phiala Shanahan a commenté la formalisation. La démonstration reprend un plan de Shachar Lovett et Jiapeng Zhang, qui avaient laissé une inégalité sans démonstration. PSI la remplace par une nouvelle inégalité.

En 2019, une première preuve s'était effondrée

Il y a une raison à cette prudence. En novembre 2019, Scott Aaronson saluait sur son blog une preuve de Nathan Keller et Ohad Klein. Les auteurs l'ont ensuite retirée : le mathématicien Paata Ivanisvili y avait trouvé une « faille fatale » dans un lemme. Aaronson a laissé le billet en ligne pour l'histoire.

Cette fois, une équipe de Stanford (Guy Blanc, Jordan Docter, Carmen Strassle et Li-Yang Tan) relit la preuve. Elle avait démontré un cas particulier en août. Elle a envoyé des commentaires et prépare une présentation plus courte. PSI rapporte sa réaction : « C'est un résultat énorme. » Au 8 novembre, nous n'avons trouvé aucune réaction publique d'Aaronson ni d'Ambainis.

Ces annonces se multiplient, comme lorsque OpenAI et Anthropic ont affirmé que leurs IA avaient réfuté une hypothèse clé de l'informatique. Elles posent chaque fois la question de la vérification et de la part qui revient aux humains. C'est l'une des raisons pour lesquelles OpenAI et Anthropic financent, avec la fondation Simons, un programme qui aide les mathématiciens à vérifier ces résultats. Une inconnue demeure : quel modèle d'Anthropic a fait ce travail, et quand d'autres pourront-ils s'en servir ?