KI wird formale Verifikation in den Mainstream bringen

• Formale Verifikation (formal verification) ist eine Methode, mathematisch zu beweisen, dass Code eine Spezifikation stets erfüllt, und blieb lange auf einen begrenzten, forschungsnahen Bereich beschränkt
• Einige große Systeme wie der seL4-Mikrokernel wurden mithilfe formaler Verifikation entwickelt, doch wegen des hohen Schwierigkeitsgrads und der hohen Kosten wurde sie in der Industrie kaum eingesetzt
• In jüngster Zeit zeigen LLM-basierte Coding-Assistenten nicht nur bei Implementierungscode, sondern auch beim Schreiben von Beweisskripten in verschiedenen Sprachen Erfolge, was das Kostenmodell der Verifikation grundlegend verändern könnte
• Wenn KI neben der Codegenerierung auch den Korrektheitsbeweis automatisieren kann, könnte sich die Softwareentwicklung zu einem verlässlicheren Ansatz als menschliches Code-Review wandeln
• Die Automatisierung formaler Verifikation ist eine Schlüsseltechnologie zur Sicherung der Softwarezuverlässigkeit im KI-Zeitalter; für die breite Etablierung dürfte weniger die Technik als vielmehr ein kultureller Wandel entscheidend sein

---

Aktueller Stand und Grenzen der formalen Verifikation

• Beweisorientierte Sprachen und Werkzeuge wie Rocq, Isabelle, Lean, F*, Agda ermöglichen es, mathematisch zu beweisen, dass Code eine Spezifikation erfüllt
  • Der seL4-Betriebssystemkernel, der CompCert-C-Compiler und der Kryptoprotokoll-Stack Project Everest sind typische Beispiele
• In der Industrie wird formale Verifikation jedoch kaum verwendet
  • Bei seL4 waren für die Verifikation von 8.700 Zeilen C-Code 20 Personenjahre und 200.000 Zeilen Isabelle-Code nötig
  • Pro Zeile Implementierung waren 23 Zeilen Beweis und ein halber Personentag Arbeit erforderlich
• Weltweit gibt es Schätzungen zufolge nur einige Hundert Experten, die solche Beweise schreiben können
• Auch wirtschaftlich waren bei den meisten Systemen die Verifikationskosten höher als die Verluste durch Bugs, weshalb die praktische Nutzbarkeit gering war

Wie KI die Wirtschaftlichkeit formaler Verifikation verändert

• In jüngster Zeit zeigen LLM-basierte Coding-Assistenten nicht nur bei Implementierungscode, sondern auch beim Schreiben von Beweisskripten Erfolge
  • In Nature, bei Galois, auf arXiv usw. wurden Fälle berichtet, in denen LLMs Beweise in mehreren Sprachen erzeugt haben
• Derzeit ist noch Anleitung durch Experten nötig, doch eine vollständige Automatisierung scheint in den nächsten Jahren möglich
• Wenn die Verifikationskosten stark sinken, kann formale Verifikation auf deutlich mehr Software angewendet werden
• Gleichzeitig braucht von KI erzeugter Code formale Verifikation statt menschlicher Prüfung, um Zuverlässigkeit sicherzustellen
  • Wenn KI die Korrektheit ihres Codes selbst beweisen kann, könnte er gegenüber handgeschriebenem Code bevorzugt werden

Die komplementäre Beziehung zwischen LLMs und Beweisprüfung

• Wenn LLMs Beweisskripte schreiben, können sie zwar Falschinhalte (Halluzinationen) erzeugen, doch ein Proof Checker weist diese zurück
  • Der Checker besteht selbst aus kleinem, eigenständig verifiziertem Code, sodass falsche Beweise nur schwer akzeptiert werden können
• Dadurch ergänzt die Strenge formaler Verifikation die Unsicherheit von LLMs
• Diese Kombination bildet einen sicheren Automatisierungspfad, um die Zuverlässigkeit von KI-generiertem Code sicherzustellen

Neue Herausforderung: die Korrektheit der Spezifikation

• Auch in einer automatisierten Verifikationsumgebung bleibt die korrekte Definition der Spezifikation (specification) die zentrale Aufgabe
  • Es muss überprüft werden, ob die bewiesenen Eigenschaften tatsächlich den vom Entwickler beabsichtigten Eigenschaften entsprechen
• Das Schreiben von Spezifikationen erfordert weiterhin Fachwissen und sorgfältiges Nachdenken, ist aber deutlich einfacher und schneller als manuelle Beweise
• KI könnte auch die Übersetzung von Spezifikationen zwischen natürlicher Sprache und formalen Sprachen unterstützen
  • Allerdings besteht das Risiko von Bedeutungsverlusten, das jedoch als beherrschbar eingeschätzt wird

Ausblick auf Veränderungen in der Softwareentwicklung

• Entwickler könnten die gewünschten Eigenschaften des Codes deklarativ als Spezifikation beschreiben, während KI Implementierung und Beweis gemeinsam erzeugt
• In diesem Fall müssten Entwickler den von der KI erzeugten Code nicht mehr direkt prüfen und könnten ihn ähnlich vertrauensbasiert wie Maschinencode aus dem Compiler verwenden
• Zusammengefasst sind die folgenden drei Veränderungen zu erwarten
  1. Ein drastischer Rückgang der Kosten formaler Verifikation
  2. Eine steigende Nachfrage nach Verifikation, um das Vertrauen in KI-generierten Code sicherzustellen
  3. Die Präzision formaler Verifikation ergänzt die probabilistische Natur von LLMs
• Wenn diese Faktoren zusammenwirken, ist es sehr wahrscheinlich, dass formale Verifikation zu einer Mainstream-Technologie des Software Engineering wird
• Künftige Begrenzungsfaktoren dürften weniger technischer Natur sein als vielmehr die Geschwindigkeit, mit der Entwicklungskulturen den Wandel annehmen