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

Resumo Técnico: O Lado do Verificador da Decodificação de Janela Especulativa

Declaração do Problema
A correção de erros quânticos (QEC) em tempo real enfrenta um gargalo crítico de latência. As rodadas de síndrome chegam em um cadência de hardware fixa (aproximadamente um microssegundo para qubits supercondutores), mas os decodificadores muitas vezes não conseguem acompanhar o ritmo, permitindo que os acúmulos de síndrome cresçam até que a decoerência destrua o estado lógico. Embora a "decodificação de janela" (window decoding) divida o histórico de síndrome em blocos paralelizáveis, as janelas adjacentes permanecem serialmente dependentes: a correção comprometida em uma janela determina o problema de decodificação para a próxima. Trabalhos anteriores, especificamente SWIPER e ARTERY, tentaram remover esse gargalo serial usando especulação: prevendo decisões transfronteiriças para permitir que as janelas subsequentes comecem antecipadamente, com a decodificação completa rodando de forma preguiçosa (lazy) para verificar. No entanto, esses sistemas implementaram apenas a metade do preditor (alcançando ~90% de precisão) e careciam de um lado verificador rigoroso. Consequentemente, quatro questões fundamentais permaneceram sem resposta: o limite teórico de precisão da predição, o "raio de explosão" (blast radius) do pior caso de uma predição errônea, se a especulação vale o risco dados esses limites, e se o ciclo completo de predizer-verificar-recuperar realmente esconde a latência e recupera corretamente em um decodificador real.

Metodologia
Os autores construíram um harness SWIPER reconstruído usando Stim (código de superfície rotacionado) e PyMatching (correspondência perfeita de peso mínimo, MWPM) para responder a essas questões. A metodologia procede em quatro estágios:

1. Enquadramento da Preditibilidade: Em vez de depender de um único preditor heurístico, os autores estabeleceram um limite superior ("teto") de precisão alcançável usando um decodificador MWPM local de raio-$R$. Este decodificador utiliza apenas dados de síndrome dentro de $R$ rodadas do corte da fronteira, tratando as fronteiras abertas exatamente como um decodificador de janela faria. Isso enquadra o limite teórico do que qualquer preditor pode alcançar dado o conhecimento local.
2. Limitação do Raio de Explosão e Falsificação: Os autores modelaram a propagação de uma predição errônea (bits de dependência incorretos) através de uma janela. Primeiro, estabeleceram um limite temporal de pior caso usando um núcleo de probabilidade verificado por máquina em Lean 4, condicional a uma hipótese de redução de que uma predição errônea exige que um caminho defeituoso se propague. Em seguida, testaram rigorosamente essa hipótese "tiro a tiro" contra um adversário de bit único aguçado para falsificar o mecanismo de redução.
3. Derivação de Passagem de Compilador: Usando a preditibilidade e o raio de explosão medidos, uma passagem de compilador foi desenvolvida para derivar uma política de reinicialização ótima. Esta passagem opera em um grafo de dependência de janela abstrato, anotando fronteiras com flags de especulação baseadas em um modelo de custo: $custo = preditibilidade \times folga - raio\_de\_explosão$.
4. Execução em Tempo de Execução e Agnosticismo de Decodificador: Um executor de tempo de execução foi construído para rodar o ciclo completo de predizer-verificar-recuperar no harness. Para determinar quais descobertas são intrínsecas ao framework de especulação versus específicas ao decodificador MWPM, os autores repetiram experimentos chave usando um segundo decodificador, algoritmicamente distinto: o Union-Find (crescimento de cluster não ponderado).

Principais Contribuições e Resultados

• A Preditibilidade é Local e Quase Saturada: A decisão transfronteiriça é determinada por aproximadamente três rodadas de síndrome em cada lado do corte. Um MWPM local com um campo receptivo de $R=3$ alcança ~0,999 de precisão, indicando que a precisão de ~90% dos preditores anteriores (SWSWIPER) não era um limite fundamental, mas deixava uma margem pequena e difusa (0,019 a 0,063 dependendo da distância do código).
• O Raio de Explosão é Um (Contenção Temporal): A probabilidade de pior caso de uma predição errônea se propagar para a próxima janela decai exponencialmente com a largura de compromisso $W$. Na largura padrão ($W=d$), a probabilidade de propagação é ordens de magnitude inferior à taxa de erro lógico (ex: $10^{-7}$ vs $10^{-5}$ em $d=7$). Isso estabelece que o raio de explosão temporal é efetivamente um, o que significa que a especulação não introduz um piso de erro (error floor).
• Refutação do Mecanismo de Caminho Defituoso: A prova em Lean 4 era condicional à hipótese de que a propagação requer um "caminho defeituoso" (uma cadeia de erros conectando a inversão ao corte). A falsificação tiro a tiro mostrou que essa hipótese é falsa: a propagação ocorre rotineiramente sem qualquer caminho defeituoso próximo ao bit invertido. O verdadeiro mecanismo é um reemparelhamento de peso mínimo global, onde o decodificador redireciona um defeito existente para o bit invertido porque é mais barato do que a absorção local. Esse mecanismo é impulsionado pela degenerescência, particularmente em ruído próximo ao limiar.
• Recuperação Exata e Ocultação de Latência: O executor de tempo de execução confirmou que o ciclo predizer-verificar-recuperar recupera exatamente. Em uma cadeia de 16 janelas, o sistema alcança um ganho de velocidade de ~16,00 (o máximo teórico), removendo o travamento da cadeia de compromisso serial com uma penalidade de reinicialização negligível ($\sim 10^{-5}$).
• Fenomenologia Estrutural Agnóstica ao Decodificador: Embora as magnitudes de precisão absoluta e o mecanismo específico de "peso mínimo" sejam específicos do decodificador, as descobertas estruturais são robustas. O decodificador Union-Find confirmou que a decisão do corte é local (saturando em $R=3$) e que a propagação sem um caminho defeituoso persiste, validando a fenomenologia estrutural do wrapper de especulação.

Significância e Alegações
O artigo afirma ter construído o "lado do verificador" que faltava para a decodificação de janela especulativa, transformando-a de uma heurística empírica em um sistema rigorosamente limitado. A significância reside em:

1. Provando a Segurança: Demonstrar que a especulação não introduz um piso de erro, pois as predições errôneas são contidas em um raio de um com limites de probabilidade verificados por máquina.
2. Esclarecendo o Mecanismo: Substituir o modelo intuitivo de "caminho defeituoso" pelo correto mecanismo de "reemparelhamento global", explicando por que a propagação acontece mesmo sem cadeias de erro diretas.
3. Permitindo a Automação: Fornecer uma passagem de compilador que deriva políticas de reinicialização a partir de números medidos em vez de valores fixos, tornando a abordagem portátil entre diferentes layouts de código e pilhas de controle.
4. Reusabilidade: Estabelecer o wrapper predizer-verificar-recuperar como uma camada reutilizável que reside acima de qualquer decodificador, desacoplando a lógica de especulação do algoritmo de decodificação específico.

Os autores mantêm a modéstia quanto ao escopo, observando que os números de aceleração são baseados em um mapa analítico de cadeia linear (já que o pipeline completo SWIPER-SIM não é público) e que a formalização do limite de peso de correspondência (a fonte do decaimento exponencial) permanece um alvo para trabalhos futuros. O trabalho é apresentado como uma camada fundamental para QEC em tempo real, validada em um harness reconstruído com código reproduzível e provas verificadas por máquina.