The verifier side of speculative window decoding: a predictability bracket, a machine-checked blast-radius bound, and a decoder-agnostic recover loop

Technisches Resümee: Die Verifizierungsseite der spekulativen Fensterdekodierung

Problemstellung
Die Quantenfehlerkorrektur (QEC) in Echtzeit steht vor einem kritischen Latenzengpass. Syndromrunden treffen in einem festen Hardware-Takt ein (etwa eine Mikrosekunde bei supraleitenden Qubits), aber Dekodierer können oft nicht Schritt halten, wodurch sich Syndrom-Rückstände aufbauen können, bis die Dekohärenz den logischen Zustand zerstört. Während „Fensterdekodierung“ (Window Decoding) die Syndromhistorie in parallelisierbare Stücke aufteilt, bleiben benachbarte Fenster seriell abhängig: Die in einem Fenster vorgenommene Korrektur bestimmt das Dekodierungsproblem für das nächste. Vorherige Arbeiten, insbesondere SWIPER und ARTERY, versuchten, diesen seriellen Engpass durch Spekulation zu beseitigen: Vorhersage von grenzüberschreitenden Entscheidungen, um nachfolgende Fenster vorzeitig starten zu lassen, während die vollständige Dekodierung verzögert zur Verifizierung läuft. Diese Systeme implementierten jedoch nur die Prädiktor-Hälfte (erreichten ~90 % Genauigkeit) und ließen eine rigorose Verifizierungsseite vermissen. Infolgedessen blieben vier fundamentale Fragen unbeantwortt: das theoretische Limit der Vorhersagegenauigkeit, der Worst-Case-„Ausbreitungsradius“ (Blast Radius) einer Fehlprognose, ob Spekulation angesichts dieser Grenzen das Risiko wert ist, und ob der vollständige Predict-Verify-Recover-Zyklus tatsächlich Latenz verbirgt und auf einem echten Dekodierer korrekt regeneriert.

Methodik
Die Autoren konstruierten einen rekonstruierten SWIPER-Harness unter Verwendung von Stim (rotierte Oberflächen-Code) und PyMatching (Minimum-Weight Perfect Matching, MWPM), um diese Fragen zu beantworten. Die Methodik gliedert sich in vier Stufen:

1. Vorhersagbarkeit-Eingrenzung (Predictability Bracketing): Anstatt sich auf einen einzelnen heuristischen Prädiktor zu verlassen, etablierten die Autoren eine obere Schranke („Ceiling“) für die erreichbare Genauigkeit mittels eines Radius-$R$ lokalen MWPM-Dekodierers. Dieser Dekodierer nutzt nur Syndromdaten innerhalb von $R$ Runden um den Schnitt der Grenze und behandelt offene Grenzen exakt wie ein Fensterdekodierer. Dies grenzt das theoretische Limit dessen ein, was ein Prädiktor angesichts lokaler Informationen erreichen kann.
2. Begrenzung und Falsifizierung des Ausbreitungsradius: Die Autoren modellierten die Ausbreitung einer Fehlprognose (falsche Abhängigkeitsbits) durch ein Fenster. Zuerst etablierten sie eine Worst-Case-Zeitgrenze mittels eines in Lean 4 maschinell geprüften Wahrscheinlichkeitskerns, bedingt auf eine Reduktionshypothese, wonach eine Fehlprognose einen fehlerhaften Pfad benötigt, um zu propagieren. Sie testeten diese Hypothese dann rigoros „Schuss für Schuss“ gegen einen scharfen Single-Bit-Adversary, um den Reduktionsmechanismus zu falsifizieren.
3. Ableitung des Compiler-Pass: Unter Verwendung der gemessenen Vorhersagbarkeit und des Ausbreitungsradius wurde ein Compiler-Pass entwickelt, um eine optimale Neustart-Policy abzuleiten. Dieser Pass operiert auf einem abstrakten Fenster-Abhängigkeitsgraphen und annotiert Grenzen mit Spekulations-Flags basierend auf einem Kostenmodell: $cost = predictability \times slack - blast\_radius$.
4. Laufzeitausführung und Dekodier-Agnostik: Ein Runtime-Executor wurde gebaut, um den vollständigen Predict-Verify-Recover-Zyklus auf dem Harness auszuführen. Um zu bestimmen, welche Erkenntnisse intrinsisch zum Spekulations-Framework gehören und welche spezifisch für den MWPM-Dekodierer sind, führten die Autoren Schlüsselexperimente mit einem zweiten, algorithmisch unterschiedlichen Dekodierer durch: dem Union-Find-Dekodierer (ungewichtetes Clusterwachstum).

Wesentliche Beiträge und Ergebnisse

• Vorhersagbarkeit ist lokal und nahezu gesättigt: Die grenzüberschreitende Entscheidung wird durch etwa drei Runden der Syndromdaten auf jeder Seite des Schnitts bestimmt. Ein lokaler MWPM mit einem Rezeptionsfeld von $R=3$ erreicht eine Genauigkeit von ~0,999, was darauf hindeutet, dass die ~90 % Genauigkeit früherer Prädiktoren (SWWEIPER) kein fundamentales Limit waren, sondern einen kleinen, diffusen Spielraum (0,019 bis 0,063 je nach Code-Distanz) ließen.
• Ausbreitungsradius ist Eins (Temporale Begrenzung): Die Wahrscheinlichkeit, dass eine Fehlprognose zum nächsten Fenster propagiert, sinkt exponentiell mit der Commit-Breite $W$. Bei der Standardbreite ($W=d$) liegt die Propagationswahrscheinlichkeit um Größenordnungen unter der logischen Fehlerrate (z. B. $10^{-7}$ gegenüber $10^{-5}$ bei $d=7$). Dies etabliert, dass der temporale Ausbreitungsradius effektiv eins ist, was bedeutet, dass Spekulation keinen Fehler-Floor (Error Floor) hinzufügt.
• Widerlegung des „Faulty-Path“-Mechanismus: Der Lean 4-Beweis war konditional auf die Hypothese, dass eine Propagation einen „fehlerhaften Pfad“ (eine Kette von Fehlern, die den Flip mit dem Schnitt verbindet) erfordert. Die Schuss-für-Schuss-Falsifizierung zeigte, dass diese Hypothese falsch ist: Eine Propagation tritt routinemäßig auf, selbst ohne einen fehlerhaften Pfad nahe dem geflippten Bit. Der wahre Mechanismus ist ein globales Minimum-Weight Re-Pairing, bei dem der Dekodierer einen bestehenden Defekt zum geflippten Bit umleitet, da dies kostengünstiger ist als eine lokale Absorption. Dieser Mechanismus wird durch Degeneriertheit getrieben, insbesondere bei Rauschen nahe der Schwelle.
• Exakte Rekonstruktion und Latenzverdeckung: Der Runtime-Executor bestätigte, dass der Predict-Verify-Recover-Zyklus exakt rekonstruiert. Auf einer Kette von 16 Fenstern erreicht das System eine Beschleunigung von ~16,00, dem theoretischen Maximum, wodurch der serielle Commit-Ketten-Stau bis auf eine vernachlässigbare Neustart-Strafe ($\sim 10^{-5}$) entfernt wird.
• Dekodier-agnostische strukturelle Phänomenologie: Während die absoluten Genauigkeitsbeträge und der spezifische „Min-Weight“-Mechanismus dekodierspezifisch sind, sind die strukturellen Befunde robust. Der Union-Find-Dekodierer bestätigte, dass die Schnittentscheidung lokal ist (Sättigung bei $R=3$) und dass die Propagation ohne einen fehlerhaften Pfad fortbesteht, was die strukturelle Phänomenologie des Spekulations-Wrappers validiert.

Bedeutung und Ansprüche
Das Paper beansprucht, die fehlende „Verifizierungsseite“ der spekulativen Fensterdekodierung aufgebaut zu haben, wodurch sie von einer empirischen Heuristik in ein rigoros begrenztes System transformiert wurde. Die Bedeutung liegt in:

1. Nachweis der Sicherheit: Der Nachweis, dass Spekulation keinen Error Floor einführt, da Fehlprognosen mit einer maschinell geprüften Wahrscheinlichkeit auf einen Radius von eins begrenzt sind.
2. Klärung des Mechanismus: Ersetzung des intuitiven „Faulty-Path“-Modells durch den korrekten „Global Re-Pairing“-Mechanismus, der erklärt, warum Propagation auch ohne direkte Fehlerketten stattfindet.
3. Ermöglichung von Automatisierung: Bereitstellung eines Compiler-Pass, der Neustart-Policies aus gemessenen Werten statt aus Hardcodierung ableitet, was den Ansatz über verschiedene Code-Layouts und Control-Stacks hinweg portabel macht.
4. Wiederverwendbarkeit: Etablierung des Predict-Verify-Recover-Wrappers als wiederverwendbare Schicht, die über jedem Dekodierer sitzt und die Spekulationslogik von dem spezifischen Dekodier-Algorithmus entkoppelt.

Die Autoren bleiben hinsichtlich des Umfangs bescheiden und merken an, dass die Beschleunigungszahlen auf einer analytischen linearen Ketten-Map basieren (da die vollständige SWIPER-SIM-Pipeline nicht öffentlich ist) und dass die Formalisierung der Matching-Weight-Schranke (die Quelle des exponentiellen Abfalls) ein Ziel für zukünftige Arbeiten bleibt. Die Arbeit wird als fundamentale Schicht für die Echtzeit-QEC präsentiert, validiert auf einem rekonstruierten Harness mit reproduzierbarem Code und maschinell geprüften Beweisen.