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

Resumen Técnico: El Lado del Verificador de la Decodificación de Ventanas Especulativas

Planteamiento del Problema
La corrección de errores cuánticos (QEC) en tiempo real enfrenta un cuello de botella crítico de latencia. Las rondas de síndromes llegan con una cadencia de hardware fija (aproximadamente un microsegundo para qubits superconductores), pero los decodificadores a menudo no pueden mantener el ritmo, permitiendo que las acumulaciones de síndromes crezcan hasta que la decoherencia destruye el estado lógico. Aunque la "decodificación de ventanas" (window decoding) divide el historial de síndromes en fragmentos paralelizables, las ventanas adyacentes siguen siendo serialmente dependientes: la corrección comprometida en una ventana determina el problema de decodificación para la siguiente. Trabajos previos, específicamente SWIPER y ARTERY, intentaron eliminar este cuello de botella serial mediante la especulación: prediciendo decisiones transfronterizas para permitir que las ventanas posteriores comiencen temprano, con la decodificación completa ejecutándose de forma perezosa para verificar. Sin embargo, estos sistemas solo implementaron la mitad del predictor (alcanzando aproximadamente un 90% de precisión) y carecían de un lado de verificación riguroso. En consecuencia, cuatro preguntas fundamentales quedaron sin respuesta: el límite teórico de la precisión de la predicción, el "radio de explosión" (blast radius) del peor caso de una predicción errónea, si la especulación vale el riesgo dados esos límites, y si el bucle completo de predecir-verificar-recuperar realmente oculta la latencia y recupera correctamente en un decodificador real.

Metodología
Los autores construyeron un entorno de SWIPER reconstruido utilizando Stim (surface code rotado) y PyMatching (emparejamiento perfecto de peso mínimo, MWPM) para responder a estas preguntas. La metodología procede en cuatro etapas:

1. Acotación de la Predictibilidad: En lugar de depender de un único predictor heurístico, los autores establecieron un límite superior ("techo") de la precisión alcanzable utilizando un decodificador MWPM local de radio-$R$. Este decodificador utiliza únicamente datos de síndromes dentro de $R$ rondas del corte de la frontera, tratando las fronteras abiertas exactamente como lo haría un decodificador de ventana. Esto acota el límite teórico de lo que cualquier predictor puede lograr dada la información local.
2. Acotación y Falsificación del Radio de Explosión: Los autores modelaron la propagación de una predicción errónea (bits de dependencia incorrectos) a través de una ventana. Primero establecieron un límite temporal del peor caso utilizando un núcleo de probabilidad verificado por máquina en Lean 4, condicionado a una hipótesis de reducción donde una predicción errónea requiere que un camino defectuoso se propague. Luego probaron rigurosamente esta hipótesis "disparo a disparo" contra un adversario de un solo bit agudo para falsificar el mecanismo de reducción.
3. Derivación del Paso del Compilador: Utilizando la predictibilidad y el radio de explosión medidos, se desarrolló un paso de compilación para derivar una política de reinicio óptima. Este paso opera sobre un grafo de dependencia de ventana abstracto, anotando las fronteras con banderas de especulación basadas en un modelo de costo: $costo = predictibilidad \times holgura - radio\_de\_explosión$.
4. Ejecución en Tiempo de Ejecución y Agnóstico al Decodificador: Se construyó un ejecutor de tiempo de ejecución para correr el bucle completo de predecir-verificar-recuperar en el entorno. Para determinar qué hallazgos son intrínsecos al marco de especulación versus específicos del decodificador MWPM, los autores repitieron experimentos clave utilizando un segundo decodificador, algorítmicamente distinto: el decodificador Union-Find (crecimiento de clústeres sin pesos).

Contribuciones Clave y Resultados

• La Predictibilidad es Local y está Casi Saturada: La decisión transfronteriza está determinada por aproximadamente tres rondas de síndromes en cada lado del corte. Un MWPM local con un campo receptivo de $R=3$ logra una precisión de ~0.999, lo que indica que la precisión del ~90% de los predictores anteriores (SWIPER) no era un límite fundamental, sino que dejaba un margen pequeño y difuso (0.019 a 0.063 dependiendo de la distancia del código).
• El Radio de Explosión es Uno (Contención Temporal): La probabilidad del peor caso de que una predicción errónea se propague a la siguiente ventana decae exponencialmente con el ancho de compromiso $W$. Con el ancho estándar ($W=d$), la probabilidad de propagación es órdenes de magnitud inferior a la tasa de error lógico (por ejemplo, $10^{-7}$ vs $10^{-5}$ en $d=7$). Esto establece que el radio de explosión temporal es efectivamente uno, lo que significa que la especulación no añade un piso de error.
• Refutación del Mecanismo de Camino Defectuoso: La prueba de Lean 4 fue condicional a la hipótesis de que la propagación requiere un "camino defectuoso" (una cadena de errores que conecta el giro con el corte). La falsificación disparo a disparo mostró que esta hipótesis es falsa: la propagación ocurre rutinariamente sin ningún camino defectuoso cerca del bit volteado. El verdadero mecanismo es un re-emparejamiento de peso mínimo global, donde el decodificador re-enruta un defecto existente hacia el bit volteado porque es más barato que la absorción local. Este mecanismo es impulsado por la degeneración, particularmente ante un ruido cercano al umbral.
• Recuperación Exacta y Ocultación de Latencia: El ejecutor de tiempo de ejecución confirmó que el bucle de predecir-verificar-recuperar recupera exactamente. En una cadena de 16 ventanas, el sistema logra una aceleración de ~16.00, el máximo teórico, eliminando el estancamiento de la cadena de compromiso serial con una penalización de reinicio insignificante ($\sim 10^{-5}$).
• Fenomenología Estructural Agnóstica al Decodificador: Aunque las magnitudes de precisión absoluta y el mecanismo específico de "peso mínimo" son específicos del decodificador, los hallazgos estructurales son robustos. El decodificador Union-Find confirmó que la decisión del corte es local (saturando en $R=3$) y que la propagación sin un camino defectuoso persiste, validando la fenomenología estructural del envoltorio de especulación.

Significancia y Reivindicaciones
El artículo afirma haber construido el "lado del verificador" faltante de la decodificación de ventanas especulativa, transformándola de una heurística empírica en un sistema rigurosamente acotado. La significancia radica en:

1. Probar la Seguridad: Demostrar que la especulación no introduce un piso de error, ya que las predicciones erróneas se contienen en un radio de uno con límites de probabilidad verificados por máquina.
2. Clarificar el Mecanismo: Reemplazar el modelo intuitivo de "camino defectuoso" con el mecanismo correcto de "re-emparejamiento de peso mínimo", explicando por qué la propagación ocurre incluso sin cadenas de error directas.
3. Permitir la Automatización: Proporcionar un paso de compilación que deriva políticas de reinicio a partir de números medidos en lugar de codificarlos rígidamente, haciendo que el enfoque sea portable a través de diferentes disposiciones de código y pilas de control.
4. Reutilización: Establecer el envoltorio de predecir-verificar-recuperar como una capa reutilizable que se sitúa por encima de cualquier decodificador, desacoplando la lógica de especulación del algoritmo de decodificación específico.

Los autores mantienen la modestia respecto al alcance, señalando que las cifras de aceleración se basan en un mapa de cadena lineal analítico (ya que el pipeline SWIPER-SIM completo no es público) y que la formalización del límite de peso de emparejamiento (la fuente del decaimiento exponencial) sigue siendo un objetivo para trabajos futuros. El trabajo se presenta como una capa fundacional para la QEC en tiempo real, validada en un entorno reconstruido con código reproducible y pruebas verificadas por máquina.