Können LLMs beweisbar korrekten Code schreiben?

Software-Fehler kosten die US-Wirtschaft jährlich über zwei Billionen Dollar¹. Ein Problem, das wir in Europa nicht haben, wir schreiben schließlich alle formal verifizierten Code.

Nein, natürlich nicht. Für die meisten Projekte ist ein Bug ärgerlich, aber kein Desaster. Anders sieht es bei der Software in Insulinpumpen aus, bei Flugzeugsteuerungen, in Kernkraftwerken.

Die Antwort ist ernüchternd: Auch dort setzt kaum jemand auf mathematische Beweise. Die EU-Medizinprodukteverordnung verlangt Verifikation und Validierung für Software, aber sie schreibt nicht vor, wie. Mathematische Beweise sind nirgends Pflicht². Selbst in sicherheitskritischer Software sind formale Methoden die Ausnahme, nicht die Regel³.

Dabei existiert eine Lösung für einen Teil des Problems seit Jahrzehnten: formale Verifikation, also Code, der mathematisch bewiesen korrekt ist — korrekt relativ zu einer formalen Spezifikation. Es gibt echte Beispiele. AWS hat Teile ihrer TLS-Bibliothek formal verifiziert⁴. Der Mikrokernel seL4 läuft in Boeing-Drohnen⁵. Im Hardware-Design ist formale Verifikation Standard, Intel setzt sie seit dem Pentium 4 ein, nachdem der FDIV-Bug 1994 einen Rückruf erzwang⁶. Aber das sind Ausnahmen, exquisite artifacts, wie ein DARPA-Paper sie nennt⁵, handverlesene Komponenten, jede für sich ein Forschungsprojekt.

Die Gründe für die geringe Verbreitung sind ein ganzes Bündel: Formale Spezifikationen zu schreiben ist teuer und ungewohnt. Verifier geben bei Fehlern wenig hilfreiches Feedback. Integration in bestehende Systeme ist aufwändig. Und die wenigen Experten sind rar.

Martin Kleppmann, Professor in Cambridge und Autor von “Designing Data-Intensive Applications”, glaubt, dass sich das ändern wird⁷. Seine These: KI macht formale Verifikation massentauglich. Die Logik dahinter ist einfach. Proof-Checker liefern binäres Feedback, entweder der Beweis ist korrekt oder nicht. Halluziniert das Modell? Weniger schlimm als sonst, der Checker weist den Beweis ab, das Modell versucht es nochmal. Aber nicht egal: Ohne gute Spezifikation oder hilfreiches Feedback kann der Loop trotzdem steckenbleiben.

Ein Paper von JetBrains Research testet genau das⁸.

method Abs(x: int) returns (y: int)
  ensures 0 <= y
  ensures y == x || y == -x
{
  if x < 0 { return -x; }
  else { return x; }
}

public static BigInteger Abs(BigInteger x) {
    if (x.compareTo(BigInteger.ZERO) < 0) {
        return x.negate();
    } else {
        return x;
    }
}

Das Experiment

Im Zentrum steht eine Kernfrage: Wie viel muss ein LLM wissen, um verifizierten Code zu erzeugen?

Reicht eine Textbeschreibung wie “sortiere dieses Array aufsteigend”, und das Modell liefert korrekten Code samt Beweis? Oder braucht es die formale Spezifikation, und das Modell füllt nur die Lücken? Im ersten Fall wäre keine Verifikationssprache nötig. Im zweiten bleibt Dafny oder Nagini Voraussetzung, das LLM spart nur den letzten Schritt.

Sechs Szenarien testen das Spektrum von “füll die Lücken” bis “mach alles”. In Mode 1 und 2 ist die Implementation gegeben und der Beweis fehlt, wobei Mode 1 die Spezifikation mitliefert und Mode 2 nicht. In Mode 3 und 4 ist die Spezifikation gegeben, aber Implementation und Beweis fehlen. In Mode 5 und 6 gibt es nur Methodensignatur und Textbeschreibung, das LLM muss alles liefern.

Die Pipeline funktioniert genau wie Kleppmann es beschreibt: Prompt an LLM, der Verifier prüft, bei Fehlern gibt es Feedback, und das bis zu fünf Iterationen. Danach folgt Validation, wobei das System prüft, ob die generierte Spezifikation die Referenz impliziert. Triviale Postconditions sind nicht erlaubt — also etwa ensures true oder Bedingungen, die keinerlei Verhalten einschränken.

Die Benchmarks umfassen 132 Dafny-Programme, 106 Nagini -Programme in Python und 55 Verus -Programme in Rust, alle manuell aus HumanEval übersetzt — einem 2021 von OpenAI veröffentlichten Standard-Benchmark mit 164 Programmieraufgaben, von String-Manipulation bis zu einfachen Algorithmen. Jede Aufgabe enthält eine Funktionssignatur, einen Docstring und Unit-Tests. Der Benchmark misst, ob generierter Code die Tests besteht, und ist der De-facto-Standard zum Vergleich von Code-Generierungsmodellen.

Das Ergebnis

Getestet wurde mit Claude 3.5 Sonnet, da GPT-4o und Claude 3 Opus deutlich schlechter abschnitten.

Die Tabelle zeigt drei repräsentative Szenarien: Mode 1 (Beweis ergänzen bei gegebener Spezifikation und Implementation), Mode 4 (Implementation und Beweis aus Spezifikation), Mode 6 (alles aus Textbeschreibung). Die übrigen Modes liegen erwartbar dazwischen.

Die Antwort auf die Kernfrage ist eindeutig: Ohne formale Spezifikation funktioniert es nicht. Mit Spezifikation überraschend gut.

Konkret bedeutet das: “Sortiere dieses Array aufsteigend” reicht nicht, die Erfolgsrate liegt bei 29% für Dafny und 15% bei den anderen. Aber wenn der Mensch die Spezifikation liefert, also Methodensignatur plus requires und ensures, erledigt das LLM den Rest. Es schreibt den Code, findet die Loop-Invarianten und fügt die nötigen Assertions ein. Bei Dafny gelingt das in über 80% der Fälle.

Das bedeutet: Die Verifikationssprache bleibt Voraussetzung. Aber Loop-Invarianten, einer der klassisch schwierigsten mechanischen Teile formaler Verifikation⁹, kann das Modell übernehmen — während die schwierigste inhaltliche Arbeit, die Spezifikation, beim Menschen bleibt.

Und das mit Claude 3.5 Sonnet, einem Modell von Mitte 2024. Die getesteten Alternativen wie GPT-4o und Claude 3 Opus gelten mittlerweile als überholt. Das legt nahe, dass neuere Modelle hier weiter zulegen könnten — aber die harte Grenze bleibt die Spezifikation und die Skalierung auf reale Systeme.

Was das bedeutet

Kleppmanns These bestätigt sich, aber nur teilweise. Der Feedback-Loop funktioniert tatsächlich, denn LLMs können formale Beweise generieren, wenn sie genug Kontext bekommen. Mit formaler Spezifikation liegt der Erfolg bei 63-86%, je nach Sprache und Szenario. Das ist bemerkenswert, denn Loop-Invarianten galten bisher als der Teil formaler Verifikation, der menschliche Intuition erfordert⁹. Ein LLM kann das offenbar lernen.

Aber ohne formale Spezifikation bricht die Erfolgsrate auf 15-29% ein. Das Modell kann einen Beweis führen, wenn jemand sagt, was bewiesen werden soll. Es kann nicht zuverlässig ableiten, was bewiesen werden sollte. Die Herausforderung verschwindet also nicht, sie wandert. Weg vom Beweis, hin zur Spezifikation.

Das klingt nach einem kleinen Unterschied, ist aber ein fundamentaler. Korrekter Code für die falsche Anforderung bringt niemandem etwas. Wenn die Spezifikation sagt “sortiere aufsteigend” und der Code das beweisbar tut, aber eigentlich hätte absteigend sortiert werden sollen, hilft der Beweis nicht. Die Arbeit, die beim Menschen bleibt, ist also nicht irgendeine Restarbeit, sondern die eigentliche intellektuelle Leistung: Definieren, was korrekt überhaupt bedeutet.

Trotzdem ist das ein Fortschritt, und zwar ein größerer als es klingt. Dafny lesen ist nicht schwer, die Syntax ist vertraut und die Spezifikationen sind oft selbsterklärend. Dafny so schreiben, dass der Compiler zufrieden ist, war bisher das Problem. Binär heißt: korrekt oder inkorrekt — und genau das macht das Debugging so mühsam. Der Compiler sagt nicht “hier fehlt eine Invariante”, er sagt nur “Beweis fehlgeschlagen”. Die richtige Invariante zu finden erfordert Intuition für mathematische Induktion, und genau das übernimmt jetzt die KI. Ein Entwickler, der Pre- und Postconditions formulieren kann, muss nicht mehr wissen, wie man Loop-Invarianten findet oder Hilfslemmas strukturiert. Die Einstiegshürde sinkt erheblich, auch wenn sie nicht verschwindet.

Für die AI-Labs ist formale Verifikation aus einem weiteren Grund interessant. Sie liefert perfektes Trainingssignal für Reinforcement Learning¹⁰. Ein Unit-Test kann bestehen, obwohl ein Bug existiert, er wurde nur nicht getroffen. Ein formaler Beweis lässt diese Lücke nicht, denn er deckt jeden möglichen Input ab. Wenn ein Modell auf Millionen solcher Rückmeldungen trainiert wird, lernt es nicht nur Beweise zu generieren, sondern auch, was einen gültigen Beweis ausmacht. Die Qualität des Feedbacks bestimmt die Qualität des Lernens, und formale Verifikation liefert eines der saubersten Feedbacksignale: binär, fälschungssicher, ohne Testlücken.

Das Paper zeigt, dass dieser Kreislauf bereits funktioniert, zumindest für algorithmische Probleme auf dem Niveau von HumanEval. Der Sprung zu echten Systemen mit tausenden Zeilen Code und komplexen Abhängigkeiten steht noch aus.