PSI teigia, kad „Anthropic“ pagrįstas DI įrodė kvantinę hipotezę

Fizikos srities DI startuolis „Physical Superintelligence“ (PSI) lapkričio 6 d., penktadienį, pranešė, kad jų sukurta tyrimų sistema įrodė Aaronson-Ambainis hipotezę – kvantinio sudėtingumo problemą, atvirą nuo 2008 m. – naudodama viešai neprieinamo „Anthropic“ modelio egzempliorius. Bendrovė teigė, kad sistema pateikė išsamų įrodymą trečiąją vykdymo dieną savo infrastruktūroje, o „Lean“ įrodymų asistentas jį priėmė. Rezultatas dar nebuvo recenzuotas moksliniame žurnale. Kol kas tai yra bendrovės teiginys, tačiau straipsnis ir mašininiu būdu patikrintas įrodymas yra vieši, todėl išorės ekspertai gali jį patikrinti.psi.inc

Ką teigia įrodymas

Hipotezėje klausiama, ar kvantiniai kompiuteriai gali būti eksponentiškai greitesni už įprastus atsitiktinėms įvestims, kuriose beveik niekada nėra paslėptų modelių, kuriais naudojasi tokie algoritmai kaip Shoro faktorizavimo metodas. Aaronsonas ir Ambainis parodė, kad jei jų teiginys apie ribotus žemo laipsnio polinomus būtų teisingas, kvantinis pagreitis atsitiktinėms įvestims būtų daugiausiai polinominis. PSI pranešime rezultatas suformuluotas taip: "kvantinis kompiuteris negali sutaupyti eksponentiškai daug peržiūrų, nebent eilutė turi retą modelį". Teorema riboja, kiek kartų algoritmas nuskaito savo įvestį, o ne bendrą skaičiavimo laiką, todėl lieka vietos praktiniams kvantiniams pranašumams.thequantuminsider.com+1

Pirmasis įrodymas pateikė silpnesnę ribą. PSI nukreipus sistemą į susijusias atviras problemas, rezultatas buvo pagerintas du kartus, o „Lean“ priėmė galutinę versiją. Argumentas seka Shacharo Lovetto ir Jiapengo Zhango planu. Jis pakeičia nelygybę, kurią jie paliko kaip hipotezę, nauja, įrodyta suporuojant įvesties nustatymus per determinantą.psi.inc

Žmonių vaidmuo ir patikra

PSI darbuotojas Davidas Turtureanas sukūrė ir paleido sistemą, paragino modelį parengti straipsnį ir yra atsakingas už jo teisingumą. Patarėjai Jimas Halversonas ir Phiala Shanahan atliko įrodymo auditą ir pakomentavo formalizavimą. Projekto „GitHub“ saugykloje teigiama, kad įrodymą, straipsnį ir formalizavimą sukūrė DI modeliai. Taip pat teigiama, kad „Lean“ teoremose nėra vietos žymeklių ar papildomų aksiomų ir jas pakartotinai patikrino dvi nepriklausomos branduolio implementacijos. Skaitytojai vis tiek turi patvirtinti, kad formalus teiginys atitinka pradinę hipotezę.github.com+1

Stanfordo tyrėjai Guy Blancas, Jordanas Docteris, Carmen Strassle ir Li-Yang Tan rugpjūčio mėnesį išsprendė specialų atvejį. Jie skaitė visą įrodymą ir PSI paskelbtame pareiškime pavadino jį "didžiuliu rezultatu", kuriame "viskas sujungta gana stebuklingu būdu".psi.inc

Neatsakyti klausimai

PSI neatskleidė, kurį „Anthropic“ modelį naudojo, o „Anthropic“ neatsakė į prašymą pakomentuoti. Pranešimas pasirodė po „OpenAI“ rugsėjo mėnesio teiginio, kad jie išsprendė problemą, susijusią su Navier-Stokes lygtimis, ir prisideda prie diskusijų apie tai, ką DI reiškia matematikų karjerai.businessinsider.com