Une preuve assistée par IA fixe une limite à l’avantage quantique sur des entrées aléatoires

Un système de PSI utilisant un modèle non public d’Anthropic a produit une preuve de la conjecture d’Aaronson-Ambainis, formalisée dans Lean.

Une machine quantique peut interroger plusieurs positions d’une suite de bits en superposition. Scott Aaronson et Andris Ambainis ont cherché combien de lectures il faudrait à une machine classique pour imiter ses réponses sur des entrées tirées au hasard. Le laboratoire Physical Superintelligence (PSI) a publié une démonstration de leur conjecture le 6 novembre, accompagnée d’une formalisation dans Lean. Ce que mesure l’écart entre les deux machines

Dans le cadre étudié, la machine répond par oui ou par non. Sur la plupart des suites de bits tirées uniformément, une machine classique peut estimer la probabilité que la machine quantique réponde oui. Pour une précision donnée et une proportion fixée d’exceptions, le nombre de lectures classiques nécessaires est borné par un polynôme en fonction du nombre de consultations quantiques. Cette borne concerne les accès aux données. Le temps de calcul total, qui inclut le travail entre deux lectures, relève d’une autre question.

En août, Guy Blanc, Jordan Docter, Carmen Strassle et Li-Yang Tan avaient établi cette conséquence dans un cas particulier. Leur résultat concernait les procédures quantiques qui consultent leur entrée en un nombre fixe de tours parallèles. D’après PSI, les quatre chercheurs ont examiné la nouvelle preuve, transmis leurs commentaires et préparent un exposé plus court. Le bit qui mérite d’être lu

Le lien avec les polynômes vient de la probabilité de répondre oui. Après (T) consultations quantiques, cette probabilité s’écrit comme un polynôme de degré au plus (2T) dans les bits de l’entrée. Dans leur article d’origine, Aaronson et Ambainis avaient montré qu’une borne sur l’influence de ces bits permettrait de déterminer lesquels lire du côté classique.

Pour mesurer l’influence d’un bit, on inverse sa valeur, on prend le carré de la variation du polynôme et on en fait la moyenne sur toutes les entrées possibles. La preuve garantit que, si le polynôme varie et reste compris entre 0 et 1, au moins un bit atteint un seuil d’influence lié au degré et à la variance. À variance donnée, ce seuil diminue comme l’inverse d’une puissance du degré et reste indépendant du nombre total de bits. La démonstration reprend une piste de Shachar Lovett et Jiapeng Zhang et s’appuie sur un résultat de David Reimer pour apparier des configurations de bits. De la recherche assistée à la vérification dans Lean

Selon PSI, son système a produit une première preuve complète au troisième jour d’une exécution sur son infrastructure, en utilisant un modèle non public d’Anthropic. David Turturean a conçu le système, délimité le problème, lancé l’exécution et relu le manuscrit préparé à partir des résultats.

La formalisation publiée dans le dépôt Lean 4 couvre la borne d’influence qui constitue le cœur de la conjecture. Deux implémentations indépendantes du vérificateur ont accepté les preuves formelles, selon les journaux de PSI. Les conséquences pour le calcul quantique sont développées dans le manuscrit, hors du périmètre de cette vérification.