Formale Verifikation bezeichnet den mathematisch strengen Nachweis, dass ein System eine Spezifikation erfüllt. Anders als Tests, die Stichproben prüfen, liefert sie Aussagen, die für alle zulässigen Eingaben gelten. In der KI-Debatte hat der Ansatz zwei Anknüpfungspunkte: die maschinelle Beweisführung in der Mathematik und die Frage, ob sich Sicherheitseigenschaften von KI-Systemen beweisen statt nur erproben lassen.
Zusammenfassung
Der Reiz des Verfahrens liegt in seiner Reichweite: Ein Test zeigt die Anwesenheit von Fehlern, ein Beweis deren Abwesenheit.
Für sicherheitskritische Software ist es seit Jahrzehnten etabliert. Auf KI übertragen ergeben sich zwei Richtungen. In der Mathematik ist die Verbindung bereits praktisch wirksam: Sprachmodelle erzeugen Beweisvorschläge, ein Beweisassistent prüft sie – die Unzuverlässigkeit der Erzeugung wird durch die Zuverlässigkeit der Prüfung aufgefangen.
In der KI-Sicherheit ist die Übertragung offen, weil sich die maßgeblichen Eigenschaften kaum formal fassen lassen. Dass Jacob Tsimerman seinen Wechsel zu OpenAI im Juli 2026 unmittelbar nach der Verleihung der Fields-Medaille bekanntgab und ihn ausdrücklich damit begründete, mathematische Gewissheit für KI-Sicherheit zu suchen, gilt als Anzeichen dafür, dass diese Frage ernsthaft verfolgt wird.
Grundlagen
Formale Verifikation verlangt drei Bestandteile: ein formales Modell des Systems, eine formale Spezifikation der geforderten Eigenschaft und ein Verfahren, das die Übereinstimmung nachweist.
| Verfahren | Vorgehen | Grenze |
|---|---|---|
| Modellprüfung | Durchmusterung aller Zustände | Zustandsraum wächst explosionsartig |
| Theorembeweisen | Ableitung aus Axiomen | erfordert menschliche Führung |
| Abstrakte Interpretation | Analyse über Näherungen | erzeugt Fehlalarme |
Der grundlegende Vorbehalt gilt für alle: Bewiesen wird die Übereinstimmung mit der Spezifikation, nicht deren Richtigkeit. Ist die Spezifikation unvollständig oder falsch, ist der Beweis wertlos – ein Problem, das dem äußeren Alignment-Problem entspricht.
Beweisassistenten
Ein Beweisassistent ist ein Programm, in dem mathematische Aussagen und Beweise so formuliert werden, dass jeder Schritt maschinell geprüft wird. Lean, ursprünglich von Leonardo de Moura entwickelt, ist gegenwärtig der verbreitetste; daneben bestehen Coq, Isabelle und weitere.
Die Bibliothek mathlib sammelt formalisierte Mathematik in erheblichem Umfang und bildet die Grundlage, auf der neue Formalisierungen aufsetzen.
Terence Tao hat mehrere Vorhaben dieser Art geleitet, darunter die Formalisierung der polynomialen Freiman-Ruzsa-Vermutung. Sein Argument ist arbeitsteilig: Wo Korrektheit maschinell geprüft wird, können viele Beteiligte zusammenarbeiten, ohne dass jemand die Beiträge der anderen nachvollziehen muss.
Verbindung mit KI
Die Verbindung ist wechselseitig und in der Mathematik bereits praktisch wirksam.
KI erzeugt, Verifikation prüft. Sprachmodelle schlagen Beweisschritte vor, der Assistent akzeptiert oder verwirft sie. Da die Prüfung zuverlässig ist, richtet der unzuverlässige Erzeuger keinen Schaden an – falsche Vorschläge werden zurückgewiesen. Tao benennt als größte Schwäche der Systeme, dass sie Fehler machen, die sich nicht überprüfen lassen; in der Mathematik entfällt dieser Nachteil.
Systeme. DeepMinds AlphaProof verbindet bestärkendes Lernen mit formaler Beweisführung in Lean und erreichte bei Aufgaben der Internationalen Mathematik-Olympiade Ergebnisse auf Medaillenniveau. Weitere Systeme verfolgen die automatische Übersetzung natürlichsprachlicher Mathematik in formale Form.
Verifikation erzeugt Trainingssignal. Ein geprüfter Beweis ist ein eindeutig korrektes Ergebnis. Das macht formale Mathematik zu einem geeigneten Gegenstand für bestärkendes Lernen mit überprüfbarer Belohnung – anders als bei Präferenzurteilen entfällt die Frage, ob die Bewertung stimmt.
Anwendung auf KI-Sicherheit
Die weitergehende Hoffnung lautet, Sicherheitseigenschaften von KI-Systemen zu beweisen statt nur zu erproben. Der Anlass ist eine erkannte Grenze: Red-Teaming, Benchmarks und Stresstests erfassen Stichproben. Ein Verhalten, das in keiner Prüfung auftrat, ist damit nicht ausgeschlossen – ein Vorbehalt, der bei Scheming besonders schwer wiegt, weil das fragliche Verhalten darauf angelegt ist, sich der Prüfung zu entziehen.
Die Schwierigkeiten sind erheblich:
Spezifizierbarkeit. Eigenschaften wie hilfreich, ehrlich oder harmlos lassen sich nicht formal fassen. Was sich beweisen ließe, sind engere Aussagen – etwa dass ein System bestimmte Handlungen nicht ausführt oder bestimmte Grenzen einhält.
Größenordnung. Modelle mit hunderten Milliarden Parametern entziehen sich der Analyse durch heutige Verfahren.
Modellierung. Ein Beweis gilt für ein formales Modell des Systems. Ob dieses das tatsächliche Verhalten erfasst, ist selbst nicht beweisbar.
Als gangbarer gilt daher, nicht das Modell zu verifizieren, sondern die Umgebung: Werden Handlungsbefugnisse durch verifizierte Komponenten begrenzt, so lässt sich der Schaden eines Fehlverhaltens beschränken, ohne das Modell selbst zu erfassen. Dieser Gedanke berührt sich mit den architektonischen Gegenmaßnahmen gegen Prompt Injection.
Was ein Beweis nicht beweist
Der Ausdruck bewiesen sicher legt eine Gewissheit nahe, die das Verfahren nicht liefern kann. Ein formaler Beweis ist eine Aussage über das Verhältnis zweier formaler Gegenstände: Ein Modell des Systems erfüllt eine Spezifikation. Beide Gegenstände sind menschgemacht, und beide können falsch sein.
Die Spezifikation kann das Falsche verlangen. Ein bewiesenermaßen spezifikationstreues System tut genau, was aufgeschrieben wurde – auch dann, wenn das Aufgeschriebene nicht das Gemeinte trifft. Die Erfahrung mit Zielspezifikationen im maschinellen Lernen zeigt, dass die Lücke zwischen Gemeintem und Formuliertem der Regelfall und nicht die Ausnahme ist.
Das Modell kann von der Wirklichkeit abweichen. Bewiesen wird über eine Abstraktion, die von Zeitverhalten, Hardwarefehlern, Seitenkanälen oder physikalischen Einflüssen absieht. Angriffe auf verifizierte Systeme setzen typischerweise genau dort an, wo die Abstraktion die Wirklichkeit weglässt.
Die Werkzeugkette gehört zur Vertrauensbasis. Der Beweisprüfer selbst, der Übersetzer, die Laufzeitumgebung – jedes dieser Werkzeuge müsste seinerseits korrekt sein. In der Praxis wird die Vertrauensbasis klein gehalten und geprüft, aber sie verschwindet nicht.
Für die KI-Sicherheit folgt daraus keine Absage, wohl aber eine Bescheidung. Verifikation kann bestimmte Ausschlüsse hart machen – dieser Prozess erhält keinen Netzzugang, jene Handlung wird ohne zweite Bestätigung nicht ausgeführt. Was sie nicht kann, ist die Frage beantworten, ob ein System wohlgesinnt ist; diese Frage ist nicht schwer zu beweisen, sondern nicht formulierbar.
Verwandte Begriffe
- Lean – verbreiteter Beweisassistent (eigener Artikel)
- Terence Tao – prominenter Anwender in der Mathematik
- Jacob Tsimerman – Mathematiker, der in die KI-Sicherheit wechselte
- AlphaProof – KI-System zur formalen Beweisführung
- Red-Teaming – empirisches Prüfverfahren mit den benannten Grenzen
- Scheming – Risiko, das empirische Prüfung besonders erschwert
- Outer Alignment – Problem der korrekten Spezifikation
- Prompt Injection – Bereich mit verwandtem Architekturansatz
Quellenangaben
- de Moura, Leonardo / Ullrich, Sebastian (2021): The Lean 4 Theorem Prover and Programming Language. In: CADE-28, LNCS 12699, S. 625–635.
- Google DeepMind (2024): AI Achieves Silver-Medal Standard Solving International Mathematical Olympiad Problems. Juli 2024.
- Sinha, Anusha / Grimes, Keltin / Lucassen, James / Feffer, Michael / VanHoudnos, Nathan / Wu, Zhiwei Steven / Heidari, Hoda (Carnegie Mellon University / Software Engineering Institute) (2025): From Firewalls to Frontiers: AI Red-Teaming is a Domain-Specific Evolution of Cyber Red-Teaming. arXiv: 2509.11398.
- Tao, Terence (2025): Machine-Assisted Proof. In: Notices of the American Mathematical Society 72 (1), S. 6–13.
- Tao, Terence (2026): Mathematics in the Age of AI. Öffentliche Vorlesung, International Congress of Mathematicians, Philadelphia, 24. Juli 2026.
- The mathlib Community, laufend. The Lean Mathematical Library.
← Zurück zur Lexikon-Übersicht
Zuletzt bearbeitet: 10. August 2026
Zusammengestellt, formuliert, lektoriert und korrigiert mit KI-Unterstützung. Kuratiert von Nils Brauer. Alle Angaben ohne Gewähr.