formal verifiziert
Formal verifiziert bedeutet, dass die Korrektheit eines Programms oder einer KI-Komponente mathematisch bewiesen wurde — nicht nur durch Tests, sondern durch einen Beweis, der alle möglichen Eingaben abdeckt. In der KI-Sicherheitsforschung gilt formale Verifikation als eines der wenigen Verfahren, das Garantien statt bloßer Wahrscheinlichkeiten liefert.
Wenn Software getestet wird, prüft man eine begrenzte Auswahl von Fällen. Läuft alles durch, gilt das Programm als wahrscheinlich korrekt. Bei formaler Verifikation ist das anders: Ein mathematischer Beweis zeigt, dass das Programm unter allen denkbaren Umständen eine festgelegte Eigenschaft erfüllt. Es gibt keine Ausnahme, die im Test zufällig nicht auftauchte. Das Verfahren stammt ursprünglich aus der Mathematik, wo ein Satz erst dann gilt, wenn er bewiesen ist — nicht wenn er in tausend Fällen stimmt.
Garantie statt Stichprobe
Tests haben ein strukturelles Problem: Sie können zeigen, dass ein Fehler vorhanden ist, aber nie beweisen, dass keiner existiert. Ein Test mit einer Million Eingaben lässt trotzdem unendlich viele Fälle offen. Bei einem Autopiloten oder einem medizinischen Diagnosesystem kann genau dieser ungetestete Fall der entscheidende sein.
Formale Verifikation schließt diese Lücke. Sie eignet sich vor allem für klar definierte Eigenschaften: „Dieses Programm teilt niemals durch null.“, „Die Ausgabe liegt immer zwischen 0 und 1.“, „Der Roboter bewegt sich nie schneller als 1 m/s auf eine Person zu.“ Solche Zusicherungen lassen sich beweisen, nicht nur wahrscheinlich machen.
Deshalb ist formale Verifikation besonders in sicherheitskritischen Bereichen wertvoll: in der Luftfahrt, in Kernkraftwerken und zunehmend in der KI-Forschung, wo diskutiert wird, wie man sicherstellt, dass ein Modell bestimmte Grenzen nie überschreitet.
Beweisen statt Ausprobieren
Grundlage ist eine formale Spezifikation: eine präzise, mathematische Beschreibung dessen, was das Programm tun soll. Umgangssprache reicht dafür nicht — „das System soll sicher sein“ ist keine prüfbare Aussage. Stattdessen formuliert man Eigenschaften in einer Logiksprache, zum Beispiel: „Für jede mögliche Eingabe x gilt: Wenn x größer als null ist, dann ist die Ausgabe positiv.“
Ein Beweisassistent — ein spezielles Programm — prüft dann, ob der Code diese Eigenschaft tatsächlich immer erfüllt. Bekannte Werkzeuge dafür heißen Coq, Isabelle oder Lean. Sie zwingen den Entwickler, jeden Schritt der Argumentation explizit zu machen. Lücken im Beweis werden als Fehler angezeigt, ähnlich wie Syntaxfehler in normalem Code.
Für einfache Programme ist das aufwendig, aber machbar. Bei großen neuronalen Netzen, also den Modellen hinter modernen KI-Systemen, stoßen aktuelle Methoden noch an Grenzen: Die Anzahl möglicher Zustände ist so riesig, dass vollständige Beweise rechnerisch kaum zu erbringen sind. Forscher arbeiten deshalb an vereinfachten Teilbeweisen, die zumindest für bestimmte Schichten oder Ausgaben Garantien liefern.
Wo formal verifiziert in der Praxis auftaucht
Im Alltagsleben steckt formale Verifikation meist unsichtbar in Systemen, bei denen ein Absturz keine Option ist. Der Bordcomputer der Ariane-5-Rakete enthielt einen Fehler in einer Typumwandlung — eine Art von Bug, den formale Verifikation hätte ausschließen können. Beim Nachfolger wurden Teile des Codes tatsächlich formal verifiziert.
In der KI-Debatte taucht der Begriff im Zusammenhang mit KI-Sicherheit auf. Organisationen wie DeepMind oder das Alignment Forum diskutieren, ob künftige KI-Systeme formal verifizierte Sicherheitseigenschaften haben müssen, bevor sie eingesetzt werden dürfen. Die Idee: Ein Modell, dessen Verhalten mathematisch bewiesen korrekt ist, wäre zuverlässiger als eines, das nur gut getestet wurde.
Auch in der Chipentwicklung spielt das Verfahren eine große Rolle. Intel und AMD verwenden formale Methoden, um sicherzustellen, dass ihre Prozessoren arithmetisch korrekt rechnen — eine Reaktion auf den Pentium-FDIV-Bug aus dem Jahr 1994, bei dem ein Rechenfehler im Chip Millionen Dollar Rückrufkosten verursachte. Seitdem ist formale Verifikation in der Halbleiterindustrie Standard für kritische Recheneinheiten.