AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs (Technical Report)

AutoQ 2.0 ist ein fortschrittlicher Verifizierer, der die Verifizierung von Quantenschaltkreisen auf vollständige Quantenprogramme ausweitet, indem er theoretische und ingenieurtechnische Herausforderungen im Zusammenhang mit klassischem Kontrollfluss adressiert, und der seine Effizienz erfolgreich an komplexen Algorithmen wie Repeat-Until-Success und schwachmessungsbasierter Grover-Suche demonstriert.

Das Wesentliche

Das große Ganze: Von statischen Bauplänen zu dynamischen Rezepten

Stellen Sie sich vor, Sie bauen ein Haus.

• AutoQ 1.0 (Die alte Version) war wie ein Werkzeug, das nur statische Baupläne prüfen konnte. Es konnte verifizieren, ob ein bestimmter, unveränderlicher Satz von Wänden und Balken (ein „Quantenschaltkreis") korrekt gebaut wurde. Aber es konnte kein Haus handhaben, bei dem der Architekt entschied: „Wenn der Wind von Norden kommt, baue ich eine Veranda; sonst baue ich eine Garage."
• AutoQ 2.0 (Die neue Version) ist ein Werkzeug, das dynamische Rezepte prüfen kann. Es versteht, dass Quantenprogramme nicht nur statische Schaltkreise sind; sie sind Anweisungen, die Entscheidungen treffen (Verzweigungen) und Schritte wiederholen (Schleifen) können, basierend darauf, was während des Prozesses passiert.

Die Autoren haben dieses neue Werkzeug entwickelt, um zu verifizieren, dass diese komplexen, entscheidungsfälligen Quantenprogramme genau so funktionieren, wie der Programmierer es beabsichtigt, ohne dass ein Mensch jeden einzelnen Schritt manuell prüfen muss.

Die Kernherausforderung: Das „Kollaps"-Problem

In der Quantenwelt gibt es eine einzigartige Regel: Messung.
Stellen Sie sich eine sich drehende Münze vor, die gleichzeitig Kopf und Zahl ist (eine Superposition). In dem Moment, in dem Sie sie ansehen (messen), „kollabiert" sie entweder zu Kopf oder zu Zahl.

• Die Schwierigkeit: In älteren Werkzeugen wurde die Mathematik, sobald man eine Münze gemessen hatte, chaotisch. Die Wahrscheinlichkeiten mussten „normalisiert" werden (neu berechnet, damit sie 100 % ergeben), was die Computermathematik unglaublich langsam und schwierig machte.
• Der AutoQ 2.0-Trick: Die Autoren erkannten, dass sie die Mathematik nicht sofort korrigieren mussten. Sie entschieden, die Zahlen während des Prozesses „chaotisch" (nicht normalisiert) zu lassen und nur zu prüfen, ob die Form des Ergebnisses korrekt war. Sie bauten einen speziellen „Implikationstest" (ein Vergleichswerkzeug), der sagt: „Selbst wenn Ihre Zahlen hoch- oder runter skaliert sind, solange das Muster übereinstimmt, sind Sie in Ordnung." Das ist wie der Vergleich, ob zwei Karten die gleichen Straßen haben, auch wenn eine Karte im Maßstab 1:100 und die andere im Maßstab 1:1000 gezeichnet ist.

Der Motor: „Level-Synchronisierte Baumautomaten" (LSTAs)

Um diese komplexen Programme zu handhaben, verwendet das Werkzeug eine spezielle Datenstruktur namens LSTAs.

• Die Analogie: Stellen Sie sich einen Quantenzustand als einen riesigen, verzweigten Baum vor. Jeder Ast repräsentiert einen möglichen Pfad, den der Quantencomputer nehmen könnte.
• Das Problem: Standardwerkzeuge versuchen, jedes einzelne Blatt auf dem Baum zu zeichnen. Wenn Sie 100 Qubits (Quantenbits) haben, hat der Baum mehr Blätter als Atome im Universum. Es ist unmöglich, sie alle zu zeichnen.
• Die Lösung (LSTAs): Anstatt jedes Blatt zu zeichnen, verwenden LSTAs eine „Schablone" oder ein „Muster". Sie sagen: „Alle Äste auf dieser Ebene sehen so aus."
• Der „synchronisierte" Teil: Das ist die Zaubersauce. In einem Quantenprogramm, wenn Sie an einem Teil des Baumes eine Entscheidung treffen, beeinflusst dies den gesamten Baum auf dieser Ebene. LSTAs stellen sicher, dass alle Äste auf derselben „Etage" des Baumes derselben Entscheidung zustimmen. Das ist wie ein Chor, in dem alle auf derselben Tonhöhe singen müssen; wenn eine Person einen anderen Ton singt, bricht die gesamte Harmonie zusammen. Dies ermöglicht es dem Werkzeug, massive Quantenzustände in eine winzige, handhabbare Datei zu komprimieren.

Wie es funktioniert: Die drei Schritte

Wenn Sie ein Quantenprogramm mit AutoQ 2.0 verifizieren möchten, agieren Sie wie ein Lehrer, der die Hausaufgaben eines Schülers korrigiert:

1. Das Setup (Vorbedingungen): Sie sagen dem Werkzeug: „Starten Sie mit einer Münze, die sich so dreht." (Dies ist der Eingabezustand).
2. Die Schleife (Invarianten): Wenn das Programm eine Schleife hat (eine „wiederhole bis"-Anweisung), müssen Sie eine „Schleifeninvariante" angeben.
   • Analogie: Stellen Sie sich einen Läufer vor, der Runden dreht. Sie sagen dem Werkzeug: „Egal wie viele Runden er läuft, er wird immer auf der Bahn bleiben." Sie müssen nicht jeden einzelnen Schritt prüfen; Sie müssen nur beweisen, dass, wenn er am Anfang einer Runde auf der Bahn ist, er am Ende der Runde immer noch auf der Bahn sein wird.
3. Das Ziel (Nachbedingungen): Sie sagen dem Werkzeug: „Das Programm muss mit der Münze enden, die Kopf zeigt."

Das Werkzeug führt das Programm dann virtuell aus und nutzt sein „Muster" (LSTA), um den Zustand zu verfolgen. Es prüft:

• Hat das Programm korrekt begonnen?
• Hält die Schleife den Läufer auf der Bahn (die Invariante)?
• Endete das Programm damit, dass die Münze Kopf zeigt?

Reale Tests: Was haben sie verifiziert?

Die Autoren testeten AutoQ 2.0 an zwei sehr schwierigen Arten von Quantenprogrammen, die frühere Werkzeuge nicht automatisch handhaben konnten:

1. Wiederholen-bis-Erfolg (Repeat-Until-Success, RUS):

   • Das Szenario: Stellen Sie sich vor, Sie versuchen, einen Kuchen zu backen, wissen aber nicht, ob der Ofen heiß genug ist. Sie legen den Kuchen hinein, prüfen die Temperatur und wenn es zu kalt ist, nehmen Sie ihn heraus, warten und versuchen es erneut. Sie wiederholen dies, bis der Kuchen fertig ist.
   • Das Ergebnis: AutoQ 2.0 verifizierte diese „nochmal-versuchen"-Algorithmen sofort.

2. Schwache-Messung Grover-Suche:

   • Das Szenario: Grovers Algorithmus ist eine berühmte Methode, um eine Nadel im Heuhaufen zu finden. Die „Schwache-Messung"-Version ist eine knifflige neue Art, dies zu tun, bei der Sie vorsichtig in den Heuhaufen spähen, ohne ihn sofort vollständig kollabieren zu lassen, was es Ihnen ermöglicht, weiterzusuchen, selbst wenn Sie die Nadel nicht sofort finden.
   • Das Ergebnis: Dies ist ein massives Programm. Die Autoren verifizierten eine Version mit 100 Qubits (eine riesige Zahl für das Quantencomputing) in etwa 20 Minuten. Dies ist eine massive Skalierung im Vergleich zu dem, was zuvor möglich war.

Das Fazit

AutoQ 2.0 ist ein Durchbruch, weil es das erste Werkzeug ist, das komplexe Quantenprogramme, die Schleifen und Entscheidungsfindung verwenden, automatisch verifizieren kann. Dies erreicht es durch die Verwendung intelligenter „Mustererkennung" (LSTAs), um nicht in unmöglicher Mathematik stecken zu bleiben, und durch einen klugen Umgang mit der chaotischen Mathematik von Quantenmessungen.

Es hat erfolgreich bewiesen, dass diese fortschrittlichen Quantenrezepte korrekt funktionieren, selbst für sehr große Systeme, ohne dass ein Mensch die schwere Arbeit des Beweises leisten muss.

Technische Zusammenfassung

Technische Zusammenfassung: AutoQ 2.0: Von der Verifikation quantenmechanischer Schaltkreise zur Verifikation quantenmechanischer Programme

1. Problemstellung

Quantenprogramme erweitern quantenmechanische Schaltkreise durch die Einbeziehung klassischer Kontrollflusskonstrukte wie Verzweigungen und Schleifen. Während quantenmechanische Schaltkreise (das Domäne von AutoQ 1.0) ausreichen, um statische Folgen von Gattern zu definieren, erfordern fortgeschrittene Quantenalgorithmen – wie Repeat-Until-Success (RUS)-Algorithmen und schwache Messung basierte Versionen von Grovers Suche – eine dynamische Steuerung basierend auf klassischen Werten, die aus Qubit-Messungen gewonnen werden.

Die Verifikation dieser Programme stellt erhebliche Herausforderungen dar, die bei der reinen Schaltkreisverifikation nicht auftreten:

• Messung und Normalisierung: Messungen kollabieren quantenmechanische Zustände und liefern klassische Werte (0 oder 1), die den Kontrollfluss steuern. Dieser Prozess erfordert oft eine Normalisierung von Wahrscheinlichkeitsamplituden, was formales Schließen erschwert.
• Schlussfolgern über Kontrollfluss: Die Verifikation von Schleifen und Verzweigungen erfordert den Umgang mit Zustandsräumen, die sich basierend auf Messergebnissen entwickeln, eine Aufgabe, die für bestehende automatisierte Werkzeuge schwierig ist.
• Fehlende automatisierte Werkzeuge: Zwar existieren deduktive Verifikationswerkzeuge für klassische Programme (z. B. Dafny, KeY) und einige Quantenwerkzeuge (z. B. CoqQ, Qbricks), doch fehlt ihnen entweder die vollständige Automatisierung oder sie erfordern erheblichen manuellen Aufwand (z. B. die Bereitstellung komplexer hermitescher Operatoren oder umfangreiche Beweis-Suchen). Bestehende automatisierte Werkzeuge konzentrieren sich oft auf Schaltkreisäquivalenz oder spezifische parametrisierte Programme und bieten keine allgemeine Unterstützung für Kontrollfluss in Quantenprogrammen.

2. Methodik

AutoQ 2.0 adressiert diese Herausforderungen, indem es das vorherige Schaltkreisverifikationsframework erweitert, um vollständige Quantenprogramme zu unterstützen. Die Kernmethodik basiert auf Level-Synchronisierten Baumautomaten (LSTAs) und einem neuartigen Entailment-Testansatz (Folgerungstest).

2.1 Formales Modell: Level-Synchronisierte Baumautomaten (LSTAs)

Das Werkzeug repräsentiert Mengen von Quantenzuständen (Vorbedingungen, Nachbedingungen und Schleifeninvarianten) mittels LSTAs.

• Struktur: LSTAs sind symbolische Baumautomaten, die entwickelt wurden, um Quantenzustände als perfekte binäre Bäume zu kodieren, wobei Äste rechnerische Basiszustände repräsentieren und Blätter komplexe Wahrscheinlichkeitsamplituden darstellen.
• Synchronisation: Ein Schlüsselmerkmal von LSTAs ist der „Choice"-Mechanismus (Auswahlmechanismus). Übergänge auf derselben Baumebene müssen eine gemeinsame Auswahlmenge teilen. Dies ermöglicht es LSTAs, verschränkte Zustände und Überlagerungen, die mit Standard-Baumautomaten nicht kompakt darstellbar sind, kompakt zu repräsentieren, indem sichergestellt wird, dass nur gültige Kombinationen von Ästen (jene, die eine Auswahl teilen) generiert werden.
• Eingabeformat: Benutzer geben Vorbedingungen, Nachbedingungen und Schleifeninvarianten als .lsta-Dateien an, die die Automaten definieren, die die Mengen gültiger Quantenzustände erkennen.

2.2 Verifikationsframework

Der Verifikationsprozess ist automatisiert und folgt einem deduktiven Stil:

1. Programmausführung: Das Werkzeug führt Quantengatter (z. B. $H$, $CX$, $T$) auf dem LSTA aus, der die Vorbedingung repräsentiert.
2. Umgang mit Messung und Verzweigungen:
   • Wenn eine Messung $M_i = b$ auftritt, wird der LSTA in zwei Kopien aufgeteilt, die den Ergebnissen $b=0$ und $b=1$ entsprechen.
   • Der Algorithmus aktualisiert den Baum, indem er die Wahrscheinlichkeitsamplituden der nicht übereinstimmenden Äste auf Null setzt (z. B. wenn $M_1=0$, werden die Amplituden des $1$-Teilbaums unter $x_1$ auf 0 gesetzt).
   • Entscheidend ist, dass das Werkzeug die Amplituden in diesem Schritt nicht normalisiert. Es bewahrt die rohen Amplituden, um komplexe Arithmetik während der Ausführung zu vermeiden und Normalisierungsprüfungen auf den finalen Entailment-Test zu verschieben.
   • Verzweigungsanweisungen werden behandelt, indem die resultierenden LSTAs für beide Pfade (wahr und falsch) berechnet und deren Vereinigung gebildet wird.
3. Umgang mit Schleifen:
   • Für while-Schleifen muss der Benutzer eine Schleifeninvariante als LSTA bereitstellen.
   • Das Werkzeug verifiziert, dass die Invariante induktiv ist: Sie muss alle vor der Schleife erreichbaren Zustände abdecken, und die Ausführung des Schleifenkörpers auf der Invariante (bedingt durch die Schleifenfortsetzung) muss zu Zuständen führen, die weiterhin von der Invariante abgedeckt werden.
   • Die Zustände beim Schleifenaustritt werden durch die Invariante, bedingt durch das Schleifenende, überapproximiert.
4. Entailment-Test (bis auf Skalierung):
   • Der letzte Schritt prüft, ob die Menge der erreichbaren Zustände (repräsentiert durch einen LSTA $R$) in der Nachbedingung (LSTA $Q$) enthalten ist.
   • Da Normalisierungsfaktoren während der Ausführung ignoriert wurden, verwendet das Werkzeug eine spezialisierte Entailment-Relation bis auf Skalierung ($|=_{uts}$).
   • $A |=_{uts} B$ gilt, wenn jeder Baum in $A$ eine linear skalierte Version eines Baums in $B$ ist (d. h. $T_A = r \cdot T_B$ für einen nicht-Null-Skalierungsfaktor $r$).
   • Dieser Check wird mittels eines Graphensuchalgorithmus durchgeführt, der die LSTAs Ebene für Ebene durchläuft, Zustände und Terme abbildet und schließlich einen SMT-Löser (Z3) aufruft, um die Existenz eines Skalierungsfaktors $r$ zu verifizieren, der die globalen Constraints erfüllt.

3. Hauptbeiträge

• Erweiterung auf Quantenprogramme: AutoQ 2.0 ist das erste Werkzeug, das eine automatisierte deduktive Verifikation für Quantenprogramme mit Schleifen und Verzweigungen bietet und damit über den reinen Schaltkreisbereich von AutoQ 1.0 hinausgeht.
• Automatisierter Umgang mit Messung: Das Werkzeug führt Algorithmen ein, um LSTAs basierend auf Messergebnissen aufzuteilen und die resultierenden Zustandsräume ohne manuellen Eingriff zu verwalten.
• Normalisierungsfreie Verifikation: Durch die Entwicklung eines Entailment-Tests, der mit nicht-normalisierten Zuständen (bis auf Skalierung) arbeitet, vermeidet das Werkzeug die rechnerische Komplexität der Normalisierung von Amplituden während der Ausführungsphase und verbessert die Effizienz erheblich.
• LSTA-basierte Invarianten: Das Framework nutzt LSTAs zur Darstellung von Schleifeninvarianten, was eine kompakte Repräsentation komplexer Quantenzustände ermöglicht, die für iterative Algorithmen erforderlich sind.
• Skalierbarkeit: Der Ansatz unterstützt die Verifikation von Programmen mit einer großen Anzahl von Qubits (bis zu 100 Qubits in den berichteten Benchmarks), indem er die Kompaktheit von LSTAs und effizientes SMT-Lösen nutzt.

4. Experimentelle Ergebnisse

Die Autoren bewerteten AutoQ 2.0 an zwei Klassen fortgeschrittener Quantenprogramme:

1. Repeat-Until-Success (RUS)-Algorithmen: Werden zur Erzeugung nicht-standardisierter Quantengatter verwendet (z. B. spezifische Unitätsoperatoren wie $(2X + \sqrt{2}Y + Z)/\sqrt{7}$).
   • Ergebnis: Alle RUS-Benchmarks wurden sofort verifiziert (0,0 s).
2. Schwache-Messung-basierte Grovers Suche: Eine Version von Grovers Algorithmus, die kein Vorwissen über die Anzahl der Lösungen erfordert.
   • Ergebnis: Das Werkzeug verifizierte Instanzen mit bis zu 100 Qubits (speziell 101 Qubits in der Tabelle) erfolgreich in etwa 11 Sekunden (für den 101-Qubit-Fall) bis 20 Minuten (wie im Abstract für den 100-Qubit-Fall angegeben, obwohl die Tabelle 11 s für 101 Qubits zeigt; das Abstract bezieht sich wahrscheinlich auf eine spezifische Konfiguration oder beinhaltet die Einrichtungszeit). Die Verifikationszeit skaliert vernünftig mit der Anzahl der Qubits und Gatter.

Die Experimente wurden auf einem Server mit einem AMD EPYC 7742-Prozessor und 1.152 GiB RAM durchgeführt.

5. Bedeutung und Behauptungen

Die Arbeit behauptet, dass AutoQ 2.0 derzeit das einzige Werkzeug ist, das in der Lage ist, Quantenprogramme mit einem so hohen Grad an Automatisierung zu verifizieren. Im Gegensatz zu bestehenden Werkzeugen, die auf Beweisassistenten angewiesen sind (was erheblichen menschlichen Aufwand erfordert) oder sich ausschließlich auf Schaltkreisäquivalenz konzentrieren, schließt AutoQ 2.0 die Lücke zwischen der Theorie der formalen Verifikation und der praktischen Quantenprogrammierung, indem es Kontrollfluss und Messung automatisch behandelt.

Die Autoren positionieren das Werkzeug als einen bedeutenden Schritt hin zur formalen Verifikation komplexer Quantenalgorithmen und zeigen auf, dass automatisierte deduktive Verifikation für Programme machbar ist, die nicht als einfache Quantenschaltkreise ausgedrückt werden können. Sie vermerken bescheiden, dass die aktuelle Implementierung nicht-verschachtelten Kontrollfluss und reine Zustände behandelt, während zukünftige Arbeiten darauf abzielen, die Generierung von Invarianten zu automatisieren und die Unterstützung auf gemischte Zustände zu erweitern, die aus komplexeren Schleifen entstehen.