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

Technische Samenvatting: De Verifier-zijde van Speculatieve Window Decoding

Probleemstelling
Real-time kwantumfoutcorrectie (QEC) kampt met een kritieke latentie-bottleneck. Syndroomrondes arriveren op een vaste hardware-cadans (ongeveer één microseconde voor supergeleidende qubits), maar decoders kunnen vaak de snelheid niet bijhouden, waardoor syndroom-backlogs groeien totdat decoherentie de logische staat vernietigt. Hoewel "window decoding" de syndroomgeschiedenis in paralleliseerbare brokken splitst, blijven aangrenzende vensters serieel afhankelijk: de correctie die in één venster wordt vastgelegd (committed), bepaalt het decodeerprobleem voor het volgende. Eerdere werken, specifiek SWIPER en ARTERY, probeerden deze seriële bottleneck te verwijderen door middel van speculatie: het voorspellen van grensoverschrijdende beslissingen om downstream vensters vervroegd te laten starten, waarbij de volledige decoding vertraagd (lazily) wordt uitgevoerd om te verifiëren. Deze systemen implementeerden echter alleen de voorspeller-zijde (met een nauwkeurigheid van ~90%) en misten een rigoureuze verifier-zijde. Bijgevolg bleven vier fundamentele vragen onbeantwoord: de theoretische limiet van de voorspellingsnauwkeurigheid, de slechtst denkbare "blast radius" van een misvoorspelling, of speculatie de risico's waard is gezien deze limieten, en of de volledige predict-verify-recover lus daadwerkelijk latentie verbergt en correct herstelt op een echte decoder.

Methodologie
De auteurs hebben een gereconstrueerde SWIPER-harness geconstrueerd met behulp van Stim (rotated surface code) en PyMatching (minimum-weight perfect matching, MWPM) om deze vragen te beantwoorden. De methodologie verloopt in vier fasen:

1. Predictability Bracketing: In plaats van te vertrouwen op een enkele heuristische voorspeller, hebben de auteurs een bovengrens ("ceiling") vastgesteld op de haalbare nauwkeurigheid met behulp van een radius-$R$ lokale MWPM-decoder. Deze decoder gebruikt enkel syndroomgegevens binnen $R$ rondes van de grens snede (boundary cut), waarbij open grenzen exact behandeld worden zoals een window decoder dat zou doen. Dit kader de theoretische limiet in van wat een voorspeller kan bereiken met lokale informatie.
2. Blast Radius Bounding en Falsificatie: De auteurs modelleerden de propagatie van een misvoorspelling (foutieve dependency bits) door een venster. Eerst stelden zij een worst-case temporele grens vast met behulp van een in Lean 4 machinaal gecontroleerde probabilistische kern, onder conditie van een reductiehypothese die stelt dat een misvoorspelling een foutief pad vereist om te propageren. Vervolgens testten zij deze hypothese rigoureus "shot-voor-shot" tegen een scherpe single-bit adversary om het reductiemechanisme te falsificeren.
3. Compiler Pass Afleiding: Met behulp van de gemeten voorspelbaarheid en blast radius werd een compiler pass ontwikkeld om een optimale restart-policy af te leiden. Deze pass opereert op een abstract window dependency graph en annoteert grenzen met speculatievlaggen op basis van een kostenmodel: $cost = predictability \times slack - blast\_radius$.
4. Runtime Executie en Decoder Agnosticisme: Er werd een runtime executor gebouwd om de volledige predict-verify-recover loop op de harness uit te voeren. Om te bepalen welke bevindingen intrinsiek zijn aan het speculatie-framework versus specifiek aan de MWPM-decoder, hebben de auteurs sleutelexperimenten opnieuw uitgevoerd met een tweede, algoritmisch verschillende decoder: de Union-Find decoder (unweighted cluster growth).

Belangrijkste Bijdragen en Resultaten

• Voorspelbaarheid is lokaal en bijna verzadigd: De grensoverschrijdende beslissing wordt bepaald door ongeveer drie rondes van syndroom aan elke zijde van de snede. Een lokale MWPM met een receptief veld van $R=3$ bereikt ~0,999 nauwkeurigheid, wat aangeeft dat de ~90% nauwkeurigheid van eerdere voorspellers (SWIPER) geen fundamentele limiet was, maar een kleine, diffuse marge liet (0,019 tot 0,063 afhankelijk van de code-afstand).
• Blast Radius is Eén (Temporele Inperking): De worst-case waarschijnlijkheid dat een misvoorspelling naar het volgende venster propageert, neemt exponentieel af met de commit-breedte $W$. Bij de standaard breedte ($W=d$) is de propagatiewaarschijnlijkheid orden van grootte lager dan de logische foutenrate (bijv. $10^{-7}$ vs $10^{-5}$ bij $d=7$). Dit stelt vast dat de temporele blast radius effectief één is, wat betekent dat speculatie geen foutenvloer (error floor) toevoegt.
• Weerlegging van het Faulty-Path Mechanisme: Het Lean 4-bewijs was conditioneel op de hypothese dat propagatie een "foutief pad" vereist (een keten van fouten die de flip verbindt met de snede). Shot-voor-shot falsificatie toonde aan dat deze hypothese onjuist is: propagatie vindt routinematig plaats zonder enig foutief pad nabij de geflipte bit. Het werkelijke mechanisme is een globale minimum-weight re-pairing, waarbij de decoder een bestaand defect herrouteert naar de geflipte bit omdat dit goedkoper is dan lokale absorptie. Dit mechanisme wordt gedreven door degeneratie, met name bij ruis nabij de drempelwaarde.
• Exact Herstel en Latentieverbruik: De runtime executor bevestigde dat de predict-verify-recover loop exact herstelt. Op een keten van 16 vensters bereikt het systeem een versnelling van ~16,00, wat de seriële commit-keten stall volledig wegneemt met een verwaarloosbare restart-penalty ($\sim 10^{-5}$).
• Decoder-Agnostische Structurele Fenomenologie: Hoewel de absolute nauwkeurigheidsmarges en het specifieke "min-weight" mechanisme decoder-specifiek zijn, zijn de structurele bevindingen robuust. De Union-Find decoder bevestigde dat de cut-beslissing lokaal is (verzadiging bij $R=3$) en dat propagatie zonder een faulty path persisteert, wat de structurele fenomenologie van de speculatie-wrapper valideert.

Betekenis en Claims
Het artikel claimt de ontbrekende "verifier-zijde" van speculatieve window decoding te hebben gebouwd, waardoor het is getransformeerd van een empirische heuristiek naar een rigoureus begrensde systematiek. De betekenis ligt in:

1. Bewijzen van Veiligheid: Het aantonen dat speculatie geen foutenvloer introduceert, aangezien misvoorspellingen beperkt blijven tot een radius van één met machinaal gecontroleerde waarschijnlijkheidsgrenzen.
2. Verheldering van het Mechanisme: Het vervangen van het intuïtieve "faulty path" model door het correcte "global re-pairing" mechanisme, wat verklaart waarom propagatie plaatsvindt zelfs zonder directe foutenketens.
3. Mogelijk maken van Automatisering: Het bieden van een compiler pass die restart-policies afleidt uit gemeten waarden in plaats van ze hard te coderen, wat de aanpak draagbaar maakt over verschillende code-layouts en control stacks.
4. Herbruikbaarheid: Het vestigen van de predict-verify-recover wrapper als een herbruikbare laag die boven elke decoder staat, waardoor de speculatie-logica wordt ontkoppeld van het specifieke decoding-algoritme.

De auteurs blijven bescheiden over de reikwijdte en merken op dat de versnellingscijfers gebaseerd zijn op een analytische lineaire-keten kaart (aangezien de volledige SWIPER-SIM pipeline niet publiek is) en dat de formalisering van de matching-weight bound (de bron van de exponentiële afname) een doel voor toekomstig werk blijft. Het werk wordt gepresenteerd als een fundamentele laag voor real-time QEC, gevalideerd op een gereconstrueerde harness met reproduceerbare code en machinaal gecontroleerde bewijzen.