PSI melder om maskinverifisert bevis for Aaronson–Ambainis-formodningen

Physical Superintelligence kunngjorde 6. november 2026 at et internt forskningssystem, som kjørte instanser av en ikke-offentlig Anthropic-modell, hadde funnet et bevis for Aaronson–Ambainis-formodningen, et problem innen kvantedatabehandling som har stått uløst siden 2008.

Systemet produserte et fullstendig bevis på den tredje dagen av en kjøring på PSIs egen infrastruktur, og Lean-bevisassistenten godtok det. PSI ga deretter systemet beslektede, åpne problemer, og det forbedret resultatet to ganger før Lean godtok den endelige versjonen. Manuskriptet og Lean 4-formaliseringen er offentlig tilgjengelige.

Hva formodningen sier om kvantefortrinn

Spørsmålet er når kvantedatamaskiner kan være eksponentielt raskere enn klassiske maskiner. Shors faktoriseringsalgoritme fra 1994 avhenger av struktur: Inndataene inneholder et gjentakende mønster som algoritmen kan utnytte. PSIs resultat tar for seg den motsatte situasjonen, med tilfeldige eller ustrukturerte inndata, der et slikt mønster som regel mangler.

I spørringsmodellen leser en klassisk algoritme én bit per spørring, mens en kvantespørring kan være fordelt i superposisjon over mange posisjoner i inndataene. PSI forklarer sammenhengen mellom denne modellen og polynomer slik: Etter T kvantespørringer er sannsynligheten for at algoritmen svarer ja, et begrenset polynom av inngangsbitene med grad på høyst 2T. Å simulere kvantealgoritmen blir dermed et spørsmål om å anslå dette polynomet uten å lese eksponentielt mange inngangsbiter.

I den opprinnelige artikkelen sin formodet Scott Aaronson og Andris Ambainis at ethvert begrenset polynom av lav grad har en svært innflytelsesrik variabel. De beviste at dersom formodningen holder, kan enhver kvantealgoritme med T spørringer simuleres for de fleste inndataene av en klassisk algoritme som gjør polynomisk mange spørringer i T. Konsekvensen er en polynomisk snarere enn eksponentiell vekst i antallet klassiske spørringer, for enhver fast tilnærmingsfeil og andel utelatte inndata; resultatet utelukker ikke eksponentielle kvantefortrinn for problemer med egnet struktur.

Formelt sett ser repositoriet på et reelt polynom p med grad på høyst d, der verdiene på den diskrete kuben ligger mellom 0 og 1. Hvis variansen over uniformt tilfeldige inndata er minst ε, har en koordinat en innflytelse på minst (8√15 / (125π⁴)) · ε^(5/2) / d⁶, og følgelig minst (ε/d)⁷. Innflytelse er den forventede kvadrerte endringen i p når biten for den aktuelle koordinaten snus.

Slik ble beviset utarbeidet og kontrollert

Argumentasjonen følger en plan av Shachar Lovett og Jiapeng Zhang, basert på fraksjonelle sertifikater og nivåmengder, men erstatter en ulikhet som planen lot stå som en formodning, med en ny ulikhet som gjelder for alle par. En determinant gir en en-til-en-paring av inndatakonfigurasjoner. Ifølge PSI går denne paringen lenger enn den svakere paringen i David Reimers Butterfly Lemma, fordi den også begrenser hvor ofte parvise konfigurasjoner er enige i hver koordinat – en grense som trengs for den nye ulikheten.

Repositoriet deler det elementære beviset inn i fire deler: å utlede ulikheten for alle par fra determinanten og bijeksjonen, å integrere den over nivåmengder, å ta gjennomsnitt over koordinater og å etablere en radgrense med en punktvis sensitivitetsgrense. Til sammen gir disse trinnene den eksplisitte innflytelsesgrensen.

Ifølge den dokumenterte revisjonen i repositoriet inneholder den formelle utviklingen ingen plassholdere for bevis eller ekstra aksiomer. Deklarasjonene ble kjørt gjennom på nytt med Leans kjerne og lean4lean, en uavhengig implementering av Leans typesjekker. I en sandkassegodkjente et sammenligningsverktøy som bruker nanoda- og Lean-kjernene, de fire endelige teoremene. På en annen maskin godtok verktøyet én korrekt, liten løsning og avviste fire løsninger som med hensikt var feil.

Disse kontrollene har uttrykkelige begrensninger. Leseren må fortsatt bekrefte at den formelle formuleringen samsvarer med den trykte formodningen. Den leservennlige artikkelen er ikke i seg selv maskinverifisert, og Leans kjerne og kompilator, definisjonene i Mathlib og maskinene som brukes til kontrollen, inngår fortsatt i tillitsgrunnlaget.

Menneskelige roller og ekspertgjennomgang

David Turturean, som er medlem av PSIs tekniske stab, utviklet og kjørte forskningssystemet, avgrenset problemet, ba modellen sette sammen et førsteutkast, gjennomgikk utkastet og er ansvarlig for at artikkelen er korrekt. Repositoriet opplyser at AI-modeller produserte de matematiske påstandene, førsteutkastet og Lean-formaliseringen. Jim Halverson reviderte beviset, og Phiala Shanahan kommenterte formaliseringen.

Kunngjøringen kommer etter en artikkel innsendt 19. august 2026 av Guy Blanc, Jordan Docter, Carmen Strassle og Li-Yang Tan. Disse forfatterne hadde fastslått konsekvensen for klassisk simulering av parallelle kvantealgoritmer og bevist at en algoritme med t spørringer og d runder kan simuleres for de fleste inndataene med t^(O(d²)) klassiske spørringer. PSI opplyser at alle fire har lest hele beviset, kommet med kommentarer og forbereder en kortere framstilling for eksperter.

I vurderingen som ble publisert av PSI, skrev forskerne: «Dette er et svært viktig resultat. Det løser en flere tiår gammel formodning med viktige implikasjoner for hva slags problemer som kan gi kvantehastighetsgevinster. Beviset bygger på og videreutvikler flere forskningslinjer innen analyse av boolske funksjoner og probabilistisk kombinatorikk. Alt er satt sammen på en nærmest magisk måte.»

Den umiddelbare prøven er uvanlig konkret: Uavhengige kjerner kan reprodusere det kodede argumentet, mens eksperter fortsatt må bekrefte at den kodede påstanden samsvarer med formodningen til Aaronson og Ambainis, og vurdere de delene av artikkelen som ligger utenfor Lean. Denne arbeidsdelingen avgjør hva maskinens kontrollering fastslår, og hva som fortsatt krever menneskelig matematisk gjennomgang.