Kernpunkte
- Anthropic und der Partner Theorem nutzten Claude, um vorhandenen Softwarecode mathematisch zu verifizieren und formale Beweise für dessen Korrektheit zu generieren.
- Das Modell erzeugte rund 180 Millionen Zeilen Beweiscode für 123 Open-Source-Bibliotheken in nur wenigen Wochen. Dabei entdeckte Claude Hunderte von Fehlern, die konventionelle Tests übersehen hatten.
- Wenn KI Code schreiben und beweisen kann, dass er korrekt ist, könnte die Softwareautomatisierung einen großen Sprung machen. Anthropic möchte, dass formale Verifikation mit KI so selbstverständlich wird wie Standardtests.
Anthropic nutzte Claude, um mathematisch zu beweisen, dass bestehender Code korrekt ist. Der Ansatz greift ein Kernproblem KI-generierter Software an, ist aber in der Praxis mit strengen Grenzen verbunden.
Den Nachweis zu erbringen, dass Software unter allen Umständen fehlerfrei läuft, war stets prohibitiv teuer. Ein Team von Spezialisten benötigte 20 Personenjahre um nur den kleinen Betriebssystemkernel seL4 formal zu verifizieren, sodass die Methode extremen Fällen wie Airbus-Avioniksoftware.
Anthropics Frontier Red Team, in Zusammenarbeit mit dem Partner Theorem, stattdessen Claude die Beweisarbeit übernehmen zu lassen. Das Modell erzeugte in nur wenigen Wochen rund 180 Millionen Zeilen mathematischen Beweiscodes und stützte sich dabei auf Testprogramme aus 123 Open-Source-Bibliotheken in Googles OSS-Fuzz Sicherheitsprojekt.
Statt neuen Code zu schreiben, verifizierte Claude bestehende Software, indem es Crashtests in mathematische Probleme übersetzte, den kompilierten Maschinencode analysierte und umfangreiche Beweise erstellte. Ein unabhängiges Verifikationsprogramm namens Rocq prüft diese Beweise automatisch, und laut Anthropic benötigt der Prozess fast keine menschlichen Prüfer. Die Forscher nennen es eine „vollständig autonome“ Beweiserstellung, obwohl die Werkzeuge und formalen Grundlagen von Menschen bei Theorem.Ad entwickelt wurden.
Claude findet Fehler, die jahrelange Tests übersehen haben
Während der Erzeugung von Beweisen stieß Claude auf Hunderte von Fehlern und durfte diese selbst beheben. Viele wären konventionellen Tests entgangen, weil sie nur unter sehr speziellen Bedingungen auftreten, etwa bei ungewöhnlich großen Eingabedateien oder einer bestimmten Abfolge von Zugriffen, sagen die Forscher.
Bei dem Versuch, einen weit verbreiteten PDF-Reader zu verifizieren, fand das Team beispielsweise in einer Woche genauso viele Sicherheitsfehler, wie für diese Software normalerweise in einem ganzen Jahr gemeldet werden. In einer anderen Anwendung entdeckte Claude einen logischen Fehler, der über ein Jahrzehnt unentdeckt geblieben war. Selbst wenn ein vollständiger Beweis letztendlich scheitert, sagt Anthropic, bringe der Versuch dennoch echte Bugs ans Licht.
Was formale Verifikation kann und was nicht
Anthropic räumt ein, dass "formal verifiziert" nicht "fehlerfrei" bedeutet. Die Beweise gelten nur unter strengen Bedingungen: einer bestimmten Prozessorarchitektur, single-threaded Programmen und Eingaben unter 64 MB. In der Praxis laufen diese Bibliotheken auf unterschiedlicher Hardware und in anderen Konfigurationen.
Die Rechen kosten sind hoch, einzelne Beweise verbrauchen Hunderte Millionen Tokens. Anthropic nennt die Gesamtkosten des Projekts nicht. Aber wenn KI ihren eigenen Code verifizieren kann, können Entwickler KI-generierter Software mehr vertrauen und weniger Zeit mit deren Überprüfung verbringen. Das spart nicht nur Kosten bei der Verifikation, sondern beim gesamten Programmierprozess. Ein kleinerer Testlauf zeigte außerdem, dass Beweise wiederverwendbar sind, und neuere Modelle werden effizienter: Opus 5.5 löst die Hälfte der Beweise mit etwa 40 Prozent weniger Tokens als Opus 5.Werbung
Das Projekt stärkt das Argument für Software-Automatisierung. Wenn KI Code schreiben und dessen Korrektheit unter definierten Bedingungen garantieren kann, verschiebt sich die Frage von "Kann KI programmieren?" zu "Kann KI beweisen, dass der von ihr geschriebene Code sicher ist?" Wenn die Antwort ja lautet, könnten die Folgen weit über die heutigen Programmierwerkzeuge hinausgehen.
Ein Beispiel dafür: Anthropic erwartet, dass formale Verifikation mit KI bald so praktikabel wird wie Standardtests, und Theorems Roadmap zielt bereits auf kritische Infrastruktur wie glibc, OpenSSL und cURL ab.
Quelle: Anthropic