Verified: Formaler Beweis mit null Fehlern in der KI

Im August 2026 veröffentlichte der Forscher Dmitry V. Alexandrov auf arXiv die erste mechanisierte Formalisierung von Romanovs Triplet Logic, umgesetzt mit dem Proof Assistant Rocq. Die ungewöhnliche Entscheidung zeigt sich sofort: Vor dem Bau eines ausführbaren Werkzeugs beschloss er, jede mathematische Eigenschaft des Systems zu beweisen. Das Ergebnis trägt ein Etikett, das in Produktionssoftware selten ist: verified.

Die ursprüngliche Idee: erst die Theorie beweisen, dann das Werkzeug extrahieren

Die Triplet Logic, abgekürzt TLS, ist ein kombinatorisches Framework auf Basis von Tripletts. Es dient dazu, über kompatible Pfade innerhalb geschichteter Strukturen zu schließen, der sogenannten Compact Triplets Structures. Der operative Motor ist eine Schnittprozedur: die Simple Vertex Intersection.

Alexandrov formalisierte den Kern der Theorie in Rocq. Er bezog die Compact Triplets Formulas, die Hyperstrukturen, die Clearing-Prozedur und die SVI selbst ein.

Die Logik hinter dieser Entscheidung ist klar. Eine eigenständige mathematische Theorie verdient bewiesene Fundamente, vor jedem anwendungsbezogenen Versprechen. Viele Softwareprojekte kehren die Reihenfolge um: Sie schreiben den Code und suchen anschließend nach Garantien. Hier ist die Sequenz methodisch umgedreht, und diese Umkehrung prägt die gesamte Geschichte. Die Umkehrung der Reihenfolge hat eine präzise Konsequenz. Jede vom Werkzeug genutzte Eigenschaft ruht auf einem bereits geschlossenen Beweis. Jeder Spielraum für nachgelagert angenommene Garantien entfällt. Wer den Code erbt, erbt auch die Beweise.

Die verifizierten Ergebnisse

Die Zahlen dieser Arbeit haben einen expliziten Nenner. Jede Ziffer verweist auf ein öffentliches, reproduzierbares Artefakt.

Laut dem auf arXiv hinterlegten Paper umfasst die Rocq-Entwicklung über 23.000 Zeilen Code, verteilt auf siebzehn Dateien, mit 427 bewiesenen Lemmata und Theoremen und null zugelassenen Beweiszielen.

• Über 23.000 Zeilen Rocq-Code
• 17 Entwicklungsdateien
• 427 bewiesene Lemmata und Theoreme
• Null zugelassene Beweisziele (zero admitted goals)

Der Ausdruck zero admitted goals verdient Aufmerksamkeit. In einem Proof Assistant ist ein zugelassenes Beweisziel ein Schritt, der als wahr gesetzt wird, ohne Beweis. Ein einziges zugelassenes Beweisziel schwächt die gesamte Kette. Ein einziges unbewiesenes Glied genügt, um alles darüber Liegende zu schwächen. Sie auf null zu bringen bedeutet: Die gesamte Kette trägt sich selbst. Jedes Theorem steht ohne Abkürzung.

Eine weitere Zahl betrifft die Komplexität. Alexandrov beweist explizite polynomielle Zeitschranken für die Phasen des Filters. Diese theoretische Garantie begleitet die Benchmarks auf zufälligen und strukturierten Instanzen, und die beiden Messungen konvergieren zum vorhergesagten Verhalten. Die Konvergenz zählt. Die bewiesene Schranke sagt, wie sich der Code verhalten sollte. Der Benchmark zeigt, wie er sich tatsächlich verhält. Wenn die beiden Werte übereinstimmen, beweist sich die Theorie in der Praxis. Die vollständige Toolchain ist als kuratiertes Artefakt auf Zenodo verfügbar.

Die Korrektheitsgrenze: wo die Geschichte lehrreich wird

Der zentrale Beitrag ist eine präzise Korrektheitsgrenze. Hier gewinnt die Geschichte echten Wert.

Die Existenz einer Menge, die das System erfüllt, impliziert eine besetzte SVI. Die umgekehrte Implikation scheitert im allgemeinen Fall. Eine besetzte SVI lässt die Existenz einer gültigen Lösung offen. Die Verbindung gilt in einer Richtung; die Gegenrichtung bleibt offen.

Für ausgerichtete Strukturen wird die doppelte Implikation vollständig. Sie gilt auch für Systeme ausgerichteter Strukturen. In diesem Perimeter deckt die Methode beide Richtungen ab.

Es gibt mehr. Alexandrov formalisiert die Korrektheit der Übersetzung mit gruppierten Fenstern. Dann zeigt er ein formales Gegenbeispiel zu ihrer Vollständigkeit und erklärt die Grenze mit derselben Sorgfalt wie die Theoreme. Das ist der Moment der Reibung: Eine Arbeit, die zeigt, wo sie an ihre Grenze stößt, ist wertvoller als eine, die totale Abdeckung verspricht. Die Eingrenzung bleibt die informativste Angabe. Wer liest, weiß im Voraus, wo die Methode endet. Diese Transparenz ist wertvoller als eine generische Garantie, weil sie die Überraschung in der Produktion eliminiert.

Vom Beweis zum Prototyp: VFR

Die bewiesene Theorie wird zum Werkzeug. Alexandrov extrahiert VFR, einen Prototyp in OCaml.

VFR bietet zwei unterschiedliche Garantien. Für das Sliding-Window-Fragment liefert es eine verifizierte Entscheidungsprozedur. Für das allgemeine 3-CNF bietet es einen einseitig korrekten Filter.

Ein einseitiger Filter hat eine nützliche Eigenschaft: Wenn er eine Instanz ausschließt, ist der Ausschluss verlässlich. Falsche Aussonderungen sind ausgeschlossen. Wenn er eine Instanz passieren lässt, bleibt das Urteil offen. Wer diese Asymmetrie kennt, nutzt das Werkzeug richtig. Der Prototyp kommt mit einer Python-Laufzeitumgebung und reproduzierbarem Docker-Packaging.

Die Reproduzierbarkeit ist hier konkrete Substanz, weit über die Rahmung hinaus. Alle können das Artefakt herunterladen, die Benchmarks ausführen und die Ergebnisse mit den erklärten Werten vergleichen. Der Wert dieser Entscheidung zeigt sich im Vergleich mit der gängigen Praxis: Viele KI-Werkzeuge kommen als geschlossene Boxen, mit schwer replizierbaren Ergebnissen. VFR geht den entgegengesetzten Weg.

Was 'verified' für alle bedeutet, die KI bauen

Der Begriff verified zirkuliert reichlich im KI-Marketing. Dieser Fall gibt dem Wort sein ursprüngliches Gewicht zurück.

Ein verifiziertes Ergebnis erklärt drei Dinge: was bewiesen wurde, mit welcher Methode, innerhalb welcher Grenze. Alexandrovs Arbeit erfüllt alle drei Kriterien.

Für einen CTO ist die Lektion direkt. Eine formale Garantie ist so viel wert wie der Perimeter, den sie erklärt. Ein einseitig korrekter Filter mit expliziten Grenzen ist nützlicher als ein opakes Modell, das alles verspricht. Der erklärte Perimeter sagt, wo das Werkzeug trägt und wo Vorsicht gilt. Ein opakes Modell lässt diese Frage offen und verlagert das Risiko auf das Team, das es integriert.

Diese Position kehrt in vielen Enterprise-Fällen wieder, die dieser Desk untersucht hat. Ergebnisse, die halten, tragen stets einen expliziten Nenner, während aufgeblähte Ergebnisse den Vorher-Nachher-Vergleich meiden. Für ein Board betrifft das Signal die Benchmarks des Möglichen: Die Messlatte des Vertrauens verschiebt sich zur überprüfbaren Evidenz.

What you can take from this

Die Geschichte bietet ein übertragbares Playbook, auch außerhalb der formalen Logik.

Erste Lektion: Die erklärte Gültigkeitsgrenze erhöht die Glaubwürdigkeit. Ein Ergebnis mit expliziten Grenzen besteht die externe Prüfung.

Zweite Lektion: Reproduzierbarkeit verwandelt eine Behauptung in Evidenz. Offener Code, offene Benchmarks und offenes Packaging erlauben allen die Überprüfung.

Dritte Lektion: Die Reihenfolge zählt. Die Fundamente vor der Extraktion des Werkzeugs zu beweisen reduziert das nachgelagerte Risiko. Für ein KMU, das KI integriert, gilt das Prinzip identisch: die Metrik definieren, den Perimeter erklären, das Ergebnis überprüfbar machen. Diese Disziplin unterscheidet ein operatives Ergebnis von einer Kommunikation.

Die offene Frage

Jede Organisation, die KI einführt, steht vor derselben Wahl. Wie viel der eigenen Ergebnisse besteht eine externe, reproduzierbare Kontrolle?

Alexandrov investierte über 23.000 Zeilen Beweis, um die Antwort öffentlich zu machen. Die meisten Enterprise-Deployments bleiben weit von diesem Standard entfernt.

Die Frage an die Leser ist konkret: Welche Metrik Ihres letzten KI-Projekts übersteht ein unabhängiges Audit, mit Wert vorher und nachher? Die Antwort zeigt die Distanz zwischen dem, was Sie verkünden, und dem, was Sie beweisen können.