Anthropic: Ook Claude weerlegt een bijna dertig jaar oud vermoeden over rekentijd
Anthropic zegt dat een intern Claude-model zelf een snellere manier vond om een beroemde rekenpuzzel op te lossen. OpenAI meldde kort ervoor hetzelfde, als een van zijn drie AI-doorbraken. Een computer controleerde het bewijs al; nu kijken wiskundigen of het klopt.
Anthropic heeft een wiskundig artikel online gezet waarin een intern onderzoeksmodel van Claude volgens het bedrijf zelfstandig een bekend vermoeden uit de informatica weerlegt: de Exponential Time Hypothesis (ETH). Dat vermoeden, in 1999 opgesteld door Russell Impagliazzo, Ramamohan Paturi en Francis Zane, is in de informatica een van de stille aannames waar veel ander werk op steunt.
Het nieuws kwam kort nadat OpenAI drie grote doorbraken van zijn eigen AI-modellen meldde, in de wiskunde, de informatica en de natuurkunde. Een van die drie is precies dit resultaat: ook volgens OpenAI is de ETH onjuist. Twee AI-bedrijven zeggen dus los van elkaar hetzelfde oude vraagstuk te hebben opgelost.
Waar gaat het om?
Het vermoeden gaat over een puzzel die 3-SAT heet. Je krijgt een lange lijst ja/nee-vragen en een stapel voorwaarden, die elk over hooguit drie van die vragen gaan. De opgave: vind een antwoord op alle vragen waarbij aan alle voorwaarden tegelijk wordt voldaan. Wie alle mogelijkheden afloopt, heeft bij elke extra vraag twee keer zoveel werk. Bij 100 vragen is dat al ondoenlijk.
Slimme rekenmethoden doen het sneller. Bij de beste tot nu toe kwam er per extra vraag ongeveer een derde werk bij, in plaats van een verdubbeling. Maar ook dan groeit het werk bij elke extra vraag met hetzelfde vaste percentage, en dat loopt bij grote puzzels alsnog uit de hand. De ETH zegt dat dat nooit wezenlijk beter kan: er blijft altijd zo'n vast percentage over. Volgens Anthropic laat Claude zien dat het wél kan. Bij de nieuwe methode wordt de extra hoeveelheid werk per vraag steeds kleiner naarmate de puzzel groter wordt, en op den duur kleiner dan elk vast percentage.
Wat Anthropic beweert
Het artikel heet 'A 2^o(n) Time Algorithm for 3-SAT' en staat op naam van 'Claude, Anthropic'. De informaticus Jelani Nelson zette het op 27 oktober namens Anthropic op de wiskundesite Hexagon. Het beschreven rekenrecept lost 3-SAT op en kan ook tellen hoeveel oplossingen er zijn. Volgens het artikel en Anthropic-onderzoeker Levent Alpoge vond het model de kern van de methode op 16 oktober, zonder hulp van mensen. Het gebruikte daarvoor 14 miljoen tokens (stukjes tekst die het model schrijft). Daarna werkten onderzoekers met Claude aan de uitleg.
Het bewijs is ook uitgeschreven in Lean 4, een programma dat een wiskundig bewijs stap voor stap door de computer laat controleren. Anthropic zette die versie op GitHub. Twee los van elkaar gebouwde controleprogramma's keuren het bewijs goed. Eerder dit jaar maakte Claude al een door de computer gecontroleerde versie van het bewijs van de laatste stelling van Fermat.
Anthropic is open over wat nog moet gebeuren. Volgens het artikel is de Lean-versie door AI-modellen geschreven en door andere exemplaren van dezelfde modellen nagekeken. Er is nog geen mens bekend die die versie zelf heeft gecontroleerd. Mensen moeten ook nagaan of de stelling in Lean precies hetzelfde zegt als in het artikel; daarom staan de belangrijkste stellingen in Lean-vorm in een bijlage van het artikel, met wat de computer wel en niet heeft gecontroleerd.
Mooi voor de theorie, niet voor de praktijk
Het resultaat is vooral theoretisch. Volgens het artikel zegt het niets over het oplossen van zulke puzzels in de praktijk. De nieuwe methode wint op zijn vroegst van gewoon alles aflopen bij een aantal vragen van een 1 met 108 nullen. Voor een gewone puzzel, met zo'n vijf voorwaarden per vraag, ligt die grens zelfs bij een 1 met 10.000 nullen. Ter vergelijking: het waarneembare heelal telt naar schatting zo'n 1 met 80 nullen aan atomen. Het resultaat lost ook de beroemde P-versus-NP-vraag niet op.
Toch is het voor de wetenschap groot nieuws, als het klopt. Ook een strengere versie van het vermoeden (SETH) valt dan weg. Volgens een literatuuronderzoek van Claude in het artikel steunen meer dan 800 eerdere wetenschappelijke artikelen op de ETH of een aanname die daaruit volgt. Houdt het bewijs stand, dan moeten onderzoekers voor die artikelen een nieuwe basis zoeken. De onderliggende problemen worden er in de praktijk niet makkelijker door.
Twee keer hetzelfde resultaat
De resultaten van Anthropic en OpenAI lijken sterk op elkaar. Ook het model van OpenAI vond volgens dat bedrijf op 16 oktober een rekenmethode die telt hoeveel oplossingen zo'n puzzel heeft, en ook dat bewijs staat in Lean. Anthropic verwijst in zijn eigen artikel naar het resultaat van OpenAI.
Het verschil zit vooral in de controle. Bij OpenAI bekijkt een groep onder leiding van Impagliazzo en Paturi, twee van de bedenkers van de ETH, en Ryan Williams (MIT) het bewijs. Zij benadrukken dat hun deelname nog geen goedkeuring is. Anthropic zette zijn artikel en het Lean-bewijs openbaar online. Beide claims komen dus van de bedrijven zelf; het oordeel van wiskundigen volgt nog.
Wat betekent dit voor de weg naar de singulariteit?
Kloppen beide claims, dan kwamen twee AI-modellen los van elkaar op dezelfde dag tot een doorbraak in een vraag waar mensen bijna dertig jaar op vastzaten. Dat is een stap van AI als hulpmiddel naar AI die zelf nieuwe wiskunde vindt.
Tegelijk wordt duidelijk waar het nu om draait: controleren. Een AI kan een bewijs in dagen vinden, maar er zijn maar weinig mensen die zo'n bewijs kunnen beoordelen. Dat zie je ook bij OpenAI, dat begin oktober al 372 resultaten over open vragen in wiskunde en informatica online zette, bijna allemaal uit één opdracht aan een AI-model. Ook daar zijn wiskundigen nog volop met de controle bezig. Bewijzen die de computer al heeft gecontroleerd, zoals hier in Lean, maken dat werk een stuk lichter. Zo kan nieuwe kennis van AI straks sneller en betrouwbaarder bij de wetenschap terechtkomen.
