PSI rapporterer maskinkontrolleret bevis for Aaronson-Ambainis-formodningen

Physical Superintelligence meddelte den 6. november 2026, at et internt forskningssystem, der kørte instanser af en ikke-offentlig Anthropic-model, havde fundet et bevis for Aaronson-Ambainis-formodningen, et problem inden for kvantecomputere, der havde stået åbent siden 2008.

Systemet udarbejdede et fuldstændigt bevis på den tredje dag af en kørsel på PSIs egen infrastruktur, og Lean-bevisassistenten accepterede det. PSI tildelte derefter systemet beslægtede åbne problemer, og systemet forbedrede resultatet to gange, før Lean accepterede den endelige version. Manuskriptet og Lean 4-formaliseringen er offentligt tilgængelige.

Hvad formodningen siger om kvantefortrin

Spørgsmålet handler om, hvornår kvantecomputere kan være eksponentielt hurtigere end klassiske maskiner. Shors faktoriseringsalgoritme fra 1994 afhænger af struktur: Dens input indeholder et gentaget mønster, som algoritmen kan udnytte. PSIs resultat omhandler det modsatte tilfælde med tilfældige eller ustrukturerede input, hvor et sådant mønster som regel mangler.

I forespørgselsmodellen læser en klassisk algoritme én bit pr. forespørgsel, mens en kvanteforespørgsel kan være fordelt i superposition over mange inputpositioner. PSIs forklaring forbinder denne model med polynomier: Efter T kvanteforespørgsler er sandsynligheden for, at algoritmen svarer ja, et begrænset polynomium i inputbittene med en grad på højst 2T. At simulere kvantealgoritmen bliver derfor et spørgsmål om at estimere dette polynomium uden at læse eksponentielt mange inputbit.

I deres oprindelige artikel fremsatte Scott Aaronson og Andris Ambainis den formodning, at ethvert begrænset polynomium af lav grad har en variabel med stor indflydelse. De beviste, at enhver kvantealgoritme med T forespørgsler, hvis formodningen holder, kan simuleres på de fleste input af en klassisk algoritme, der foretager polynomielt mange forespørgsler i T. Konsekvensen er en polynomiel snarere end eksponentiel vækst i antallet af klassiske forespørgsler for enhver fast tilnærmelsesfejl og andel af udelukkede input; det udelukker ikke eksponentielle kvantefordele for problemer med passende struktur.

Formelt betragter arkivet et reelt polynomium p af grad højst d, hvis værdier på den diskrete kube ligger mellem 0 og 1. Hvis dets varians over et uniformt tilfældigt input er mindst ε, har en koordinat en indflydelse på mindst (8√15 / (125π⁴)) · ε^(5/2) / d⁶ og dermed mindst (ε/d)⁷. Indflydelse er den forventede kvadrerede ændring i p, når bitværdien for den pågældende koordinat vendes.

Sådan blev beviset udarbejdet og kontrolleret

Argumentet følger en plan udarbejdet af Shachar Lovett og Jiapeng Zhang, som bygger på fraktionelle certifikater og niveaumængder, men erstatter en ulighed, som planen lod stå som en formodning, med en ny ulighed for alle par. En determinant skaber en en-til-en-parring af inputindstillinger. PSI oplyser, at denne parring går videre end David Reimers svagere parring i Butterfly Lemma, fordi den også begrænser, hvor ofte parrede indstillinger er enige om hver koordinat – en grænse, der er nødvendig for den nye ulighed.

Arkivet opdeler det elementære bevis i fire dele: at udlede uligheden for alle par fra determinanten og bijektionen, at integrere den over niveaumængder, at beregne gennemsnittet over koordinater og at fastslå en rækkegrænse med en punktvis følsomhedsgrænse. Tilsammen giver disse trin den eksplicitte grænse for indflydelse.

Ifølge arkivets dokumenterede kontrol indeholder den formelle udvikling ingen pladsholdere for beviser eller tilføjede aksiomer. Dens erklæringer blev genafspillet gennem Leans kerne og lean4lean, en uafhængig implementering af Leans typekontrol. I en sandkassekørsel accepterede en sammenligner, der brugte nanoda- og Lean-kernerne, de fire endelige sætninger; på en anden maskine accepterede den én korrekt, lille løsning og afviste fire bevidst forkerte løsninger.

Disse kontroller har udtrykkelige begrænsninger. En læser skal stadig bekræfte, at den formelle formulering svarer til den trykte formodning. Den tekst, der er skrevet til mennesker, er ikke i sig selv maskinkontrolleret, mens Leans kerne og compiler, Mathlibs definitioner og de maskiner, der bruges til kontrollen, fortsat indgår i det betroede grundlag.

Menneskelige roller og ekspertvurdering

David Turturean, medlem af PSIs tekniske medarbejderstab, udviklede og kørte forskningssystemet, afgrænsede problemet, bad modellen samle et første udkast, gennemgik dette udkast og er ansvarlig for artiklens korrekthed. Arkivet oplyser, at AI-modeller udarbejdede de matematiske udsagn, det første udkast og Lean-formaliseringen. Jim Halverson gennemgik beviset, og Phiala Shanahan kommenterede formaliseringen.

Meddelelsen følger efter en artikel indsendt den 19. august 2026 af Guy Blanc, Jordan Docter, Carmen Strassle og Li-Yang Tan. Disse forfattere havde fastslået konsekvensen for klassisk simulering af parallelle kvantealgoritmer og bevist, at en algoritme med t forespørgsler og d runder kan simuleres på de fleste input med t^(O(d²)) klassiske forespørgsler. PSI oplyser, at alle fire har læst hele beviset, har bidraget med kommentarer og er ved at udarbejde en kortere fremstilling til eksperter.

I deres vurdering, der blev offentliggjort af PSI, skrev forskerne: »Dette er et enormt resultat. Det løser en årtier gammel formodning med vigtige konsekvenser for karakteren af de problemer, der kan løses hurtigere ved hjælp af kvantecomputere. Beviset bygger på og videreudvikler flere forskningsområder inden for analyse af booleske funktioner og probabilistisk kombinatorik. Det hele bliver samlet på nærmest magisk vis.«

Den umiddelbare prøve er usædvanligt konkret: Uafhængige kerner kan genafspille det kodede argument, mens eksperter stadig skal bekræfte, at det kodede udsagn stemmer overens med Aaronson og Ambainis’ formodning, og vurdere de dele af artiklen, der ligger uden for Lean. Denne arbejdsdeling afgør, hvad maskinkontrollerne fastslår, og hvad der stadig kræver menneskelig matematisk gennemgang.