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

Résumé Technique : Le côté Vérificateur du Décodage par Fenêtre Spéculative

Énoncé du Problème
La correction d'erreurs quantiques (QEC) en temps réel fait face à un goulot d'étranglement critique de latence. Les cycles de syndromes arrivent selon une cadence matérielle fixe (environ une microseconde pour les qubits supraconducteurs), mais les décodeurs ne parviennent souvent pas à suivre le rythme, permettant aux files d'attente de syndromes de croître jusqu'à ce que la décohérence détruise l'état logique. Bien que le « décodage par fenêtre » (window decoding) divise l'historique des syndromes en blocs parallélisables, les fenêtres adjacentes restent sériellement dépendantes : la correction engagée dans une fenêtre détermine le problème de décodage pour la suivante. Des travaux antérieurs, spécifiquement SWIPER et ARTERY, ont tenté de supprimer ce goulot d'étrance sériel en utilisant la spéculation : prédire les décisions transfrontalières pour permettre aux fenêtres en aval de démarrer plus tôt, avec un décodage complet s'exécutant de manière paresseuse pour vérifier. Cependant, ces systèmes n'ont implémenté que la moitié prédictive (atteignant environ 90 % de précision) et manquaient d'un côté vérificateur rigoureux. Par conséquent, quatre questions fondamentales restaient sans réponse : la limite théorique de la précision de la prédiction, le « rayon d'impact » (blast radius) maximal d'une erreur de prédiction, si la spéculation vaut le risque compte tenu de ces limites, et si la boucle complète prédire-vérifier-récupérer cache réellement la latence et permet une récupération correcte sur un vrai décodeur.

Méthodologie
Les auteurs ont construit un harnais SWIPER reconstruit en utilisant Stim (code de surface tourné) et PyMatching (appariement parfait de poids minimum, MWPM) pour répondre à ces questions. La méthodologie se déroule en quatre étapes :

1. Encadrement de la Prédictibilité : Au lieu de s'appuyer sur un seul prédicteur heuristique, les auteurs ont établi une borne supérieure (« plafond ») sur la précision réalisable en utilisant un décodeur MWPM local de rayon $R$. Ce décodeur utilise uniquement les données de syndrome dans un rayon de $R$ cycles autour de la coupure de la frontière, traitant les frontières ouvertes exactement comme un décodeur de fenêtre le ferait. Cela encadre la limite théorique de ce que tout prédicteur peut accomplir avec des informations locales.
2. Évaluation et Falsification du Rayon d'Impact : Les auteurs ont modélisé la propagation d'une erreur de prédiction (bits de dépendance erronés) à travers une fenêtre. Ils ont d'abord établi une borne temporelle de pire cas en utilisant un noyau de probabilité vérifié par machine dans Lean 4, conditionnellement à une hypothèse de réduction stipulant qu'une erreur de prédiction nécessite qu'un chemin défectueux se propage. Ils ont ensuite testé rigoureusement cette hypothèse « coup par coup » contre un adversaire à bit unique tranchant pour falsifier le mécanisme de réduction.
3. Dérivation de Passage de Compilateur : En utilisant la prédictibilité et le rayon d'impact mesurés, un passage de compilateur a été développé pour dériver une politique de redémarrage optimale. Ce passage opère sur un graphe de dépendance de fenêtre abstrait, annotant les frontières avec des drapeaux de spéculation basés sur un modèle de coût : $coût = prédictibilité \times marge\_de\_manœuvre - rayon\_d'impact$.
4. Exécution au Runtime et Agnosticisme du Décodeur : Un exécuteur de runtime a été construit pour faire fonctionner la boucle complète prédire-vérifier-récupérer sur le harnais. Pour déterminer quels résultats sont intrinsèques au cadre de spéculation versus spécifiques au décodeur MWPM, les auteurs ont réexécuté des expériences clés en utilisant un second décodeur algorithmiquement distinct : le décodeur Union-Find (croissance de clusters non pondérés).

Contributions Clés et Résultats

• La Prédictibilité est Locale et Presque Saturée : La décision transfrontalière est déterminée par environ trois cycles de syndrome de chaque côté de la coupure. Un MWPM local avec un champ de réception de $R=3$ atteint environ 0,999 de précision, indiquant que la précision d'environ 90 % des prédicteurs précédents (SWIPER) n'était pas une limite fondamentale mais laissait une petite marge diffuse (0,019 à 0,063 selon la distance du code).
• Le Rayon d'Impact est de Un (Confinement Temporel) : La probabilité de pire cas qu'une erreur de prédiction se propage à la fenêtre suivante décroît exponentiellement avec la largeur d'engagement $W$. À la largeur standard ($W=d$), la probabilité de propagation est de plusieurs ordres de grandeur inférieure au taux d'erreur logique (ex: $10^{-7}$ contre $10^{-5}$ pour $d=7$). Cela établit que le rayon d'impact temporel est effectivement de un, signifiant que la spéculation n'ajoute aucun plancher d'erreur.
• Réfutation du Mécanisme de Chemin Défectueux : La preuve Lean 4 était conditionnelle à l'hypothèse qu'une propagation nécessite un « chemin défectueux » (une chaîne d'erreurs reliant le basculement à la coupure). La falsification coup par coup a montré que cette hypothèse est fausse : la propagation se produit couramment sans aucun chemin défectueux à proximité du bit basculé. Le véritable mécanisme est un ré-appariement de poids global (global minimum-weight re-pairing), où le décodeur réachemine un défaut existant vers le bit basculé car cela est moins coûteux qu'une absorption locale. Ce mécanisme est piloté par la dégénérescence, particulièrement à un bruit proche du seuil.
• Récupération Exacte et Dissimulation de la Latence : L'exécuteur de runtime a confirmé que la boucle prédire-vérifier-récupérer est exacte. Sur une chaîne de 16 fenêtres, le système atteint une accélération d'environ 16,00, le maximum théorique, éliminant le blocage de la chaîne d'engagement sérielle avec une pénalité de redémarrage négligeable ($\sim 10^{-5}$).
• Phénoménologie Structurelle Agnostique au Décodeur : Bien que les magnitudes de précision absolue et le mécanisme spécifique de « poids minimum » soient propres au décodeur, les conclusions structurelles sont robustes. Le décodeur Union-Find a confirmé que la décision de coupure est locale (saturant à $R=3$) et que la propagation sans chemin défectueux persiste, validant la phénoménologie structurelle de l'enveloppe de spéculation.

Signification et Revendications
Le document affirme avoir construit le « côté vérificateur » manquant de la décodage par fenêtre spéculative, transformant une heuristique empirique en un système rigoureusement borné. La signification réside dans :

1. La Preuve de Sécurité : Démontrer que la spéculation n'introduit pas de plancher d'erreur, car les erreurs de prédiction sont contenues dans un rayon de un avec des bornes de probabilité vérifiées par machine.
2. La Clarification du Mécanisme : Remplacer le modèle intuitif de « chemin défectueux » par le mécanisme correct de « ré-appariement global », expliquant pourquoi la propagation se produit même sans chaînes d'erreurs directes.
3. L'Automatisation : Fournir un passage de compilateur qui dérive des politiques de redémarrage à partir de mesures plutôt que de les coder en dur, rendant l'approche portable à travers différentes configurations de code et piles de contrôle.
4. La Réutilisabilité : Établir l'enveloppe prédire-vérifier-récupérer comme une couche réutilisable qui se situe au-dessus de n'importe quel décodeur, découplant la logique de spéculation de l'algorithme de décodage spécifique.

Les auteurs restent modestes quant à la portée, notant que les chiffres d'accélération sont basés sur une carte linéaire analytique (car le pipeline complet SWIPER-SIM n'est pas public) et que la formalisation de la borne de poids d'appariement (source de la décroissance exponentielle) reste un objectif pour des travaux futurs. Le travail est présenté comme une couche fondamentale pour la QEC en temps réel, validée sur un harnais reconstruit avec un code reproductible et des preuves vérifiées par machine.