PSI: Anthropicin tekoäly todisti Aaronson-Ambainis-konjektuurin

Fysiikkaan keskittyvä tekoäly-startup Physical Superintelligence (PSI) ilmoitti perjantaina 6. marraskuuta, että sen kehittämä tutkimusjärjestelmä on todistanut Aaronson-Ambainis-konjektuurin, joka on ollut avoin kvanttikompleksisuuden ongelma vuodesta 2008 lähtien. Todistuksessa käytettiin julkaisemattomia Anthropic-malleja. Yrityksen mukaan järjestelmä tuotti täydellisen todistuksen kolmantena ajopäivänä omassa infrastruktuurissaan, ja Lean-todistusavustaja hyväksyi sen. Tulos ei ole vielä läpäissyt tieteellistä vertaisarviointia. Toistaiseksi kyseessä on yrityksen väite, mutta artikkeli ja koneellisesti tarkistettu todistus ovat julkisia, joten ulkopuoliset asiantuntijat voivat testata niitä.psi.inc

Mitä todistus väittää

Konjektuuri kysyy, voivatko kvanttitietokoneet olla eksponentiaalisesti nopeampia kuin tavalliset tietokoneet satunnaisilla syötteillä, jotka eivät lähes koskaan sisällä piilotettuja kuvioita, joita esimerkiksi Shorin tekijöihinjakoalgoritmi hyödyntää. Aaronson ja Ambainis osoittivat, että jos heidän väitteensä rajoitetuista matalan asteen polynomeista pitää paikkansa, kvanttinopeutukset satunnaisilla syötteillä olisivat enintään polynomi-tasoa. PSI:n tiedote muotoili tuloksen näin: "kvanttitietokone ei voi säästää eksponentiaalisen määrän hakuja, ellei merkkijonossa ole harvinaista kuviota". Teoreema rajoittaa sitä, kuinka monta kertaa algoritmi lukee syötteensä, ei kokonaislaskenta-aikaa, mikä jättää tilaa käytännön kvanttihyödyille.thequantuminsider.com+1

Ensimmäinen todistus antoi heikomman rajan. Kun PSI asetti järjestelmän ratkomaan siihen liittyviä avoimia ongelmia, se paransi tulosta kahdesti, ja Lean hyväksyi lopullisen version. Argumentti noudattaa Shachar Lovettin ja Jiapeng Zhangin suunnitelmaa. Se korvaa heidän konjektuuriksi jättämänsä epäyhtälön uudella, joka todistettiin yhdistämällä syöteasetukset determinantin avulla.psi.inc

Ihmisten roolit ja tarkistukset

PSI:n työntekijä David Turturean rakensi ja ajoi järjestelmän, ohjeisti mallia luonnostelemaan artikkelin ja vastaa sen oikeellisuudesta. Neuvonantajat Jim Halverson ja Phiala Shanahan auditoivat todistuksen ja kommentoivat formalisointia. Projektin GitHub-arkiston mukaan todistus, artikkeli ja formalisointi on tuotettu tekoälymalleilla. Siinä todetaan myös, että Lean-teoreemat eivät sisällä paikkamerkkejä tai lisättyjä aksioomia, ja ne on tarkistettu kahdella riippumattomalla ytimen toteutuksella. Lukijoiden on silti vahvistettava, että muodollinen väite vastaa alkuperäistä konjektuuria.github.com+1

Stanfordin tutkijat Guy Blanc, Jordan Docter, Carmen Strassle ja Li-Yang Tan ratkaisivat erikoistapauksen elokuussa. He ovat lukeneet koko todistuksen ja kutsuneet sitä PSI:n julkaisemassa lausunnossa "valtavaksi tulokseksi", jossa "kaikki yhdistyy melko maagisella tavalla".psi.inc

Vastaamattomat kysymykset

PSI ei ole kertonut, mitä Anthropic-mallia se käytti, eikä Anthropic vastannut kommenttipyyntöön. Ilmoitus seuraa OpenAI:n syyskuista väitettä, jonka mukaan se olisi ratkaissut Navier-Stokesin yhtälöihin liittyvän ongelman, ja se lisää keskustelua siitä, mitä tekoäly tarkoittaa matemaatikkojen urakehitykselle.businessinsider.com