Anthropic-model bewijst quantumvermoeden uit 2008

Het Amerikaanse AI-bedrijf Physical Superintelligence (PSI) meldt dat zijn onderzoekssysteem het Aaronson-Ambainis-vermoeden heeft bewezen, een open vraag uit de quantuminformatica die sinds 2008 onbeantwoord bleef. Het systeem draaide op een niet-openbaar model van Anthropic. PSI maakt dat vrijdag 6 november bekend via de eigen onderzoekspagina.

Waar gaat het vermoeden over

Scott Aaronson en Andris Ambainis formuleerden het vermoeden in 2008. Het gaat om de vraag wanneer een quantumcomputer exponentieel sneller kan zijn dan een gewone computer. Klopt het vermoeden, dan zijn quantumcomputers op willekeurige ja-of-nee-vragen hooguit polynomiaal sneller, tenzij de invoer een zeldzaam patroon bevat. Aaronson en Ambainis brachten het probleem terug tot een uitspraak over polynomen, zo schrijft OfficeChai. PSI stelt dat het nieuwe bewijs laat zien dat elke begrensde polynoom met voldoende variantie altijd minstens één invoerbit heeft met merkbare invloed. Eerdere ondergrenzen werden exponentieel zwakker naarmate de graad van de polynoom steeg.

Drie dagen rekenen, gecontroleerd in Lean

Volgens PSI had het systeem op de derde dag van de run een volledig bewijs. Dat bewijs is daarna geformaliseerd in Lean, een bewijsassistent die elke stap door de computer laat controleren. Lean accepteerde het. Vervolgens werkte het systeem door aan verwante problemen en verbeterde het de uitkomst nog twee keer. Ook die eindversie kwam door de Lean-controle.

Inhoudelijk bouwt het werk voort op eerder onderzoek van Shachar Lovett en Jiapeng Zhang en op het zogeheten Butterfly Lemma van David Reimer. Lovett en Zhang lieten één ongelijkheid als vermoeden open liggen. Dat gat dicht PSI nu met een nieuw bewezen ongelijkheid.

Welk Anthropic-model precies is gebruikt, zegt PSI niet. FourWeekMBA merkt op dat bronnen het alleen een niet-openbaar model van Anthropic noemen. Dat sluit aan bij wat METR deze week schreef over hoe snel Anthropic zijn eigen modellen verbetert.

Mensen blijven verantwoordelijk

Het project stond onder leiding van PSI-medewerker David Turturean. Hij bouwde het systeem, koos het probleem, liet het model een eerste versie van het artikel schrijven en las die na. Volgens PSI is hij verantwoordelijk voor de juistheid. Adviseur Jim Halverson controleerde het bewijs, adviseur Phiala Shanahan gaf commentaar op de Lean-formalisering.

Er is ook een externe reactie. Guy Blanc, Jordan Docter, Carmen Strassle en Li-Yang Tan van Stanford bewezen in augustus al een speciaal geval van het vermoeden. Zij hebben het volledige bewijs gelezen en schrijven nu een kortere uitleg voor vakgenoten. “This is a huge result”, schrijven ze in een reactie die PSI publiceert. Een oordeel van Aaronson of Ambainis zelf vond FourWeekMBA nog niet en het werk is niet door een vaktijdschrift beoordeeld.

Wat betekent dit

AI-systemen leveren steeds vaker bijdragen aan echte wiskunde. Eerder hielpen AI-tools Microsoft-onderzoekers bij het bewijs van het KLS-vermoeden, liet Axiom AI-agents een enorm wiskundebewijs in Lean controleren en claimde OpenAI bewijzen voor onder meer Kakeya en Yang-Mills. Het patroon is telkens hetzelfde: het model zoekt, een formele checker als Lean controleert en mensen nemen de eindverantwoordelijkheid.

Voor quantumcomputing is de uitkomst vooral theoretisch. Ze maakt scherper waar quantumvoordeel op ongestructureerde problemen ophoudt, ook voor bedrijven die werken aan toepassingen zoals zuinigere quantumcircuits. Of de vakgemeenschap het bewijs omarmt, moet de komende maanden blijken. De Lean-controle maakt de kans op een verborgen fout wel klein.