PSI prezintă o demonstrație verificată automat a conjecturii Aaronson-Ambainis

Physical Superintelligence a anunțat la 6 noiembrie 2026 că un sistem intern de cercetare, care rula instanțe ale unui model Anthropic nepublic, găsise o demonstrație a conjecturii Aaronson-Ambainis, o problemă de calcul cuantic rămasă deschisă din 2008.

Sistemul a produs o demonstrație completă în a treia zi a unei rulări pe propria infrastructură a PSI, iar asistentul de demonstrare Lean a acceptat-o. Apoi, PSI i-a atribuit sistemului probleme deschise conexe, iar acesta a îmbunătățit rezultatul de două ori înainte ca Lean să accepte versiunea finală. Manuscrisul și formalizarea în Lean 4 sunt publice.

Ce spune conjectura despre accelerarea oferită de calculul cuantic

Întrebarea este când pot calculatoarele cuantice să fie exponențial mai rapide decât cele clasice. Algoritmul de factorizare al lui Shor din 1994 depinde de structură: datele de intrare conțin un tipar repetitiv pe care algoritmul îl poate exploata. Rezultatul PSI se referă la cazul opus, al datelor de intrare aleatorii sau nestructurate, în care un asemenea tipar lipsește, în general.

În modelul interogărilor, un algoritm clasic citește câte un bit la fiecare interogare, în timp ce o interogare cuantică poate fi distribuită în superpoziție pe mai multe poziții ale datelor de intrare. Explicația PSI leagă acest model de polinoame: după T interogări cuantice, probabilitatea ca algoritmul să răspundă „da” este un polinom mărginit al biților de intrare, de grad cel mult 2T. Prin urmare, simularea algoritmului cuantic devine o problemă de estimare a acelui polinom fără a citi un număr exponențial de biți de intrare.

În lucrarea lor originală, Scott Aaronson și Andris Ambainis au formulat conjectura că orice polinom mărginit de grad mic are o variabilă cu influență mare. Ei au demonstrat că, dacă conjectura este adevărată, orice algoritm cuantic cu T interogări poate fi simulat pentru majoritatea datelor de intrare de un algoritm clasic care face un număr de interogări polinomial în T. Rezultatul implică o creștere polinomială, nu exponențială, a numărului de interogări clasice, pentru orice eroare de aproximare fixă și orice fracție fixă de date de intrare excluse; el nu exclude avantajele cuantice exponențiale pentru probleme cu o structură adecvată.

Formal, depozitul analizează un polinom real p de grad cel mult d, ale cărui valori pe cubul discret sunt cuprinse între 0 și 1. Dacă varianța sa pentru o intrare aleasă uniform aleatoriu este cel puțin ε, atunci o coordonată are o influență de cel puțin (8√15 / (125π⁴)) · ε^(5/2) / d⁶ și, în consecință, de cel puțin (ε/d)⁷. Influența reprezintă valoarea așteptată a pătratului modificării lui p atunci când se inversează bitul acelei coordonate.

Cum a fost construită și verificată demonstrația

Demonstrația urmează un plan al lui Shachar Lovett și Jiapeng Zhang, bazat pe certificate fracționare și mulțimi de nivel, dar înlocuiește o inegalitate pe care planul o lăsa drept conjectură cu o nouă inegalitate valabilă pentru toate perechile. Un determinant generează o asociere bijectivă între configurațiile de intrare. Potrivit PSI, această asociere depășește asocierea mai slabă din lema Butterfly a lui David Reimer, deoarece limitează și frecvența cu care configurațiile asociate coincid pe fiecare coordonată, o limită necesară pentru noua inegalitate.

Depozitul împarte demonstrația elementară în patru părți: deducerea inegalității pentru toate perechile din determinant și bijecție, integrarea acesteia pe mulțimi de nivel, calcularea mediei pe coordonate și stabilirea unei limite pentru rânduri cu ajutorul unei limite punctuale a sensibilității. Împreună, acești pași dau limita explicită pentru influență.

Potrivit auditului consemnat în depozit, dezvoltarea formală nu conține demonstrații incomplete sau axiome adăugate. Declarațiile au fost verificate din nou cu nucleul Lean și cu lean4lean, o implementare independentă a verificatorului de tipuri Lean. Într-o rulare izolată, un comparator care folosea nucleele nanoda și Lean a acceptat cele patru teoreme finale; pe o a doua mașină, a acceptat o soluție mică și corectă și a respins patru soluții intenționat greșite.

Aceste verificări au limite explicite. Cititorul trebuie să confirme în continuare că enunțul formal corespunde conjecturii publicate. Lucrarea redactată pentru cititori nu este ea însăși verificată automat, iar nucleul și compilatorul Lean, definițiile din Mathlib și mașinile folosite la verificare fac în continuare parte din baza de încredere.

Rolurile oamenilor și evaluarea experților

David Turturean, membru al personalului tehnic al PSI, a dezvoltat și a rulat sistemul de cercetare, a delimitat problema, a îndrumat modelul să pregătească o primă versiune, a revizuit-o și răspunde de corectitudinea lucrării. Depozitul precizează că modelele de inteligență artificială au produs enunțurile matematice, prima versiune și formalizarea Lean. Jim Halverson a auditat demonstrația, iar Phiala Shanahan a comentat formalizarea.

Anunțul vine după o lucrare trimisă la 19 august 2026 de Guy Blanc, Jordan Docter, Carmen Strassle și Li-Yang Tan. Acești autori stabiliseră consecința privind simularea clasică pentru algoritmi cuantici paraleli, demonstrând că un algoritm cu t interogări și d runde poate fi simulat pentru majoritatea datelor de intrare cu t^(O(d²)) interogări clasice. PSI spune că toți cei patru au citit demonstrația integrală, au trimis observații și pregătesc o expunere mai scurtă pentru experți.

În evaluarea lor publicată de PSI, cercetătorii au scris: „Este un rezultat major. El rezolvă o conjectură veche de decenii, cu implicații importante pentru natura problemelor care permit accelerări cuantice. Demonstrația se bazează pe mai multe direcții de cercetare din analiza funcțiilor booleene și combinatorica probabilistă și le dezvoltă. Toate sunt reunite într-un mod aproape magic.”

Verificarea imediată este neobișnuit de concretă: nuclee independente pot reexecuta argumentul codificat, însă experții trebuie în continuare să confirme că enunțul codificat corespunde conjecturii lui Aaronson și Ambainis și să evalueze părțile lucrării care nu sunt formalizate în Lean. Această delimitare stabilește ce anume confirmă verificările automate și ce necesită în continuare o analiză matematică umană.