Resumo Técnico: ConQEC – Teste Concolic para Implementações de Códigos de Correção de Erros Quânticos

1. Declaração do Problema

As implementações de Códigos de Correção de Erros Quânticos (QECC) funcionam como sistemas híbridos de controle-software onde síndromes medidas direcionam o despacho do decodificador, ações de recuperação e verificações lógicas. Embora as técnicas de verificação formal existentes possam provar obrigações matemáticas e o teste quântico geral possa expor falhas finais, os desenvolvedores carecem de um fluxo de trabalho de teste escalável que gere falhas concretas e explique onde um caminho de reparo de QECC diverge pela primeira vez da referência.

As abordagens atuais enfrentam duas limitações primárias:

1. Escalabilidade: O teste concolic quântico geral (ex: QCT) depende de modelos de restrição baseados em amplitudes. O rastreamento do espaço de estado quântico cresce exponencialmente com o número de qubits físicos, tornando esses métodos inviáveis para implementações modernas que envolvem milhares de qubits (ex: processador Condor da IBM).
2. Utilidade Diagnóstica: As ferramentas existentes frequentemente relatam apenas uma falha lógica final (passa/falha). Elas falham em fornecer uma "testemunha" (witness) reproduzível que isole o estágio específico do pipeline de reparo (extração de síndrome, decisão do decodificador ou ação de recuperação) onde a implementação divergiu do comportamento esperado.

2. Metodologia: O Framework ConQEC

O ConQEC é o primeiro framework de teste concolic projetado especificamente para implementações de QECC. Ele aborda as necessidades de escalabilidade e diagnóstico ao deslocar o foco do raciocínio de estado em nível de amplitude para restrições de caminho de reparo simbólico.

Princípios Fundamentais de Design

• Caminhos de Reparo FSDR (Falha–Síndrome–Decodificador–Recuperação): O ConQEC trata um teste não como um resultado final, mas como um caminho de execução em estágios. Um bug é aceito apenas após um "replay pareado" contra um contrato de referência produzir uma testemunha de estágio.
• Codificação Simbólica no Nível do Caminho de Reparo: Em vez de simular amplitudes quânticas, o ConQEC codifica simbolicamente:
  • Falhas de Pauli: Representadas como indicadores booleanos simbólicos ($\hat{f}_i$) para locais de injeção.
  • Predicados de Síndrome: Modelados como expressões de paridade afim ($s_c(\hat{f}) = \beta_c \oplus \bigoplus \hat{f}_i$) representando como as falhas invertem os bits de verificação.
  • Relações de Decodificador e Recuperação: Modelados como relações $D(\sigma, d)$ e $R(\sigma, d, r)$ mapeando síndromes para decisões e ações de recuperação.
• Replay Pareado: O framework gera uma falha de Pauli candidata via solver (SMT), então a executa concretamente tanto na implementação quanto em um contrato de referência. A cobertura e a aceitação do bug são creditadas apenas após este replay validar o efeito da falha e identificar o primeiro ponto de divergência.

O Loop Concolic

1. Geração Simbólica: O sistema constrói um modelo de restrição sobre o espaço de falhas legal e os predicados do caminho de reparo. Ele formula consultas para visar objetivos específicos (ex: alcançar uma síndrome específica, disparar um ramo de decodificador específico ou encontrar uma divergência entre a implementação e a referência).
2. Materialização de Candidato: Um solver fornece uma valoração para os indicadores de falha simbólicos, materializando uma falha de Pauli concreta (ex: $X@q_0$).
3. Validação Pareada: A falha concreta é reproduzida na implementação e na referência.
4. Construção de Testemunha: Se o replay revelar uma falha ($\omega = \text{FAIL}$) ou uma divergência de nível de estágio ($\delta \neq \perp$), o ConQEC constrói uma testemunha de bug FSDR. Esta testemunha inclui a falha injetada, a síndrome observada, a decisão do decodificador, a ação de recuperação, o resultado do oráculo e o estágio de divergência mais precoce.

Classificação de Bugs

O ConQEC localiza bugs em cinco classes específicas baseadas no estágio de divergência mais precoce:

1. Erro de extração de síndrome: Valores incorretos de check/detector.
2. Uso indevido do registrador de medição: Leituras de registro obsoletas ou trocadas.
3. Erro de despacho do decodificador: Síndrome correta mapeada para o braço errado do decodificador.
4. Síndrome não tratada: Síndrome alcançável sem um manipulador (handler).
5. Violação de contrato de recuperação: Decisão de decodificador correta, mas aplicação de recuperação incorreta ou falha na verificação final.

3. Principais Contribuições

1. Framework ConQEC: O primeiro framework de teste concolic para implementações de QECC, modelando testes como caminhos de reparo FSDR e retornando testemunhas baseadas em replay.
2. Geração de Caminho de Reparo Escalável: Um método de codificação simbólica que evita o raciocínio exponencial de nível de amplitude, permitindo a geração de falhas direcionadas para QECCs com até milhares de qubits.
3. Avaliação Empírica: Avaliação abrangente em famílias de QECC geradas em nível de código-fonte (Repetição, Superfície/Tórico, Tanner/LDPC, Códigos de Cor) e artefatos públicos (Tesseract, PyMatching), demonstrando a capacidade de detectar bugs semeados e fornecer testemunhas de localização de falhas em escala.

4. Resultados Experimentais

A avaliação foi conduzida em um servidor com 128 núcleos e 2,0 TiB de memória, usando o backend QSE e o solver Z3.

• Localização de Falhas (RQ1): O ConQEC localizou com sucesso bugs semeados em 195/195 casos experimentais (através de 13 configurações e 5 classes de bugs) com um orçamento de geração $B=4$. Em contraste, o teste de falha aleatória encontrou apenas ~15,7/195 testemunhas no mesmo orçamento, e a busca de ordem de ramo genérica encontrou 0. O ConQEC localizou falhas em sistemas com até 1.500 qubits físicos.
• Cobertura Semântica (RQ2): O ConQEC superou significativamente o teste aleatório na cobertura de obrigações de estabilizador "difíceis" (ex: cobertura de máscara de par onde duas falhas se cancelam). Para $n=1000$ qubits, o ConQEC cobriu ~49,9% das obrigações de máscara de par com um orçamento $B=500$, enquanto o teste aleatório cobriu apenas 0,10%.
• Escala e Custo (RQ3): O framework escalou para campanhas de nível de código-fonte com 3.000 qubits (Código de Repetição) e distância $d=41$ (Código de Superfície). O principal gargalo foi a geração de consulta/resolução de SMT, não a fase de replay pareado, que representou menos de 0,004% do tempo de execução (wall-clock time).
• Aplicabilidade a Artefatos Públicos (RQ4): O ConQEC conseguiu instanciar evidências baseadas em replay em artefatos públicos, incluindo o corpus Tesseract Stim e testes de regressão do PyMatching, identificando desacordos lógicos e regressões de fronteira de decodificador.

5. Significância e Alegações

O artigo afirma que o ConQEC fornece um fluxo de trabalho de teste escalável e diagnóstico para implementações de QECC que as ferramentas de verificação formal e testes quânticos gerais não podem oferecer.

• Depuração Centrada no Desenvolvedor: Ao retornar uma testemunha de replay FSDR, o ConQEC transforma uma falha de "caixa preta" em um artefato de depuração localizado, identificando exatamente onde o caminho de reparo divergiu (ex: "O decodificador escolheu $X@q_1$ em vez de $X@q_0$ para a síndrome $(1,0)$").
• Escalabilidade: Ao abstrair o rastreamento de estado de nível de amplitude e focar na lógica discreta de decodificação de síndrome e recuperação, o ConQEC preenche a lacuna entre a verificação teórica de QECC e o teste de software prático para sistemas de mil de qubits.
• Complementaridade: Os autores posicionam o ConQEC como complementar às ferramentas de verificação formal (como QSE ou QECV). Enquanto as ferramentas formais provam a correção, o ConQEC gera casos de teste concretos e evidências de depuração para bugs de implementação, operando dentro de um framework de teste "orçado" adequado para pilhas de software de grande escala.

O artigo mantém um escopo modesto, reconhecendo que seu modelo simbólico depende de predicados expostos e que objetivos de transição exigem relações explícitas de decodificador/recuperação. Ele não pretende resolver todos os problemas de teste de software quântico, mas visa especificamente os desafios únicos dos pipelines de reparo de QECC.