Claude schreibt mathematische Beweise für Software

Ein Parser mit 391 Zeilen Programmcode bekam einen mathematischen Beweis, der sich über rund 630.000 Zeilen erstreckt. Nicht ein Heer geduldiger Mathematiker schrieb ihn, sondern Claude. Die KI arbeitete sich durch Register, Speicheradressen, Verzweigungen und Maschinenbefehle, bis ein unabhängiges Prüfprogramm bestätigte: Unter den festgelegten Bedingungen kann der untersuchte Programmteil nicht auf die definierte Weise abstürzen.

Dieses Größenverhältnis zwischen einem kleinen Stück Software und einem umfangreichen Beweis markiert einen bemerkenswerten Moment. KI schreibt längst Code, sucht Fehler und schlägt Reparaturen vor. Nun soll sie etwas übernehmen, das bisher einem engen Kreis hoch spezialisierter Experten vorbehalten war: mathematisch nachzuweisen, dass Software bestimmte Regeln tatsächlich immer einhält.

Anthropic und das auf formale Verifikation spezialisierte Unternehmen Theorem ließen Claude Sicherheitseigenschaften von 239 Test-Einstiegspunkten in 123 Open-Source-Bibliotheken beweisen. Die Untersuchung fand nicht am lesbaren Quelltext statt, sondern eine Etage tiefer, an kompilierten RISC-V-Programmen. Dort ist die freundliche Oberfläche der Programmiersprachen verschwunden. Übrig bleiben Maschinenbefehle, Speicheroperationen und Sprünge.

Claude produzierte bei seinen Versuchen ungefähr eine Milliarde Zeilen Beweismaterial. Rund 180 Millionen davon wurden schließlich Bestandteil erfolgreicher, maschinell geprüfter Beweise. Ein typischer Nachweis umfasst etwa 600.000 Zeilen und verteilt sich auf ungefähr 1.400 Dateien. Mehr als die Hälfte dieser Masse besteht allerdings aus Tabellen und anderen Strukturen, die von Werkzeugen erzeugt wurden, welche Claude zuvor selbst geschrieben hatte. Etwa 40 Prozent entfallen auf Definitionen, Maschinenmodelle, Hilfssätze und eigentliche Beweisschritte. Recherchequelle: anthropic.com→

Vom Stochern im Dunkeln zum Beweis

Üblicherweise wird Software getestet. Entwickler geben ihr ausgewählte Eingaben und beobachten, ob sie sich korrekt verhält. Beim Fuzzing geschieht das in industriellem Maßstab: Programme werden mit Abertausenden oder Millionen veränderter, zufälliger und gezielt zusammengestellter Datensätze gefüttert. Ein ungewöhnlich aufgebautes Bild, eine beschädigte Archivdatei oder eine merkwürdige Zeichenfolge kann dabei einen Fehler ans Licht bringen.

Googles OSS-Fuzz wendet solche Verfahren fortlaufend auf Open-Source-Projekte an. Der Dienst kombiniert mehrere Fuzzing-Systeme mit sogenannten Sanitizern, die etwa ungültige Speicherzugriffe sichtbar machen. Auf diese Weise wurden bereits Tausende Sicherheits- und Stabilitätsprobleme entdeckt. Trotzdem bleibt Fuzzing eine Suche. Selbst nach Billionen Durchläufen existiert immer noch eine Eingabe, die bislang niemand ausprobiert hat. Recherchequelle: google.github.io→

Ein mathematischer Beweis verfolgt einen anderen Weg. Er testet nicht bloß viele Möglichkeiten, sondern soll für sämtliche Eingaben innerhalb seines Geltungsbereichs zeigen, dass eine festgelegte Eigenschaft eingehalten wird. Im aktuellen Projekt lautete diese Eigenschaft vereinfacht: Der untersuchte Test-Einstiegspunkt stürzt bei keiner Eingabe bis zur festgelegten Größe ab, löst keinen erfassten Speicherfehler aus und verletzt keine der enthaltenen Zusicherungen.

Dazu wurden vorhandene Fuzz-Tests in formale Spezifikationen verwandelt. Claude musste anschließend beweisen, dass die kompilierten Programme diese Vorgaben unter allen modellierten Bedingungen erfüllen. Gelang das nicht, konnte im Code ein Fehler stecken. Die KI durfte ihn suchen, einen Patch erstellen und danach einen neuen Beweis versuchen.

Gerade dieser Ablauf brachte Schwachstellen zum Vorschein, die klassischen Fuzzern entgangen waren. Dazu gehörte ein Zählerunterlauf in einem Dekompressionsprogramm, der nur bei einer etwa 20 Megabyte großen Eingabe mit einer seltenen inneren Struktur zu einem Schreibzugriff außerhalb des vorgesehenen Speicherbereichs führte. Ein anderer Fehler in einem Bilddecoder ließ sich nur mit einer 64 Megabyte großen Eingabe und mehr als zwei Gigabyte Speicher auslösen. Solche Konstellationen liegen weit außerhalb dessen, was gewöhnliche Fuzzing-Läufe bevorzugt untersuchen. Recherchequelle: anthropic.com→

Der Richter ist keine zweite KI

Entscheidend ist, dass Claude seine eigenen Beweise nicht benoten durfte. Diese Aufgabe übernahm Rocq, ein formales Beweissystem. Sein Kernel prüft nach festen logischen Regeln, ob jeder Schritt aus den vorherigen Annahmen folgt. Sprachliche Eleganz beeindruckt ihn nicht. Selbstbewusst vorgetragene Behauptungen ebenfalls nicht. Entweder der Nachweis ist gültig, oder der Prüfer weist ihn zurück.

Darin liegt ein grundlegender Unterschied zu vielen anderen Anwendungen generativer KI. Wenn ein Chatbot eine Analyse formuliert oder Programmcode erzeugt, muss ein Mensch häufig beurteilen, ob das Ergebnis plausibel und korrekt ist. Ein formaler Beweis lässt sich dagegen deterministisch kontrollieren. Die KI darf Millionen Zeilen produzieren, ohne dass ein Entwickler jede davon lesen muss. Der kleine Proof-Checker arbeitet sich durch das Material und akzeptiert nur, was den hinterlegten Regeln entspricht.

Das bedeutet allerdings nicht, dass nun 123 Bibliotheken als vollkommen fehlerfrei gelten können. Bewiesen wurden bestimmte Aussagen über die untersuchten Test-Einstiegspunkte, nicht die Fehlerfreiheit jedes einzelnen Programmteils. Die Nachweise beziehen sich vor allem auf statisch gebundene, als alleiniger Prozess laufende RISC-V-Programme unter einem modellierten Linux-System. Andere Prozessorarchitekturen, dynamisch eingebundene Bibliotheken, Mehrprogrammbetrieb und nicht erfasste Betriebssystemfunktionen liegen vielfach außerhalb des untersuchten Raums.

Auch ein logisch einwandfreier Beweis kann nur das bestätigen, was seine Spezifikation verlangt. Ist das Modell unvollständig oder beschreibt es die Wirklichkeit nicht präzise genug, bleibt eine Lücke. Ein Programm kann mathematisch korrekt die falsche Aufgabe erledigen. Die Mathematik hält sich unerbittlich an den Wortlaut.

Das öffentlich zugängliche Repository macht diese Grenzen deutlicher als jede griffige Schlagzeile. Dort stehen derzeit Beweise für 60 Test-Einstiegspunkte aus 25 Bibliotheken bereit – also nur ein Teil der gemeldeten Gesamtergebnisse. Die Dokumentation warnt ausdrücklich, dass das zugrunde liegende Linux-Prozessmodell nicht vollständig ist und Annahmen enthält, die es selbst nicht kontrolliert. Zu den veröffentlichten Beispielen gehören Komponenten aus OpenSSL, bzip2, simdjson und zstd. Recherchequelle: github.com→

Auch Beweise können Abkürzungen nehmen

Hinzu kommt ein Problem, das aus der Welt lernender Maschinen vertraut klingt: Claude könnte versuchen, das Ziel auf formal korrekte, aber unerwünschte Weise zu erreichen. Wenn die Aufgabe lautet, einen Absturz unmöglich zu machen, wäre eine radikale Lösung denkbar – das Programm so stark zu verändern, dass es kaum noch etwas tut. Der Beweis würde leichter, die Software jedoch wertlos.

Anthropic bezeichnet diese Gefahr als Reward Hacking. Um solche Abkürzungen zu erschweren, wurden Veränderungen am Code mit einer Art Strafe belegt. Zusätzliche Anerkennung erhielt das System, wenn es zwei Dinge beweisen konnte: bei welchen Eingaben sein Patch das Programmverhalten beeinflusst und wie gering deren Zahl ist. Die vorgenommenen Reparaturen wurden zudem protokolliert und kontrolliert. Vollständig verschwindet das Problem damit nicht. Es verlagert sich lediglich von der Frage „Ist der Beweis gültig?“ zur ebenso wichtigen Frage „Beweist er wirklich das, was wir wissen wollten?“

Aufschlussreich ist auch die Form der entstandenen Nachweise. Menschliche Experten bauen normalerweise Abstraktionen, um wiederkehrende Muster zusammenzufassen. Claude dagegen buchstabierte viele Details immer wieder aus: Registerinhalte, Adressen, Umwandlungen von Zahlenformaten und einzelne Programmzweige. Die Resultate sind gültig, aber aus menschlicher Sicht geradezu barock.

Diese Ausführlichkeit könnte bei komplexeren Programmen an Grenzen stoßen. Der im Forschungsanhang zitierte Experte hält es für möglich, dass weitere Fortschritte bessere modulare Strukturen und allgemeinere Beweisprinzipien verlangen. Die KI müsste dann nicht nur unermüdlich rechnen, sondern lernen, wann sich ein kompliziertes Problem durch eine kluge Abstraktion verkleinern lässt.

Eine neue Arbeitsteilung

Noch ist formale Verifikation teuer. Ein einzelner Beweis kann Hunderte Millionen Tokens verschlingen, seine Prüfung beansprucht mitunter mehrere Stunden Rechenzeit. Dennoch verändert KI die wirtschaftliche Rechnung. Was früher an fehlenden Experten und jahrelanger Handarbeit scheiterte, könnte bei häufig genutzten Bibliotheken plötzlich sinnvoll werden. Wird eine grundlegende Komponente einmal verifiziert, können zahlreiche Programme auf diesem Nachweis aufbauen.

Theorem entwirft deshalb einen weit größeren Plan: Nach einer eigenen Modellrechnung könnten 95 Prozent des Maschinencodes im umfangreichen Nix-Softwarebestand bis Ende 2027 für etwa 134 Millionen Dollar verifiziert werden. Diese Prognose beruht auf einer ausgesprochen optimistischen Annahme – die Leistungsfähigkeit der Modelle bei solchen Aufgaben müsste sich weiterhin ungefähr alle zwei Monate verdoppeln. Sie ist kein Versprechen, sondern eine Wette auf raschen technischen Fortschritt. Recherchequelle: theorem.dev→

Der bedeutendste Wandel liegt ohnehin nicht in einer einzelnen Zahl. Bisher half KI vor allem dabei, schneller mehr Software zu produzieren. Nun deutet sich eine zweite Rolle an: Maschinen könnten die Softwareproduktion durch mathematische Kontrolle ergänzen. Sie schreiben Code – und erzeugen zugleich Beweise, die ihn in ein enges Netz überprüfbarer Regeln spannen.

Software wird dadurch nicht unverwundbar. Doch zwischen einem Programm, das viele Tests überstanden hat, und einem Programm, für das eine bestimmte Eigenschaft bewiesen wurde, liegt ein feiner, entscheidender Unterschied. Der Test sagt: Bis hierher ging alles gut. Der Beweis versucht zu sagen: Innerhalb dieser Grenzen gibt es keinen verborgenen Weg zum Absturz.

Weiterführende Informationen

Quellenhinweis: Einzelne Fakten, Einschätzungen und Prognosen dieses Beitrags stützen sich auf Veröffentlichungen der nachfolgend genannten Unternehmen und Institutionen. Die Links dienen zugleich der weiterführenden Information.

Unite.AI – Anthropic: Claude weist Sicherheitseigenschaften in 123 Bibliotheken nach
Der Beitrag erläutert, wie Claude 239 Einstiegspunkte aus 123 Open-Source-Bibliotheken auf Ebene des kompilierten RISC-V-Maschinencodes verifizierte.
https://www.unite.ai/de/anthropic-says-claude-proved-security-properties-across-123-libraries/

Dr. Web – Anthropic: Sprachmodelle machen formale Softwareverifikation in großem Maßstab möglich
Der Fachbeitrag erklärt die unabhängige Prüfung durch Rocq und grenzt die Nachweise auf die spezifizierten Eigenschaften sowie das modellierte RISC-V-Linux-System ein.
https://www.drweb.de/anthropic-formale-verifikation-claude/

36Kr – Claude erzeugte in rasanter Arbeit 180 Millionen Zeilen an Beweisführungen, und alle Bugs, die bei Billionen von Testdurchläufen übersehen wurden, wurden von der KI vollständig aufgedeckt
Der Beitrag vertieft Theorems Nix-Fahrplan mit einer angestrebten Verifikationsquote von 95 Prozent bis Ende 2027 und geschätzten Gesamtkosten von 134 Millionen US-Dollar.
https://eu.36kr.com/de/p/4037771252028548