Ein Quantenprogramm kann einen mathematisch korrekten Beweis mitbringen und trotzdem eine andere Aufgabe lösen als die, die wir ihm zugedacht haben. Das klingt widersinnig. Ein Beweisassistent prüft jedoch eine präzise formulierte Aussage. Ob diese Aussage die ursprüngliche Frage trifft, müssen Menschen beurteilen. Gerade wenn KI immer mehr Programme und Beweise erzeugt, wird dieser Übergang entscheidend.
Seit dem verifizierten Schaltungsoptimierer VOQC von 2019 hat sich das Prüfprogramm erweitert. Zwei neue Forschungsarbeiten vom Oktober 2026 richten den Blick auf zusammenhängende Garantien: Was liefert eine Berechnung, welche Mittel verbraucht sie, und unter welchen Voraussetzungen gilt ein Sicherheitsversprechen? Daraus zeichnet sich eine Entwicklung ab: Vertrauen entsteht durch eine nachvollziehbare Kette von der Aufgabe bis zum Ergebnis. Die einzelnen Glieder müssen zueinander passen.
Eine kürzere Schaltung soll dasselbe tun
Quantenprogramme bestehen aus Operationen auf Quantenbits, den Qubits. Man kann sich ihre Darstellung als Schaltplan mit Leitungen und kleinen Eingriffen vorstellen. Ein Optimierer sucht darin Umwege: Operationen lassen sich etwa zusammenfassen oder aufheben. Das spart knappe Rechenschritte. Die Schwierigkeit liegt darin, beim Aufräumen die Bedeutung der Schaltung zu erhalten.
Kesha Hietala und ihre Kollegen stellten dafür VOQC vor, zunächst 2019 als Vorabveröffentlichung und später 2021 als Fachaufsatz. Der Optimierer arbeitet mit der Beschreibungssprache SQIR. Seine Umformungen wurden im Beweisassistenten Coq auf ihre Korrektheit geprüft. So lässt sich mathematisch absichern, dass eine optimierte Schaltung im verwendeten Modell dasselbe bewirkt wie die Ausgangsschaltung.
Das ist eine wichtige Arbeitsteilung. Tests betrachten einzelne Fälle; ein Beweis kann eine Umformungsregel für alle im Modell zugelassenen Fälle absichern. Dennoch bleibt die Ausgangsaufgabe eine eigene Frage. Wenn eine Rechenvorschrift von Anfang an das falsche Ziel verfolgt, kann ein perfekter Optimierer dieses Ziel sehr zuverlässig erhalten.
Ergebnis und Rechnung gehören zusammen
Hier setzt Lean-QuantumAlg von Lei Zhang und Kollegen an, ein Preprint vom 21. Oktober 2026. Die Gruppe verbindet eine formulierte Aufgabe mit einem Algorithmus und dem Nachweis, dass dieser sie erfüllt. Zu diesem Vertrag gehören Erfolgsaussichten, geforderte Endzustände und Grenzen für die benötigten Ressourcen. Sämtliche Angaben beziehen sich auf dieselbe Ausführung.
Warum diese letzte Bedingung so viel ausmacht, zeigt ein einfaches Bild: Ein Lieferservice verspricht, ein Paket ans Ziel zu bringen und dabei höchstens zehn Kilometer zu fahren. Eine korrekte Zustellung und eine kurze Strecke helfen wenig, wenn die Strecke von einem anderen Fahrzeug stammt. Genauso müssen bei einem Quantenalgorithmus die gezählten Operationen zu dem Programm gehören, dessen Ergebnis bewiesen wurde.
Die Autoren erläutern das an einer elementaren Schaltungsumformung: Der Austausch zweier Quantenzustände lässt sich mit drei kontrollierten Operationen darstellen. Wer lediglich beweist, dass drei gleich eins plus eins plus eins ist, hat die Kosten dieser konkreten Schaltung noch nicht mit ihrer Funktion verknüpft. Das neue Framework leitet Verhalten und Ressourcenverbrauch aus derselben Programmausführung ab. So erhält die Mengenangabe einen festen Gegenstand.
Auch klassische Arbeit gehört zur Rechnung. Ein Quantenprogramm kann Messungen wiederholen und anschließend mit gewöhnlichen Rechenschritten auswerten. Wer nur die Quantengatter zählt, betrachtet einen Ausschnitt. Lean-QuantumAlg erfasst die im Modell dargestellten klassischen Operationen ebenfalls. Das hilft, große algorithmische Versprechen an den vollständiger beschriebenen Ablauf zu binden.
Geliehene Qubits haben Beziehungen
Eine weitere Verpflichtung betrifft geliehene Quantensysteme. Ein Algorithmus darf zusätzliche Qubits vorübergehend benutzen und muss sie vereinbarungsgemäß zurückgeben. Dabei reicht der isolierte Blick auf das geliehene Qubit nicht immer aus. Es kann mit anderen Systemen verschränkt sein: Sein Zustand gehört dann zu einer gemeinsamen Beziehung.
Eine Rückgabe könnte für sich betrachtet unverändert aussehen, während genau diese Beziehung zerstört wurde. Das Framework vergleicht deshalb den gemeinsamen Zustand des geliehenen Systems und eines äußeren Referenzsystems vor und nach der Berechnung. Der Prüfvertrag erfasst damit eine Eigenschaft, die in einer bloßen Liste korrekter Ausgabewerte leicht verloren geht.
Die Gruppe demonstriert ihren Ansatz an neun formalisierten Algorithmen. Dazu gehören auch mathematische Quantenangriffe auf RSA-2048 und die elliptische Kurve P-256. Hier werden Algorithmen unter festgelegten Modellannahmen bewiesen und mit Ressourcenbeschränkungen versehen. Die Arbeit berichtet über solche Formalisierungen; eine tatsächlich ausgeführte Entschlüsselung auf einem entsprechend leistungsfähigen Quantencomputer ist ihr Gegenstand nicht.
Ein fehlender Beweiszweig ist ein konkreter Gewinn
Eine unabhängige Gruppe um Ruixuan Deng untersucht eine andere Stelle der Vertrauenskette. Ihr Preprint FVQKD vom 22. Oktober formalisiert im Beweisassistenten Rocq einen Sicherheitsbeweis für das Quantenschlüsselaustauschverfahren BB84. Zwei Beteiligte gewinnen dabei aus Quantensignalen und anschließender Verarbeitung einen gemeinsamen geheimen Schlüssel. Der betrachtete Beweis gilt für endliche Datenmengen und eine Sicherheit, die auch bei weiterer Verwendung des Schlüssels erhalten bleibt.
Die maschinelle Prüfung zwang das Team, Voraussetzungen auszuformulieren, die im schriftlichen Argument teilweise implizit geblieben waren. Besonders anschaulich ist ein Fall mit sehr geringer Wahrscheinlichkeit, dass das Protokoll eine Prüfung besteht. In diesem Bereich wurde eine mathematische Beziehung außerhalb ihrer zulässigen Voraussetzungen benutzt. Die Formalisierung ergänzt einen eigenen Beweiszweig: Weil das Protokoll dort fast immer abbricht, lässt sich die benötigte Sicherheitsgrenze anders absichern.
Laut den Autoren bleiben dabei die veröffentlichte Schlüssellängenformel und die Sicherheitsgarantie erhalten. Der Gewinn ist eine vollständigere Begründung. Solche Befunde zeigen den praktischen Wert formaler Prüfung: Sie kann stillschweigende Übergänge sichtbar machen, die beim Lesen einer langen Argumentation leicht übersehen werden.
Der Mensch bestimmt, was der Beweis bedeutet
Der stärkste Einwand gegen große Vertrauensversprechen bleibt bestehen. Eine exakt bewiesene Aussage kann durch ihre Voraussetzungen sehr bequem werden. Wird eine Aufgabe auf leichte Eingaben beschränkt oder praktisch jede Ausgabe als Erfolg zugelassen, bestätigt der Beweis diese schwächere Forderung. Deshalb lässt Lean-QuantumAlg die Aufgabenbeschreibung und das Ausführungsmodell ausdrücklich bei der menschlichen Prüfung.
Das Modell legt auch fest, was als elementarer Schritt zählt. Eine umfangreiche Unterroutine kann in einem Modell als einzelne erlaubte Operation erscheinen. Ob das zum angekündigten Rechenaufwand passt, ergibt sich aus dem Vergleich mit dem tatsächlichen Vorhaben. Beim Schlüsselaustausch wiederum müssen reale Quellen und Messgeräte die angenommenen Eigenschaften erfüllen. FVQKD behandelt den informationstheoretischen Sicherheitsbeweis; Geräteangriffe und technische Seitenkanäle liegen außerhalb seines beschriebenen Geltungsbereichs.
Die drei Forschungsstränge ergeben somit keine pauschale Sicherheitsgarantie für Quantensoftware. Sie zeigen eine konkretere, nützliche Richtung: Immer mehr Verbindungen innerhalb eines Rechenversprechens werden maschinell prüfbar. Für Entwickler und Prüfer verschiebt sich die anspruchsvolle Arbeit zu den Stellen, an denen Bedeutung festgelegt wird. Welche Aufgabe? Welches Gerät im Modell? Welcher Aufwand? Ein gutes Zertifikat macht diese Fragen auffindbar, bevor jemand seinem Ergebnis vertraut.
Quellen
- Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu und Michael Hicks: A Verified Optimizer for Quantum Circuits, Preprint vom 4. Dezember 2019, überarbeitete Fassung vom 13. November 2020, Fachaufsatz 2021.
- Lei Zhang, Mingrui Jing, Yusheng Zhao, Jiahong Liu und Xin Wang: Lean-QuantumAlg: A Framework for AI Agents to Produce Quantum Algorithms that Humans Can Trust, Preprint vom 21. Oktober 2026.
- Ruixuan Deng, Zhengfeng Ji, Jiayu Zhang und Li Zhou: FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq, Preprint vom 22. Oktober 2026.
Für diesen Artikel wurden KI-gestützte Recherche- und Editierwerkzeuge verwendet. Der Inhalt wurde redaktionell geprüft.
