Une preuve assistée par l’IA éclaire les limites de l’avantage quantique
La preuve publiée par Physical Superintelligence concerne une question précise sur les algorithmes quantiques. Une formalisation et une lecture par des chercheurs apportent deux contrôles distincts.
Physical Superintelligence a publié le 6 novembre une preuve de la conjecture d’Aaronson-Ambainis. L’équipe indique que son système de recherche a travaillé avec un modèle Anthropic non public. Le 8 novembre, Scott Aaronson a expliqué pourquoi il juge la preuve crédible. Des chercheurs du MIT et de Stanford ont aussi publié leur propre présentation du raisonnement.
La conjecture porte sur le nombre de lectures de l’entrée
Le problème demande quand un calculateur quantique peut obtenir une réponse avec beaucoup moins d’accès aux données qu’un calculateur classique. Pour certaines tâches structurées, l’écart peut être très grand. La question étudiée ici est différente. Elle porte sur des problèmes où il faut répondre par oui ou par non et où l’entrée est une suite de bits choisie au hasard.
La présentation de PSI explique comment cette question mène à une conjecture sur les polynômes. Après un certain nombre de consultations de l’entrée, la probabilité que l’algorithme quantique réponde oui s’exprime sous la forme d’un polynôme de faible degré. Si la valeur de ce polynôme varie suffisamment, la conjecture affirme qu’au moins un bit exerce une influence minimale que l’on peut borner. En exploitant cette propriété, un algorithme classique peut estimer cette probabilité sur la plupart des entrées avec un nombre de lectures qui augmente de façon polynomiale.
Une preuve produite dans un système de recherche
PSI attribue le résultat à un système développé en interne. L’équipe dit avoir obtenu une première preuve complète au troisième jour de l’exécution. Elle indique que Lean l’a acceptée et que le système a ensuite amélioré la borne deux fois. Cette chronologie décrit ce que rapporte PSI. Elle ne permet pas de mesurer séparément la contribution du modèle et celle du dispositif qui lui donnait accès aux tâches et aux outils.
La formalisation et la lecture de la preuve répondent à deux questions
Le dépôt de PSI fournit le manuscrit et les fichiers Lean. Il met aussi en regard l’énoncé publié et la proposition formalisée. Lean contrôle les étapes de la preuve pour cette proposition. Le rapprochement des deux formulations permet de vérifier que le contrôle porte sur la question que les chercheurs voulaient résoudre. Le dépôt indique aussi les passages explicatifs du manuscrit qui n’ont pas d’équivalent dans les fichiers de preuve.
Dans son billet du 8 novembre, Scott Aaronson dit croire la preuve correcte en raison du certificat Lean et du travail d’experts qui l’ont relue. Il précise qu’il ne l’a pas encore comprise lui-même. L’exposition de Guy Blanc et de ses coauteurs présente la démarche dans un texte distinct. Les auteurs signalent qu’ils ont privilégié les idées du raisonnement et obtiennent des exposants moins serrés que ceux du résultat original. Leur texte est daté du 7 novembre.
La portée reste celle d’un problème de complexité
Le résultat précise ce qu’on peut gagner en nombre de consultations pour les problèmes et les entrées étudiés. D’autres algorithmes quantiques exploitent une structure qui sort de ce cadre. On retrouve cette distinction entre énoncé, preuve et lecture humaine dans l’examen des résultats mathématiques publiés par OpenAI. Ici, la preuve publiée et l’exposition permettent de suivre la portée du résultat au-delà du récit sur le modèle employé.