Vad Claude Faktiskt Gjorde

Anthropic meddelade den 4 september att Claude levererade det första fullständiga, datorverifierade beviset för Fermats stora sats genom att arbeta med bevisassistenten Lean 4 i 11 dagar med enbart övergripande vägledning från en mänsklig forskare. Systemet genererade 13 miljoner rader Lean-kod och bevisade över 30 000 stödjande satser, varav 29 500 kom med i det slutliga, verifierade beviset, med hjälp av en intern forskningsmodell som förbrukade ungefär sex miljarder utdatatoken via tiotals agenter som körde parallellt på plattformen Prove2Me.

Den underliggande matematiken är inte ny. Andrew Wiles bevisade Fermats stora sats 1995, och Claude formaliserade en senare förenkling av det beviset av Darmon, Diamond och Taylor, och omvandlade ett argument på 129 sidor, som det tog den matematiska gemenskapen månader att kontrollera för hand, till en form en dator kan verifiera rad för rad. Matematikern Kevin Buzzard, som granskade resultatet, sa till Anthropic att det var ett stort steg mot automatisk formalisering av den moderna matematiska litteraturen, uppnått på betydligt kortare tid än han väntat sig.

Varför Detta Är en Kostnadshistoria, Inte en Matematikhistoria

Talet som spelar roll här är inte 13 miljoner rader, det är 11 dagar. Formell verifiering, det vill säga att bevisa att en bit matematik eller mjukvara är korrekt i stället för att bara testa den och hoppas, har alltid varit långsamt och dyrt att göra för hand, och att formalisera ett resultat av den här storleken har tidigare tagit specialistteam flera års arbete. Just den kostnaden är anledningen till att så lite säkerhetskritisk mjukvara i världen överhuvudtaget bär ett formellt korrekthetsbevis, och ett automatiserat system som klarar jämförbart arbete på under två veckor ändrar räknestycket för alla europeiska ingenjörsföretag som certifierar system enligt standarder som ISO 26262 för bilar eller DO-178C för flygplan, där formella metoder redan används men ransoneras på grund av kostnaden.

Anthropics egen redogörelse är öppenhjärtig om felfrekvensen bakom den slående siffran: cirka 7 procent av den icke-standardiserade koden kom från misslyckade försök som förkastades på vägen till det slutliga beviset. Det är en normal del av hur formell verifiering alltid har utvecklats, maskin eller människa, men det förtjänar att sägas tydligt, eftersom en framgång på 13 miljoner rader ger motsatt intryck.

Gränsen Ingen Bör Hoppa Över

Claude formaliserade ett befintligt bevis, det upptäckte inget nytt, och den skillnaden väger tyngre än själva prestationen så fort någon försöker lägga teknisk tyngd på den. Fermats stora sats fungerade som demonstration just för att matematiker redan i tre decennier varit överens om hur det korrekta beviset skulle se ut, vilket innebar att Claudes uppgift var att översätta ett känt argument till ett språk en maskin kan kontrollera, inte att avgöra om argumentet överhuvudtaget stämde.

Ett säkerhetsfall för ett bromssystem eller ett kryptografiskt protokoll börjar med en svårare fråga: vad betyder korrekt här egentligen, och har någon specificerat det tillräckligt exakt för att en formell metod ska kunna kontrollera det. Automatiserad formalisering kan nu drastiskt krympa den andra halvan av det problemet. Den ändrar ingenting i den första halvan, och varje organisation som läser detta resultat som ett frikort att hoppa över specifikationsarbete i stället för verifieringsarbete har missförstått det.

Läs vidare: 87 år föll för ett svar som vem som helst kan kontrollera  |  Anthropic flyttar dina säkerhetsloggar till ditt eget moln