PSI: AI från Anthropic har bevisat kvantkonjektur

Physical Superintelligence (PSI), en fysikfokuserad AI-startup, meddelade på fredagen den 6 november att ett forskningssystem de byggt har bevisat Aaronson-Ambainis-konjekturen, ett problem inom kvantkomplexitet som varit öppet sedan 2008, med hjälp av instanser av en icke-offentlig Anthropic-modell. Företaget uppger att systemet hade ett fullständigt bevis på den tredje dagen av en körning på deras egen infrastruktur, och att Lean-bevisassistenten accepterade det. Resultatet har ännu inte genomgått expertgranskning. För närvarande är det ett påstående från företaget, men artikeln och det maskinkontrollerade beviset är offentliga så att externa experter kan testa det.psi.inc

Vad beviset hävdar

Konjekturen frågar om kvantdatorer kan vara exponentiellt snabbare än vanliga datorer på slumpmässiga indata, vilka nästan aldrig innehåller de dolda mönster som algoritmer som Shors faktoriseringsmetod utnyttjar. Aaronson och Ambainis visade att om deras påstående om begränsade polynom av låg grad stämde, skulle kvanthastighetsökningar på slumpmässiga indata som mest vara polynomiska. PSIs tillkännagivande formulerade resultatet så här: "en kvantdator kan inte spara exponentiellt många uppslag såvida inte strängen har ett sällsynt mönster". Teoremet begränsar hur många gånger en algoritm läser sin indata, inte den totala beräkningstiden, vilket lämnar utrymme för praktiska kvantfördelar.thequantuminsider.com+1

Det första beviset gav en svagare gräns. Efter att PSI låtit systemet arbeta med relaterade öppna problem förbättrades resultatet två gånger, och Lean accepterade den slutgiltiga versionen. Argumentationen följer en plan av Shachar Lovett och Jiapeng Zhang. Den ersätter en olikhet de lämnat som en konjektur med en ny, bevisad genom att para ihop indatainställningar via en determinant.psi.inc

Mänskliga roller och kontroller

PSI-medarbetaren David Turturean byggde och körde systemet, instruerade modellen att skriva utkastet till artikeln och ansvarar för dess korrekthet. Rådgivarna Jim Halverson och Phiala Shanahan granskade beviset och kommenterade formaliseringen. Projektets GitHub-arkiv uppger att beviset, artikeln och formaliseringen producerades av AI-modeller. Det står också att Lean-teoremen inte innehåller några platshållare eller tillagda axiom och att de har kontrollerats på nytt av två oberoende kärnimplementeringar. Läsare behöver fortfarande bekräfta att det formella påståendet matchar den ursprungliga konjekturen.github.com+1

Stanford-forskarna Guy Blanc, Jordan Docter, Carmen Strassle och Li-Yang Tan löste ett specialfall i augusti. De har läst igenom hela beviset och kallade det i ett uttalande publicerat av PSI för "ett enormt resultat" där "allt sammanförs på ett närmast magiskt sätt".psi.inc

Obesvarade frågor

PSI har inte angett vilken Anthropic-modell de använde, och Anthropic har inte svarat på en förfrågan om kommentar. Tillkännagivandet följer på OpenAIs påstående i september om att de löst ett problem rörande Navier-Stokes-ekvationerna, och det bidrar till debatten om vad AI innebär för matematikers karriärer.businessinsider.com