Wat Claude Echt Deed
Anthropic maakte op 4 september bekend dat Claude het eerste volledige, computergecontroleerde bewijs van Fermats laatste stelling leverde, werkend met de bewijsassistent Lean 4 gedurende 11 dagen met slechts globale begeleiding van een menselijke onderzoeker. Het systeem genereerde 13 miljoen regels Lean-code en bewees meer dan 30.000 ondersteunende stellingen, waarvan er 29.500 in het uiteindelijke, geverifieerde bewijs terechtkwamen, met een intern onderzoeksmodel dat via tientallen parallel draaiende agenten op het platform Prove2Me ongeveer zes miljard output-tokens verbruikte.
De onderliggende wiskunde is niet nieuw. Andrew Wiles bewees Fermats laatste stelling in 1995, en Claude formaliseerde een latere vereenvoudiging van dat bewijs door Darmon, Diamond en Taylor, waarmee een argument van 129 pagina's, dat de wiskundige gemeenschap maanden kostte om met de hand te controleren, werd omgezet in een vorm die een computer regel voor regel kan verifiëren. Wiskundige Kevin Buzzard, die het resultaat beoordeelde, vertelde Anthropic dat dit een grote stap is richting automatische formalisering van de moderne wiskundige literatuur, bereikt in veel minder tijd dan hij had verwacht.
Waarom Dit een Kostenverhaal Is, Geen Wiskundeverhaal
Het getal dat hier telt, is niet 13 miljoen regels, het zijn 11 dagen. Formele verificatie, het bewijzen dat een stuk wiskunde of software correct is in plaats van het te testen en te hopen, is met de hand altijd traag en duur geweest, en het formaliseren van een resultaat van deze omvang kostte gespecialiseerde teams voorheen jaren werk. Precies die kosten verklaren waarom zo weinig veiligheidskritische software wereldwijd een formeel correctheidsbewijs draagt, en een geautomatiseerd systeem dat vergelijkbaar werk in minder dan twee weken kan doen, verandert de rekensom voor elk Europees ingenieursbedrijf dat systemen certificeert volgens normen als ISO 26262 voor auto's of DO-178C voor vliegtuigen, waar formele methoden al worden gebruikt maar gerantsoeneerd vanwege hun prijs.
Anthropics eigen verslag is open over het foutpercentage achter dat opvallende getal: ongeveer 7 procent van de niet-standaardcode kwam uit mislukte pogingen, verworpen onderweg naar het uiteindelijke bewijs. Dat is een normaal onderdeel van hoe formele verificatie altijd al vorderde, machine of mens, maar het verdient duidelijke vermelding, omdat een succes van 13 miljoen regels de tegenovergestelde indruk wekt.
De Grens Die Niemand Mag Overslaan
Claude formaliseerde een bestaand bewijs, het ontdekte geen nieuw bewijs, en dat verschil telt zwaarder dan de prestatie zelf zodra iemand er technisch gewicht op probeert te leggen. Fermats laatste stelling werkte als demonstratie juist omdat wiskundigen het al drie decennia eens waren over hoe het correcte bewijs eruitzag, wat betekende dat Claudes taak was om een bekend argument te vertalen naar een taal die een machine kan controleren, niet om te beslissen of het argument klopte.
Een veiligheidsdossier voor een remsysteem of een cryptografisch protocol begint met een moeilijkere vraag: wat betekent correct hier eigenlijk, en heeft iemand dat precies genoeg gespecificeerd zodat een formele methode het kan controleren. Geautomatiseerde formalisering kan de tweede helft van dat probleem nu drastisch verkleinen. Voor de eerste helft verandert er niets, en elke organisatie die dit resultaat leest als vrijbrief om specificatiewerk over te slaan in plaats van verificatiewerk, heeft het verkeerd begrepen.
Lees hierna: 87 jaar sneuvelde door een antwoord dat iedereen kan narekenen | Anthropic zet uw logs in uw eigen cloud
