FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning

Die Arbeit stellt FM-Agent vor, ein Framework, das mithilfe von Large Language Models und einer Top-Down-Strategie zur automatisierten Generierung von Spezifikationen aus natürlichen Spracheingaben erstmals eine skalierbare, kompositionelle Verifikation großer Softwaresysteme ermöglicht und dabei hunderte bisher unentdeckter kritischer Fehler findet.

Das Wesentliche

Das Problem: Der riesige, von KI geschriebene Code-Monster

Stell dir vor, ein genialer, aber manchmal etwas verwirrter Roboter (eine KI) hat einen riesigen, komplexen Maschinenpark gebaut. Dieser Park ist so groß, dass er über 100.000 Zeilen Code enthält – das ist wie ein ganzer Wolkenkratzer aus Bauplänen.

Das Problem: Der Roboter hat zwar viel gebaut, aber er hat auch Fehler gemacht. Manchmal hat er eine Schraube falsch gedreht oder ein Ventil verkehrt herum installiert. Da der Roboter den Plan selbst geschrieben hat, weiß kein Mensch mehr genau, wie alles hätte funktionieren sollen. Wenn man jetzt versucht, den ganzen Park auf einmal zu überprüfen, wird einem schwindelig; es ist zu groß und zu kompliziert.

Die alte Lösung: Der mühsame Handwerker-Ansatz

Früher haben Menschen versucht, solche Fehler zu finden, indem sie für jede einzelne Maschine (jeden Code-Teil) ein detailliertes technisches Regelbuch (eine „formale Spezifikation") schrieben. Sie mussten genau beschreiben: „Wenn ich diesen Hebel ziehe, muss das Licht aufleuchten."
Das Problem dabei: Das Schreiben dieser Regelbücher dauert ewig und erfordert Expertenwissen. Wenn aber der Roboter den Code geschrieben hat, weiß oft niemand mehr, was der Hebel eigentlich tun sollte. Die Regelbücher waren also oft falsch oder gar nicht vorhanden.

Die neue Lösung: FM-Agent – Der clevere Detektiv mit einem neuen Trick

Das Paper stellt FM-Agent vor. Das ist ein neues System, das KI nutzt, um KI-geschriebene Programme auf Fehler zu prüfen. Es funktioniert wie ein genialer Detektiv, der drei besondere Tricks anwendet:

Trick 1: Die „Top-Down"-Methode (Vom Chef zum Angestellten)

Statt zu fragen: „Was macht dieser kleine Motor?", fragt FM-Agent zuerst: „Was erwartet der Chef von diesem Motor?"

• Die Metapher: Stell dir vor, du willst prüfen, ob ein Koch (der Code) einen Salat macht. Anstatt den Koch zu beobachten (der vielleicht einen verfaulten Salat macht), fragst du den Gast (den Aufrufer), was er bestellt hat.
• Der Vorteil: Der Gast (der Code, der den Motor aufruft) weiß genau, was er erwartet (z. B. „Ich brauche einen frischen Salat"). Selbst wenn der Koch einen Fehler macht und einen Stein auf den Salat legt, weiß der Gast, dass das falsch ist. FM-Agent nutzt also die Erwartungen der „Kunden" (der aufrufenden Funktionen), um zu definieren, was der „Koch" (die Funktion) eigentlich tun sollte. So werden Fehler nicht durch die Fehler des Kochs selbst verschleiert.

Trick 2: Die „Allgemeinsprache"-Brille (Natürliche Sprache statt Mathematik)

Früher mussten alle Regelbücher in einer schwer verständlichen mathematischen Sprache geschrieben sein. FM-Agent ist anders: Er versteht die Sprache, die wir alle sprechen.

• Die Metapher: Früher musste man dem Sicherheitsinspektor eine komplexe mathematische Formel zeigen, um zu beweisen, dass eine Brücke sicher ist. FM-Agent reicht dem Inspektor eine einfache Beschreibung: „Die Brücke darf nicht wackeln, wenn ein Lastwagen drüber fährt."
• Der Trick: Die KI (LLM) ist so schlau, dass sie diese einfache Beschreibung versteht und dann den Code Schritt für Schritt durchgeht. Sie fragt sich: „Wenn ich hier ankomme, ist die Brücke noch stabil?" Wenn die Antwort „Nein" ist, hat sie einen Fehler gefunden.

Trick 3: Der „Fehler-Test-Generator" (Der Beweis)

Wenn der Detektiv einen Fehler vermutet, reicht es nicht, nur zu sagen „Hier stimmt was nicht". Man muss es beweisen.

• Die Metapher: FM-Agent baut nicht nur eine Theorie auf, sondern er baut sofort eine kleine Testmaschine. Er sagt: „Ich baue jetzt genau den Lastwagen, der die Brücke zum Wackeln bringt, und lasse ihn fahren."
• Das Ergebnis: Wenn die Brücke wirklich wackelt (oder das Programm abstürzt), ist der Fehler bewiesen. FM-Agent erstellt automatisch diese Testfälle, um zu zeigen: „Schau mal, hier ist der Fehler!"

Was hat FM-Agent erreicht?

Das Team hat FM-Agent an vier riesigen Systemen getestet, die komplett von anderen KIs geschrieben wurden (ein Compiler, ein Betriebssystem, eine Datenbank und ein KI-Framework).

• Das Ergebnis: Obwohl die Entwickler dieser Systeme bereits viele Tests gemacht hatten, fand FM-Agent 522 neue, schwere Fehler.
• Die Schwere: Manche dieser Fehler hätten dazu geführt, dass ganze Systeme abgestürzt sind oder falsche Ergebnisse geliefert haben (z. B. ein Compiler, der falschen Code produziert, oder ein Datenbank-System, das Zahlen falsch rundet).

Fazit

FM-Agent ist wie ein Super-Prüfer, der nicht müde wird. Er nutzt die KI, um zu verstehen, was ein Programm tun soll, und prüft dann, ob es das auch wirklich tut. Er ist schnell, kann riesige Systeme bewältigen und findet Fehler, die selbst menschliche Entwickler und andere Test-Tools übersehen haben.

Es ist nicht der perfekte Ersatz für alle alten Methoden (die sind manchmal noch genauer), aber es ist der erste Schritt, um die riesigen, von KI gebauten Welten sicher zu machen, bevor sie in die echte Welt gehen.

Technische Zusammenfassung

1. Problemstellung

Die Entwicklung von Software durch Large Language Models (LLMs) hat sich rasant weiterentwickelt und ermöglicht die Generierung großer Systeme (z. B. Compiler mit über 100.000 Zeilen Code). Ein zentrales Problem ist jedoch die Korrektur dieser generierten Codes. Da LLMs Halluzinationen produzieren können, enthalten die generierten Systeme oft Fehler.

Herausforderungen bei der automatisierten Verifikation großer Systeme sind:

• Komplexität: Systemcode weist komplexe Kontrollflüsse, Zustandsmanipulationen und tiefe prozedurale Abhängigkeiten auf.
• Skalierbarkeit bestehender Methoden: Traditionelle formale Methoden (wie Hoare-Logik) erfordern manuell geschriebene, formale Spezifikationen für jede Funktion. Dies ist bei großen Systemen ein enormer manueller Aufwand.
• Spezifikationslücke bei LLM-Code: Da Entwickler oft nicht tief in den von LLMs generierten Code eingeweiht sind, fällt es ihnen schwer, präzise Spezifikationen zu schreiben. Bestehende Ansätze, die Spezifikationen aus der Implementierung ableiten, scheitern, da die Implementierung selbst fehlerhaft sein kann und somit die „erwartete" Absicht des Entwicklers verzerrt.
• Natürliche Sprache vs. Formale Logik: Entwickler drücken ihre Absichten oft in natürlicher Sprache aus, während Verifikatoren nur formale Formeln verarbeiten können.
• Fehlerursachen-Analyse: Wenn eine Verifikation fehlschlägt, können traditionelle Verifikatoren oft nicht die Ursache des Fehlers erklären oder Testfälle generieren, die den Fehler auslösen.

2. Methodik: FM-Agent

FM-Agent ist ein Framework, das die erste automatisierte kompositionelle Verifikation für große Systeme ermöglicht. Es nutzt LLMs, um Hoare-Logik-Prinzipien auf natürliche Sprache zu erweitern. Der Ansatz basiert auf drei Kerninsights:

A. Top-Down-Spezifikationsgenerierung (Insight I)

Statt Spezifikationen aus der (möglicherweise fehlerhaften) Implementierung abzuleiten, nutzt FM-Agent einen Top-Down-Ansatz:

• Konzept der „Erwarteten Spezifikation": Die Spezifikation einer Funktion wird basierend darauf abgeleitet, wie ihre Aufrufer (Callers) sich das Verhalten der Funktion vorstellen.
• Prozess: FM-Agent analysiert den Code der Aufrufer, um die Vorbedingungen (Pre-Conditions) und Nachbedingungen (Post-Conditions) der aufgerufenen Funktion zu inferieren.
• Vorteil: Selbst wenn die Implementierung der Funktion Fehler enthält, spiegelt die so generierte Spezifikation die ursprüngliche Designabsicht wider. Bei mehreren Aufrufern werden die Erwartungen zusammengeführt (Disjunktion der Vorbedingungen, Konjunktion der Nachbedingungen).
• Ordnung: Die Generierung erfolgt in Schichten (Layers) basierend auf dem Aufrufgraphen, wobei unabhängige Funktionen parallel verarbeitet werden können.

B. Hoare-Style-Reasoning mit Natürlicher Sprache (Insight II)

FM-Agent erweitert die Hoare-Logik, um direkt mit natürlichen Sprachspezifikationen zu arbeiten:

• Inferenz: Anstatt formale Formeln zu verwenden, nutzt FM-Agent LLMs, um schrittweise Nachbedingungen für Codeblöcke zu inferieren, ausgehend von den Vorbedingungen.
• Prinzip: Wenn die inferierte Nachbedingung eines Ausführungspfades die in der Spezifikation geforderte Nachbedingung nicht impliziert, wird ein potenzieller Fehler gemeldet.
• Genauigkeit: LLMs können die Ausführungsergebnisse kleiner Codeblöcke sehr genau vorhersagen (getestet mit 98,6 % Genauigkeit auf VerusBench), was eine schrittweise Analyse in natürlicher Sprache ermöglicht.

C. Bug-Validierung durch Testfall-Generierung (Insight III)

Um False Positives zu vermeiden und Fehlerursachen zu klären:

• System-Ebene: FM-Agent generiert Testfälle auf System-Eingabe-Ebene (nicht nur auf Funktionsebene), um die Korrelation zwischen Eingabe und internem Fehlerverhalten zu nutzen.
• Validierung: Der Bug-Validator führt die generierten Testfälle aus. Nur wenn ein Testfall den Fehler tatsächlich reproduziert, wird er als bestätigter Bug gemeldet. Dies hilft Entwicklern, die Root Cause zu verstehen.

3. Architektur und Workflow

Der Workflow von FM-Agent besteht aus drei Hauptkomponenten:

1. Specification Generator: Bestimmt die Reihenfolge der Spezifikationsgenerierung (basierend auf dem Aufrufgraphen und stark zusammenhängenden Komponenten), generiert Spezifikationen für jede Funktion und leitet erwartete Spezifikationen für Aufrufer ab.
2. Code Reasoner: Überprüft die Konsistenz der Implementierung mit der natürlichen Sprachspezifikation mittels Hoare-Style-Inferenzregeln (angepasst für natürliche Sprache).
3. Bug Validator: Generiert Testfälle basierend auf den gefundenen Inkonsistenzen, führt sie aus und bestätigt echte Fehler.

4. Ergebnisse und Evaluation

FM-Agent wurde an vier großen, automatisch generierten Systemen evaluiert (insgesamt 277.000 Zeilen Code, 8.549 Funktionen):

• CCC: Ein C-Compiler (143k LoC), autonom entwickelt von Anthropic.
• VibeTensor: Ein Deep-Learning-Framework (108k LoC) von NVIDIA.
• VibeOS: Ein Betriebssystem-Kernel (15k LoC).
• Bespoke OLAP: Eine SQL-Query-Engine (11k LoC).

Ergebnisse:

• Skalierbarkeit: FM-Agent konnte alle Systeme innerhalb von 2 Tagen analysieren.
• Fehlererkennung: Trotz intensiver Tests durch die Entwickler (Unit Tests, Integrationstests, Differential Checks, Multi-Agent Reviews) entdeckte FM-Agent 522 neue, bisher unentdeckte Fehler.
  • CCC: 339 Fehler (u.a. falsche Codegenerierung, Abstürze, falsche Diagnosen).
  • VibeTensor: 141 Fehler (u.a. Speicherlecks, falsche Tensor-Werte).
  • VibeOS: 23 Fehler (u.a. Speicherkorruption, Endlosschleifen).
  • Bespoke OLAP: 19 Fehler (u.a. falsche Query-Ergebnisse).
• Vergleich: Ein ablativer Test (Spezifikation nur aus Implementierung, ohne Hoare-Reasoning) fand nur 57 Fehler im CCC, was die Überlegenheit des Top-Down-Ansatzes und der formalen Inferenz unterstreicht.

5. Bedeutung und Beiträge

• Erster Ansatz für automatisierte kompositionelle Verifikation: FM-Agent ist das erste Framework, das Hoare-Logik für große, komplexe Systeme automatisiert anwendet, indem es die Hürde manueller Spezifikationen durch LLMs überwindet.
• Paradigmenwechsel: Der Wechsel von „Bottom-Up" (Spezifikation aus Code) zu „Top-Down" (Spezifikation aus Aufrufer-Erwartungen) ist entscheidend, um Fehler in der Implementierung nicht in die Spezifikation zu übernehmen.
• Natürliche Sprache als Schnittstelle: Die Fähigkeit, direkt mit natürlichen Sprachspezifikationen zu verifizieren, macht formale Methoden für Entwickler zugänglich, die keine Experten für formale Logik sind.
• Praktische Relevanz: Das System findet schwerwiegende Fehler (Abstürze, Sicherheitslücken, Logikfehler) in Systemen, die bereits als „getestet" galten.
• Komplementäres Werkzeug: FM-Agent zielt nicht darauf ab, formale Verifikatoren mit Soundness-Garantien zu ersetzen, sondern ergänzt sie, indem es skalierbare, fehlerfindende Reasoning-Methoden für den LLM-Zeitalter bereitstellt.

Zusammenfassend demonstriert FM-Agent, dass die Kombination aus LLMs und kompositionellem Reasoning (Hoare-Logik) ein vielversprechender Weg ist, um die Zuverlässigkeit von massiv skalierten, KI-generierten Softwaresystemen zu gewährleisten.