Anthropic hat sein KI-Modell Claude mathematisch beweisen lassen, dass bestehender Code sicher ist. Das Verfahren löst ein Grundproblem KI-generierter Software, hat in der Praxis aber noch enge Grenzen.
Software zu testen ist aufwendig, aber machbar. Zu beweisen, dass sie unter allen Umständen fehlerfrei läuft, war bisher praktisch unbezahlbar. Für die formale Verifikation des kleinen Betriebssystemkerns seL4 brauchte ein Spezialistenteam laut Anthropic 20 Personenjahre. In der Praxis kam das Verfahren deshalb nur in Extremfällen zum Einsatz, etwa bei Airbus-Avioniksoftware.
Nun hat Anthropics Frontier Red Team zusammen mit dem Partner Theorem einen anderen Weg getestet: Claude übernahm die Beweisarbeit. Das Modell erzeugte laut Anthropic in wenigen Wochen rund 180 Millionen Zeilen mathematischen Beweiscode für Testprogramme aus 123 Open-Source-Bibliotheken, die in Googles Sicherheitsprojekt OSS-Fuzz laufen.
Code absichern statt nur Code schreiben
In der Debatte um KI und Programmierung steht meist die Frage im Vordergrund, ob Modelle brauchbaren Code schreiben können. Anthropic verschiebt hier den Fokus: Claude überprüfte bestehenden Code mathematisch. Das ist eine Aufgabe, die bisher so spezialisiert und zeitaufwendig war, dass sie für die allermeisten Projekte schlicht nicht infrage kam.
Der Ablauf: Vorhandene Tests, die Software auf Abstürze prüfen, werden in eine mathematische Aufgabe übersetzt. Claude arbeitet sich dann durch Hunderttausende Zeilen Maschinencode und liefert einen Beweis, den ein unabhängiges Prüfprogramm namens Rocq maschinell kontrolliert. Menschliche Prüfer braucht es dafür laut Anthropic kaum.
Die Forscher sprechen von "vollständig autonomer" Beweiserzeugung. Die Werkzeuge und formalen Grundlagen dafür haben allerdings Menschen bei Theorem gebaut.
Claude findet Fehler, die jahrelanges Testen übersehen hat
Beim Versuch, die Beweise zu erstellen, stieß Claude laut Anthropic auf Hunderte Fehler in der untersuchten Software und durfte sie selbst beheben. Viele davon wären mit herkömmlichen Testmethoden kaum aufgefallen, weil sie nur unter sehr speziellen Bedingungen auftreten: etwa bei ungewöhnlich großen Eingabedateien oder bei einer bestimmten Abfolge von Zugriffen.
Bei einem verbreiteten PDF-Reader fanden die Forscher nach eigenen Angaben in einer Woche so viele Sicherheitsfehler wie sonst in einem ganzen Jahr. In einer anderen Anwendung entdeckte Claude einen Logikfehler, der seit mehr als zehn Jahren unentdeckt geblieben war.
Laut Anthropic zeigt das: Schon der Versuch, einen mathematischen Beweis zu führen, liefert verwertbare Ergebnisse, selbst wenn der vollständige Beweis am Ende nicht gelingt.
Automatisierung des Codings schreitet voran
Anthropic räumt offen ein, dass "formal verifiziert" nicht "fehlerfrei" bedeutet. Die Beweise gelten nur unter engen Voraussetzungen: für eine bestimmte Prozessorarchitektur, für einzelthreadige Programme und für Eingaben unter 64 MB. In der Praxis laufen die Bibliotheken meist auf anderer Hardware und in anderen Konfigurationen.
Auch der Aufwand ist erheblich. Einzelne Beweise können laut Anthropic Hunderte Millionen Tokens kosten. Die Gesamtkosten des Projekts nennt das Unternehmen nicht. An einem kleineren Testlauf zeigte sich immerhin, dass neuere Modelle deutlich weniger Rechenaufwand benötigen und Beweise wiederverwendbar sind.
Das Projekt markiert dennoch einen Richtungswechsel: Wenn KI nicht nur Code schreiben, sondern dessen Korrektheit unter definierten Bedingungen garantieren kann, verschiebt sich die Automatisierungsfrage grundlegend. Statt "Kann die KI programmieren?" lautet sie dann: "Kann die KI beweisen, dass der von ihr geschriebene Code sicher ist?" Sollte die Antwort darauf "Ja" lauten, hätte das weitreichendere Folgen für die Softwareentwicklung als die derzeit verfügbare Coding-Software und könnte die Automatisierung deutlich vorantreiben.
Anthropic erwartet, dass formale Verifikation mit KI bald so praktikabel wird wie heutige Standardtests. Theorems Roadmap zielt bereits auf die Verifikation kritischer Infrastruktur wie glibc, OpenSSL und cURL.
KI-News ohne Hype – von Menschen kuratiert
Mit dem THE‑DECODER‑Abo liest du werbefrei und wirst Teil unserer Community: Diskutiere im Kommentarsystem, erhalte unseren wöchentlichen KI‑Newsletter, 6× im Jahr den "KI Radar"‑Frontier‑Newsletter mit den neuesten Entwicklungen aus der Spitze der KI‑Forschung, bis zu 25 % Rabatt auf KI Pro‑Events und Zugriff auf das komplette Archiv der letzten zehn Jahre.
