Anthropic lässt 123 Open-Source-Bibliotheken mit Claude formal verifizieren und entdeckt Hunderte Fehler

Anthropic hat gemeinsam mit seinem Partner Theorem das KI-Modell Claude eingesetzt, um mathematisch zu beweisen, dass bestehender Softwarecode korrekt funktioniert. Untersucht wurden 123 Open-Source-Bibliotheken aus Googles Sicherheitsprojekt OSS-Fuzz. Innerhalb weniger Wochen wurden rund 180 Millionen Zeilen Beweiscode generiert. Dabei sollen auch Hunderte Fehler entdeckt worden sein, die herkömmlichen Tests entgangen waren.

Zwischen „Tests bestanden“ und „Korrektheit bewiesen“ liegt ein Unterschied

Wenn es um die Qualitätssicherung von Software geht, denken viele zunächst an Tests: Man gibt vorgegebene Eingaben ein und prüft, ob das erwartete Ergebnis zurückkommt. Tests können allerdings nur die Bereiche überprüfen, die tatsächlich ausprobiert wurden. Wie sich die Software in nicht getesteten Situationen verhält, verraten sie nicht.

Hier kommt die formale Verifikation ins Spiel. Dabei wird das Verhalten eines Programms als mathematisches Problem behandelt und bewiesen, dass es innerhalb festgelegter Bedingungen stets korrekt funktioniert. Das ist in der Theorie ein mächtiges Verfahren, war aber mit enormem Aufwand verbunden. Allein die Verifikation des kleinen Betriebssystem-Kernels seL4 soll ein Expertenteam insgesamt 20 Personenjahre gekostet haben. Kein Wunder also, dass sich der Einsatz bislang auf Extremfälle wie die Steuerungssoftware von Passagierflugzeugen beschränkte.

Anthropics Frontier Red Team hat sich nun mit Theorem zusammengetan und Claude mit dieser Beweisarbeit betraut. Das Modell sollte keinen neuen Code schreiben. Stattdessen ließ man es bestehende Software untersuchen, Tests zur Erkennung von Abstürzen in mathematische Probleme übersetzen, den Code bis hin zum Maschinencode nach der Kompilierung analysieren und in großem Umfang Beweise erstellen.

Ein separates Programm bewertet die Beweise

Wenn eine KI selbst verfasste Beweise eigenständig für „bestanden“ erklärt, ist das wenig überzeugend. Interessant ist hier deshalb das Bewertungsverfahren: Ein unabhängiges Verifikationsprogramm namens Rocq prüft die generierten Beweise automatisch. Laut Anthropic sind für diesen Prozess kaum menschliche Prüfer nötig.

Das Forschungsteam bezeichnet dieses Verfahren als „vollständig autonome“ Beweiserstellung. Die dafür verwendeten Werkzeuge und die formale Grundlage wurden allerdings von Menschen bei Theorem entwickelt. Treffender als die Vorstellung, die KI habe alles von Grund auf geschaffen, ist wohl: Auf einem von Menschen vorbereiteten Fundament hat sie in kurzer Zeit eine enorme Zahl von Beweisen erstellt.

Hunderte Fehler während der Beweisführung entdeckt

Während der Beweisführung stieß Claude auf Hunderte Fehler und durfte sie auch selbst beheben. Den Forschern zufolge traten viele davon nur unter sehr speziellen Bedingungen auf, etwa bei extrem großen Eingabedateien oder einer bestimmten Reihenfolge von Speicherzugriffen. Es ist daher nicht überraschend, dass sie herkömmlichen Tests entgehen konnten.

Es gibt auch konkrete Beispiele: Bei der Verifikation eines weit verbreiteten PDF-Readers wurden innerhalb einer Woche genauso viele Sicherheitsfehler entdeckt, wie für diese Software normalerweise in einem Jahr gemeldet werden. In einer anderen Anwendung wurde zudem ein Logikfehler gefunden, der mehr als zehn Jahre lang unentdeckt geblieben war.

Nicht übersehen sollte man auch, wie mit Fällen umgegangen wird, in denen ein Beweis nicht vollständig gelingt. Anthropic zufolge können sich während eines gescheiterten Beweisversuchs dennoch echte Fehler zeigen. Beweise dienen also nicht nur dazu, ein „Gütesiegel“ auszustellen, sondern können auch wie eine Sonde Fehler aufspüren. Statt herkömmliche Tests zu ersetzen, scheinen sie diese eher zu ergänzen.

Den Aussageumfang von „formal verifiziert“ richtig einordnen

Dennoch wäre es gefährlich, „formal verifiziert“ mit „fehlerfrei“ gleichzusetzen. Auch Anthropic räumt ein, dass die Beweise nur unter engen Voraussetzungen gelten. Angenommen werden eine bestimmte Prozessorkonfiguration, ein Programm mit nur einem Thread und Eingaben von weniger als 64 MB. In der Praxis laufen Bibliotheken jedoch auf unterschiedlichster Hardware und mit verschiedenen Einstellungen.

Auch die Kosten sind beträchtlich. Für einzelne Beweise können laut Angaben Hunderte Millionen Tokens benötigt werden. Die Gesamtkosten des Projekts wurden nicht veröffentlicht. Kleinere Folgeexperimente zeigten jedoch, dass sich Beweise wiederverwenden lassen. Außerdem zeichnet sich ab, dass neuere Modelle effizienter werden: Opus 5.5 soll etwa 40 Prozent weniger Tokens benötigen als Opus 5, um die Hälfte der Beweise zu lösen.

Die Frage lautet nicht mehr: „Kann die KI programmieren?“

Wenn eine KI Code schreiben und dessen Korrektheit unter bestimmten Bedingungen garantieren kann, verändert sich die Fragestellung. Es geht dann nicht mehr darum, ob eine KI programmieren kann, sondern darum, ob sie die Sicherheit des von ihr geschriebenen Codes beweisen kann. Für Entwicklerteams, die der Zuverlässigkeit von KI-generiertem Code skeptisch gegenüberstehen, ist dieser Perspektivwechsel bedeutsam. Kann die KI ihren Code selbst überprüfen, könnte das die Belastung durch menschliche Code-Reviews verringern und nicht nur die Verifikation, sondern den gesamten Entwicklungsprozess kostengünstiger machen.

Anthropic geht davon aus, dass die formale Verifikation durch KI in naher Zukunft ebenso selbstverständlich sein wird wie herkömmliche Tests. Die Roadmap von Theorem umfasst auch Software für kritische Infrastrukturen wie glibc, OpenSSL und cURL.

Worauf es hier ankommt, ist wohl nicht so sehr der Blick für den „Inhalt“ eines Beweises, sondern für seine „Voraussetzungen“. Unter welchen Bedingungen und mit welchen Eingaben wurde der Beweis geführt? In einer Zeit, in der wir auch die Prüfung der KI überlassen, dürfte die menschliche Fähigkeit, diese Voraussetzungen zu überprüfen, die letzte Bastion der Sicherheit sein.