OpenAI's volgende model, Astra, loste zojuist tien decennialange open wiskundeproblemen op

Op 1 augustus publiceerde OpenAI een rapport waarin het beweerde dat zijn volgende model, intern Astra genoemd (nog niet beschikbaar), nieuwe resultaten had opgeleverd voor tien verschillende open problemen in de wiskunde. (Nee, het zijn niet de Millennium Prize-problemen, maar ze zijn desalniettemin aanzienlijk.)

Wat opmerkelijk is: deze oplossingen zijn geen incrementele vooruitgang op de problemen; het zijn echte beslissingen, geverifieerd met Lean. (Lean is een programmeertaal en bewijsassistent die afdwingt dat elke stap van een wiskundig argument in machinaal leesbaar detail wordt uitgeschreven.) 

Het is veel om in één keer te verwerken. In dit artikel heb ik de problemen per deelgebied geordend en op hoog niveau beschreven wat er is gebeurd, wat dit kan betekenen voor de wiskunde als vakgebied, en wat we verder over Astra kunnen afleiden.

Wat zijn de tien problemen?

Hier is elk resultaat, in gewone taal, samen met het specifieke deelgebied van de wiskunde of informatica waar het toe behoort.

Niet-sofische groepen

Deelgebied: Groepentheorie

Astra produceerde een expliciete constructie van een groep die, hoe nauwkeurig ook, niet kan worden benaderd door grote eindige structuren — waarmee een vraag wordt gesloten die openstaat sinds het concept van een "sofische" groep in 1999 werd geïntroduceerd. De constructie gaat vergezeld van een bewijs dat geen enkele reeks eindige benaderingen ooit kan werken, geformaliseerd in Lean zodat de logica mechanisch kan worden gecontroleerd.

Wikipedia is al bijgewerkt:

Bolstapeling

Deelgebied: Hoogdimensionale geometrie

De vraag is hoe dicht identieke, niet-overlappende bollen samen kunnen worden gestapeld naarmate het aantal dimensies toeneemt. Astra bewees een strakker plafond voor die dichtheid in hoge dimensies, de eerste verbetering van deze specifieke bovengrens sinds 1978. Het levert geen betere stapelmethode op — het verkleint de marge voor hoe goed een toekomstige methode in principe kan zijn.

Binaire en sferische codes

Deelgebied: Coderingstheorie

Foutcorrigerende codes werken door geldige berichten ver genoeg uit elkaar te houden zodat kleine fouten het ene niet in het andere kunnen veranderen. Astra bewees aanzienlijk strakkere (exponentieel verbeterde) grenzen aan hoeveel van zulke berichten kunnen bestaan voor een gegeven minimumafstand, met een overeenkomend resultaat voor punten verspreid over een hoogdimensionale bol.

Connes’ rigiditeitsvermoeden

Deelgebied: Operatoralgebra’s

Alain Connes vermoedde dat bepaalde groepen altijd uniek konden worden gereconstrueerd uit een algebraïsche structuur, een von Neumann-algebra, die uit hen is opgebouwd. Astra weerlegde dit door twee werkelijk verschillende groepen te produceren die tot dezelfde algebra leiden, waarmee wordt aangetoond dat de reconstructie niet altijd één-op-één is.

Rekenkundige circuitcomplexiteit

Deelgebied: Computationele complexiteitstheorie

De "permanent", één getal berekend uit een rooster van getallen, is kostbaar om uit te rekenen, en complexiteitstheoretici willen het minimum aantal rekenstappen kennen dat elke methode in principe nodig zou kunnen hebben. Astra bewees een nieuwe, sterkere ondergrens voor dat minimum — een berucht lastig type resultaat om überhaupt te verbeteren.

Kwantum parallelle herhaling

Deelgebied: Kwantumcomplexiteitstheorie

De klassieke theorie zegt dat het laten herhalen van een moeilijk spel door twee niet-communicerende spelers, vele keren parallel, de kans op valsspelen exponentieel kleiner maakt. Astra bewees dat dezelfde garantie ook geldt wanneer de spelers kwantumverstrengeling delen, waarmee een fundamenteel klassiek principe naar de kwantumsetting wordt uitgebreid.

Closest vector problem

Deelgebied: Roostergebaseerde cryptografie

Gegeven een herhalend rooster van punten (een lattice) en een doelpositie, vraagt dit probleem om het dichtstbijzijnde roosterpunt — een probleem dat in hoge dimensies als zeer moeilijk wordt beschouwd, en daarom sommige kwantumbestendige versleuteling ondersteunt. Astra bewees dat zelfs het benaderen van het antwoord, binnen een specifieke polynomiale factor, aantoonbaar moeilijk blijft, wat de cryptografie die hierop voortbouwt verder versterkt.

Ehrharts volumevermoeden

Deelgebied: Discrete en convexe geometrie

Voor een convexe vorm waarvan het enige inwendige roosterpunt precies op zijn massamiddelpunt ligt, wilden wiskundigen de maximaal mogelijke inhoud kennen die zo’n vorm in een willekeurige dimensie kan hebben. Astra bepaalde dat maximale volume voor elke dimensie en rondde daarmee het vermoeden in volle algemeenheid af.

Multikleur Ramsey-getallen

Deelgebied: Ramsey-theorie / combinatoriek

Met genoeg mensen en genoeg categorieën van relaties tussen hen, vind je uiteindelijk gegarandeerd drie mensen die allemaal door dezelfde categorie verbonden zijn. Astra bewees dat de minimale groepsgrootte die nodig is sneller groeit dan elk vast exponentieel tempo naarmate het aantal categorieën toeneemt, en loste daarmee Erdős-probleem 183 op.

Extremale getalvermoedens

Deelgebied: Extremale grafentheorie

Deze tak van de wiskunde vraagt hoeveel verbindingen een netwerk kan hebben terwijl bepaalde kleine, verboden patronen toch uitblijven. Astra besliste twee verwante vermoedens hier, overeenkomend met Erdős-problemen 146 en 180, en bepaalde hoe dicht zulke netwerken kunnen worden voordat die patronen onvermijdelijk opduiken.

Elk van deze problemen stond al minstens tien jaar open; verschillende al dertig jaar of langer, waaronder problemen waar Turing Award-win­naars aan werkten aan de theoretische CS-kant van de lijst.

Wacht, is een tegenvoorbeeld het "makkelijke" soort bewijs?

Wie ben ik om hier iets negatiefs over te zeggen, maar ik weet dat dit een veelgestelde vraag of reactie is, vooral van mensen die iets van wiskunde weten.

Het meest gehoorde commentaar als kritiek: meerdere van deze resultaten zijn tegenvoorbeelden in plaats van nieuwe algemene theorie. Dit idee is belangrijk omdat een tegenvoorbeeld een ja/nee-vraag beantwoordt, maar op zichzelf niet vertelt waarom het patroon breekt of je een familie van vergelijkbare objecten aanreikt om als volgende te bestuderen, terwijl iets anders, zoals een classificatiestelling of een nieuwe techniek, meer deuren opent.

Ik zou zeggen dat deze kritiek in het algemeen standhoudt, maar ze geldt niet als alomvattende afwijzing van deze hele reeks problemen. Ten eerste is het resultaat over niet-sofische groepen geen kleine aanpassing van een bestaande near-miss — het is de eerste constructie in zijn soort na 27 jaar waarin niemand er ook maar één had, en de techniek erachter zal naar verwachting generaliseren om er meer te vinden.

Ten tweede zijn meerdere van de andere negen resultaten, waaronder de bovengrens voor bolstapeling en de hardheidsresultaten voor CVP, helemaal geen tegenvoorbeelden; het zijn directe verbeteringen op bestaande grenzen. 

Wat nog niet is opgelost

Een paar dingen zijn het volgen waard nu dit de komende dagen, weken en maanden door het veld wordt uitgeplozen:

• Nog geen peerreview. Deze resultaten zijn met Lean geverifieerd en informeel beoordeeld door wiskundigen die preprints hebben gezien, maar geen ervan is door een gerefereerd tijdschriftproces gegaan. 
• Auteurschap wordt nog besproken. OpenAI zegt verantwoordelijkheid te nemen voor de manuscripten en Lean-formalisaties, terwijl het de wiskundige redeneringen zelf toeschrijft aan het model. Onafhankelijke replicatie van het proces (in tegenstelling tot de verificatie van de bewijzen) is op dit moment lastig te doen.

Wat dit betekent voor de wiskunde

De meest directe verschuiving zit in waar wiskundigen hun tijd daadwerkelijk aan zouden kunnen besteden. Als je een goed afgebakend open probleem aan een model kunt voorleggen en in Lean kunt controleren, verschuift de flessenhals van "kan iemand dit oplossen" naar "hebben we de juiste vraag gesteld en correct geformaliseerd". Het vermogen om een goede vraag te stellen en te weten welke de moeite waard is om aan te pakken, is een echte vaardigheid die wiskundigen door ervaring ontwikkelen. 

Er borrelt ook een kwestie van financiering en geloofwaardigheid. Onderzoeksbeurzen, tenure-dossiers en prijzen zijn historisch gebouwd op schaarste: deze problemen waren zo moeilijk dat het oplossen ervan iets zei over de oplosser. Als door AI ondersteunde resultaten routine worden, zal het veld nieuwe manieren nodig hebben om te onderscheiden wat echt moeilijk is versus wat nu binnen bereik ligt van een paar duizend dollar aan inferentiekosten. Natuurlijk begrijpt de gemiddelde persoon deze problemen niet volledig. De mensen met echte scholing wel, en dat verandert niet. Dus wiskundige kennis is waardevoller dan ooit. 

Hoe mensen reageren

Reacties op sociale media waren minder verdeeld over de vraag of de bewijzen kloppen, en meer over waar ze een teken van zijn.

Sommigen zien het tempo zelf als het echte verhaal: tien decennia-oude problemen die tegelijk landen, over niet-verwante velden heen, sneller dan experts ze überhaupt kunnen beoordelen. Een vraag voor de toekomst: "Zullen we dit allemaal kunnen blijven controleren?"

Anderen werpen tegen dat dit minder over AI in het algemeen zegt dan het lijkt. Wiskunde is een zeldzaam domein waar het werk van een model automatisch en volledig kan worden gecontroleerd. De meeste echte problemen bieden dat soort ingebouwde, automatische antwoordsleutel niet. Vanuit dat perspectief is de prestatie echt, maar zegt ze misschien meer over dat wiskunde uitzonderlijk geschikt is voor AI.

Een derde lijn van commentaar: een correct bewijs dat niemand volledig heeft gecontroleerd of doorgrond, is nog niet echt begrepen, slechts geverifieerd. Een stelling ontdekken en begrijpen wat deze betekent, zijn in deze visie twee verschillende taken.

Tot slot

Wiskundigen zeggen dat het resultaat over niet-sofische groepen op het echte werk lijkt: een authentiek, decennia-oud open vraagstuk in de groepentheorie, gesloten door een expliciete constructie die wiskundigen in het vakgebied serieus nemen. De andere negen resultaten vormen samen een brede en technisch substantiële reeks vooruitgang binnen de zuivere wiskunde.

Wat nog niet is gebeurd, is het tragere deel: peerreview, replicatie van het zoekproces, en het veld dat daadwerkelijk op deze resultaten voortbouwt. Dat deel duurt langer dan een blogpost, en het is het deel dat ons echt zal vertellen hoe groot dit was. We houden je op de hoogte.