PSI raportoi Aaronsonin–Ambainisin konjektuurin koneellisesti tarkistetusta todistuksesta

Physical Superintelligence ilmoitti 6. marraskuuta 2026, että sisäinen tutkimusjärjestelmä, joka käytti ei-julkisen Anthropic-mallin ilmentymiä, oli löytänyt todistuksen Aaronsonin–Ambainisin konjektuurille. Kyseessä on kvanttilaskennan ongelma, joka oli ollut avoinna vuodesta 2008.

Järjestelmä tuotti täydellisen todistuksen PSI:n omalla infrastruktuurilla tehdyn ajon kolmantena päivänä, ja Lean-todistusavustaja hyväksyi sen. PSI antoi järjestelmälle tämän jälkeen ratkaistavaksi siihen liittyviä avoimia ongelmia. Järjestelmä paransi tulosta kahdesti, ennen kuin Lean hyväksyi lopullisen version. Käsikirjoitus ja Lean 4 -formalisaatio ovat julkisia.

Mitä konjektuuri kertoo kvanttilaskennan nopeuseduista

Kysymys koskee sitä, milloin kvanttitietokoneet voivat olla eksponentiaalisesti nopeampia kuin klassiset tietokoneet. Shorin vuoden 1994 tekijöihinjakoalgoritmi perustuu rakenteeseen: sen syöte sisältää toistuvan kuvion, jota algoritmi voi hyödyntää. PSI:n tulos käsittelee vastakkaista tapausta eli satunnaisia tai rakenteettomia syötteitä, joista tällainen kuvio yleensä puuttuu.

Kyselymallissa klassinen algoritmi lukee yhden bitin kyselyä kohden, kun taas kvanttikysely voidaan jakaa superpositiona useille syötteen paikoille. PSI:n selityksessä tämä malli yhdistyy polynomeihin: T:n kvanttikyselyn jälkeen todennäköisyys, jolla algoritmi vastaa kyllä, on syötebittien polynomi, jonka arvot ovat rajoitettuja ja jonka aste on enintään 2T. Kvanttialgoritmin simulointi tarkoittaa siis sen arvioimista, kuinka suuri kyseinen polynomi on, lukematta eksponentiaalista määrää syötebittejä.

Alkuperäisessä artikkelissaan Scott Aaronson ja Andris Ambainis esittivät konjektuurin, jonka mukaan jokaisessa rajoitetussa matala-asteisessa polynomissa on muuttuja, jolla on suuri vaikutus. He osoittivat, että jos konjektuuri pitää paikkansa, jokainen T-kyselyn kvanttialgoritmi voidaan simuloida useimmilla syötteillä klassisella algoritmilla, joka tekee T:n suhteen polynomisen määrän kyselyitä. Tästä seuraa, että klassisten kyselyiden määrä kasvaa polynomisesti eikä eksponentiaalisesti, kun approksimaatiovirhe ja pois jätettävien syötteiden osuus pidetään vakioina. Tulos ei kuitenkaan sulje pois eksponentiaalisia kvanttietuja ongelmissa, joissa on sopiva rakenne.

Muodollisesti tietovarastossa tarkastellaan reaalikertoimista polynomia p, jonka aste on enintään d ja jonka arvot diskreetissä kuutiossa ovat välillä 0–1. Jos sen varianssi tasaisesti satunnaisen syötteen suhteen on vähintään ε, jonkin koordinaatin vaikutus on vähintään (8√15 / (125π⁴)) · ε^(5/2) / d⁶ ja siten vähintään (ε/d)⁷. Vaikutus tarkoittaa odotusarvoista neliömuutosta polynomin p arvossa, kun kyseisen koordinaatin bitti käännetään.

Miten todistus rakennettiin ja tarkistettiin

Todistus noudattaa Shachar Lovettin ja Jiapeng Zhangin suunnitelmaa, joka perustuu fraktionaalisiin todistajiin ja tasojoukkoihin, mutta korvaa uuden kaikkien parien epäyhtälön avulla epäyhtälön, jonka suunnitelma jätti konjektuurin varaan. Determinantti tuottaa syötteen asetusten välille bijektion. PSI:n mukaan tämä paritus menee David Reimerin heikompaa Butterfly Lemma -paritusta pidemmälle, sillä se rajoittaa myös sitä, kuinka usein paritetut asetukset saavat saman arvon kullakin koordinaatilla. Tätä rajaa tarvitaan uuteen epäyhtälöön.

Tietovarastossa alkeellinen todistus on jaettu neljään osaan: kaikkien parien epäyhtälön johtamiseen determinantista ja bijektiosta, epäyhtälön integroimiseen tasojoukkojen yli, koordinaattien suhteen keskiarvoistamiseen sekä rivirajan osoittamiseen pisteittäisen herkkyysrajan avulla. Yhdessä nämä vaiheet tuottavat eksplisiittisen vaikutusrajan.

Tietovaraston kirjatun tarkastuksen mukaan formaalissa kehitelmässä ei ole todistusaukkoja eikä lisättyjä aksioomia. Määritykset tarkistettiin uudelleen Lean-ytimen ja Lean-tyyppitarkistimen riippumattoman toteutuksen lean4leanin avulla. Eristetyssä suorituksessa nanoda- ja Lean-ytimiä käyttävä vertailija hyväksyi neljä lopullista lausetta. Toisella koneella se hyväksyi yhden oikean, pienen ratkaisun ja hylkäsi neljä tarkoituksella väärää ratkaisua.

Näillä tarkistuksilla on selkeät rajansa. Lukijan on edelleen varmistettava, että formaali väite vastaa julkaistua konjektuuria. Ihmisen luettavissa olevaa artikkelia ei ole itsessään tarkistettu koneellisesti, ja Lean-ydin ja -kääntäjä, Mathlibin määritelmät sekä tarkistuksessa käytetyt koneet kuuluvat edelleen luotettuun perustaan.

Ihmisten roolit ja asiantuntija-arvio

PSI:n tekniseen henkilöstöön kuuluva David Turturean kehitti ja ajoi tutkimusjärjestelmän, rajasi ongelman, kehotti mallia kokoamaan ensimmäisen luonnoksen, tarkisti luonnoksen ja vastaa artikkelin oikeellisuudesta. Tietovarastossa kerrotaan, että tekoälymallit tuottivat matemaattiset väitteet, ensimmäisen luonnoksen ja Lean-formalisaation. Jim Halverson auditoi todistuksen, ja Phiala Shanahan kommentoi formalisaatiota.

Julkistusta edelsi Guy Blancin, Jordan Docterin, Carmen Strasslen ja Li-Yang Tanin 19. elokuuta 2026 jättämä artikkeli. Nämä kirjoittajat olivat ratkaisseet klassista simulointia koskevan seurauksen rinnakkaisille kvanttialgoritmeille ja osoittaneet, että t-kyselyn ja d-kierroksen algoritmi voidaan simuloida useimmilla syötteillä t^(O(d²)) klassisella kyselyllä. PSI kertoo, että kaikki neljä ovat lukeneet koko todistuksen, esittäneet siitä kommentteja ja valmistelevat asiantuntijoille lyhyempää esitystä.

PSI:n julkaisemassa arviossaan tutkijat kirjoittivat: ”Tämä on valtava tulos. Se ratkaisee vuosikymmeniä vanhan konjektuurin, jolla on merkittäviä vaikutuksia siihen, millaiset ongelmat mahdollistavat kvanttinopeutuksen. Todistus hyödyntää ja kehittää edelleen useita Boolean-funktioiden analyysin ja todennäköisyyskombinatoriikan tutkimussuuntia. Kaikki nivoutuu yhteen jokseenkin taianomaisella tavalla.”

Välitön testi on poikkeuksellisen konkreettinen: riippumattomat todistusytimet voivat toistaa koodatun argumentin, mutta asiantuntijoiden on silti vahvistettava, että koodattu väite vastaa Aaronsonin ja Ambainisin konjektuuria, sekä arvioitava paperin Lean-järjestelmän ulkopuoliset osat. Tämä työnjako määrittää, mitä koneen tekemät tarkistukset osoittavat ja mikä edellyttää edelleen ihmisen tekemää matemaattista arviointia.