Anthropic lässt Claude Open-Source-Code formal verifizieren
Mit Partner Theorem erzeugte Claude rund 180 Millionen Zeilen Beweiscode für 123 Bibliotheken und fand dabei Hunderte Fehler.
Worum es geht
Anthropics Frontier Red Team hat zusammen mit dem Partner Theorem getestet, ob Claude bestehenden Code formal beweisen kann. Statt nur Code zu schreiben, übersetzte das Modell vorhandene Tests in mathematische Aufgaben und erstellte Beweise, die das Prüfprogramm Rocq maschinell kontrolliert.
Die wichtigsten Fakten
- Rund 180 Millionen Zeilen Beweiscode in wenigen Wochen.
- Grundlage: Testprogramme aus 123 Open-Source-Bibliotheken aus Googles OSS-Fuzz.
- Claude fand Hunderte Fehler und durfte sie selbst beheben.
- Bei einem PDF-Reader gab es in einer Woche so viele Sicherheitsfehler wie sonst in einem Jahr; ein Logikfehler war über zehn Jahre unentdeckt.
- Zum Vergleich: Die Verifikation des seL4-Kernels kostete rund 20 Personenjahre.
- Einschränkungen: nur eine Prozessorarchitektur, einzelthreadige Programme, Eingaben unter 64 MB.
- Einzelne Beweise können Hunderte Millionen Tokens kosten; Gesamtkosten nennt Anthropic nicht.
Einordnung
Das Projekt zeigt, dass KI formale Verifikation praktikabler machen könnte, die bisher nur in Extremfällen wie der Avionik eingesetzt wurde. Auch ein gescheiterter Beweisversuch liefert nützliche Fehlerfunde. "Formal verifiziert" heißt aber nicht fehlerfrei, und die hohen Kosten sowie engen Annahmen begrenzen den Nutzen derzeit.
