PSI hevder AI drevet av Anthropic har bevist kvantekonjekture

Physical Superintelligence (PSI), en fysikkfokusert AI-oppstart, kunngjorde fredag 6. november at et forskningssystem de har utviklet, har bevist Aaronson-Ambainis-konjekturen, et uløst problem innen kvantekompleksitet siden 2008, ved hjelp av en ikke-offentlig Anthropic-modell. Selskapet opplyser at systemet hadde et fullstendig bevis på tredje dag av en kjøring på deres egen infrastruktur, og at Lean-bevisassistenten godtok det. Resultatet har ennå ikke gjennomgått fagfellevurdering. Foreløpig er dette en påstand fra selskapet, men artikkelen og det maskinkontrollerte beviset er offentlig tilgjengelig slik at eksterne eksperter kan teste det.psi.inc

Hva beviset hevder

Konjekturen spør om kvantedatamaskiner kan være eksponentielt raskere enn vanlige datamaskiner på tilfeldige inndata, som nesten aldri inneholder de skjulte mønstrene som algoritmer som Shors faktoriseringsmetode utnytter. Aaronson og Ambainis viste at dersom deres påstand om begrensede polynomer av lav grad holdt stikk, ville kvantehastighetsøkninger på tilfeldige inndata maksimalt være polynomiske. PSIs kunngjøring formulerte resultatet slik: "en kvantedatamaskin kan ikke spare eksponentielt mange oppslag med mindre strengen har et sjeldent mønster". Teoremet begrenser hvor mange ganger en algoritme leser inndataene sine, ikke den totale beregningstiden, noe som gir rom for praktiske kvantefordeler.thequantuminsider.com+1

Det første beviset ga en svakere grense. Etter at PSI satte systemet til å jobbe med relaterte åpne problemer, forbedret det resultatet to ganger, og Lean godtok den endelige versjonen. Argumentasjonen følger en plan lagt av Shachar Lovett og Jiapeng Zhang. Den erstatter en ulikhet de hadde etterlatt som en konjektur med en ny, bevist ved å pare inndatainnstillinger gjennom en determinant.psi.inc

Menneskelige roller og kontroller

PSI-medarbeider David Turturean bygde og kjørte systemet, instruerte modellen til å utforme artikkelen, og er ansvarlig for korrektheten. Rådgiverne Jim Halverson og Phiala Shanahan reviderte beviset og kommenterte formaliseringen. Prosjektets GitHub-depot opplyser at beviset, artikkelen og formaliseringen ble produsert av AI-modeller. Det står også at Lean-teoremene ikke inneholder plassholdere eller ekstra aksiomer, og at de ble kontrollert på nytt av to uavhengige kjerneimplementeringer. Lesere må fremdeles bekrefte at den formelle påstanden samsvarer med den opprinnelige konjekturen.github.com+1

Stanford-forskerne Guy Blanc, Jordan Docter, Carmen Strassle og Li-Yang Tan løste et spesialtilfelle i august. De har lest gjennom hele beviset og kalte det i en uttalelse publisert av PSI for "et enormt resultat" der "alt er brakt sammen på en nærmest magisk måte".psi.inc

Ubesvarte spørsmål

PSI har ikke opplyst hvilken Anthropic-modell de brukte, og Anthropic har ikke svart på en forespørsel om kommentar. Kunngjøringen kommer i kjølvannet av OpenAIs påstand i september om at de hadde løst et problem knyttet til Navier-Stokes-ligningene, og den bidrar til debatten om hva AI betyr for matematikeres karrierer.businessinsider.com