Resumo Técnico: AutoQ 2.0: Da Verificação de Circuitos Quânticos à Verificação de Programas Quânticos

1. Declaração do Problema

Programas quânticos estendem circuitos quânticos ao incorporar construções de fluxo de controle clássico, como ramificações e loops. Embora circuitos quânticos (o domínio do AutoQ 1.0) sejam suficientes para definir sequências estáticas de portas, algoritmos quânticos avançados — como algoritmos de Repetir-Até-Sucesso (RUS) e versões baseadas em medição fraca da busca de Grover — exigem controle dinâmico baseado em valores clássicos obtidos a partir de medições de qubits.

A verificação desses programas apresenta desafios significativos não presentes na verificação de apenas circuitos:

• Medição e Normalização: A medição colapsa estados quânticos e produz valores clássicos (0 ou 1) que dirigem o fluxo de controle. Esse processo frequentemente requer a normalização de amplitudes de probabilidade, o que complica o raciocínio formal.
• Raciocínio sobre Fluxo de Controle: Verificar loops e ramificações exige lidar com espaços de estados que evoluem com base nos resultados das medições, uma tarefa difícil para as ferramentas automatizadas existentes.
• Falta de Ferramentas Automatizadas: Embora existam ferramentas de verificação dedutiva para programas clássicos (por exemplo, Dafny, KeY) e algumas ferramentas quânticas (por exemplo, CoqQ, Qbricks), elas ou carecem de automação total ou exigem esforço manual substancial (por exemplo, fornecer operadores hermitianos complexos ou realizar extensa busca de provas). Ferramentas automatizadas existentes frequentemente focam na equivalência de circuitos ou em programas parametrizados específicos, carecendo de suporte geral para fluxo de controle em programas quânticos.

2. Metodologia

O AutoQ 2.0 aborda esses desafios estendendo o quadro anterior de verificação de circuitos para suportar programas quânticos completos. A metodologia central baseia-se em Autômatos de Árvore Sincronizados por Nível (LSTAs) e em uma abordagem inovadora de teste de entailment.

2.1 Modelo Formal: Autômatos de Árvore Sincronizados por Nível (LSTAs)

A ferramenta representa conjuntos de estados quânticos (pré-condições, pós-condições e invariantes de loop) usando LSTAs.

• Estrutura: LSTAs são autômatos de árvore simbólicos projetados para codificar estados quânticos como árvores binárias perfeitas, onde os ramos representam estados da base computacional e as folhas representam amplitudes de probabilidade complexas.
• Sincronização: Uma característica fundamental dos LSTAs é o mecanismo de "escolha". Transições no mesmo nível da árvore devem compartilhar um conjunto de escolha comum. Isso permite que LSTAs representem compactamente estados emaranhados e superposições que autômatos de árvore padrão não conseguem, garantindo que apenas combinações válidas de ramos (aqueles que compartilham uma escolha) sejam geradas.
• Formato de Entrada: Os usuários especificam pré-condições, pós-condições e invariantes de loop como arquivos .lsta, que definem os autômatos que reconhecem os conjuntos de estados quânticos válidos.

2.2 Quadro de Verificação

O processo de verificação é automatizado e segue um estilo dedutivo:

1. Execução do Programa: A ferramenta executa portas quânticas (por exemplo, $H$, $CX$, $T$) no LSTA que representa a pré-condição.
2. Tratamento de Medição e Ramificações:
   • Quando ocorre uma medição $M_i = b$, o LSTA é dividido em duas cópias correspondentes aos resultados $b=0$ e $b=1$.
   • O algoritmo atualiza a árvore zerando as amplitudes de probabilidade dos ramos que não correspondem (por exemplo, se $M_1=0$, as amplitudes da subárvore $1$ sob $x_1$ são definidas como 0).
   • Crucialmente, a ferramenta não normaliza as amplitudes durante essa etapa. Ela preserva as amplitudes brutas para evitar aritmética complexa durante a execução, adiando as verificações de normalização para o teste final de entailment.
   • Instruções de ramificação são tratadas calculando os LSTAs resultantes para ambos os caminhos verdadeiro e falso e tomando sua união.
3. Tratamento de Loops:
   • Para loops while, o usuário deve fornecer um invariante de loop como um LSTA.
   • A ferramenta verifica que o invariante é indutivo: ele deve cobrir todos os estados alcançáveis antes do loop, e a execução do corpo do loop sobre o invariante (condicionado à continuação do loop) deve resultar em estados ainda cobertos pelo invariante.
   • Os estados na saída do loop são superestimados pelo invariante condicionado à terminação do loop.
4. Teste de Entailment (Até Escalonamento):
   • A etapa final verifica se o conjunto de estados alcançáveis (representado por um LSTA $R$) está incluído na pós-condição (LSTA $Q$).
   • Como os fatores de normalização foram ignorados durante a execução, a ferramenta utiliza uma relação especializada de entailment até escalonamento ($|=_{uts}$).
   • $A |=_{uts} B$ vale se cada árvore em $A$ for uma versão escalonada linearmente de uma árvore em $B$ (isto é, $T_A = r \cdot T_B$ para algum escalar não nulo $r$).
   • Essa verificação é realizada usando um algoritmo de busca em grafos que percorre os LSTAs nível por nível, mapeando estados e termos, e finalmente invocando um solver SMT (Z3) para verificar a existência de um fator de escalonamento $r$ que satisfaça as restrições globais.

3. Contribuições Principais

• Extensão para Programas Quânticos: O AutoQ 2.0 é a primeira ferramenta a fornecer verificação dedutiva automatizada para programas quânticos contendo loops e ramificações, indo além do escopo de apenas circuitos do AutoQ 1.0.
• Tratamento Automatizado de Medição: A ferramenta introduz algoritmos para dividir LSTAs com base nos resultados das medições e gerenciar os espaços de estados resultantes sem intervenção manual.
• Verificação sem Normalização: Ao projetar um teste de entailment que funciona com estados não normalizados (até escalonamento), a ferramenta evita a complexidade computacional de normalizar amplitudes durante a fase de execução, melhorando significativamente a eficiência.
• Invariantes Baseados em LSTA: O quadro utiliza LSTAs para representar invariantes de loop, permitindo a representação compacta de estados quânticos complexos necessários para algoritmos iterativos.
• Escalabilidade: A abordagem suporta a verificação de programas com um grande número de qubits (até 100 qubits nos benchmarks relatados) aproveitando a compactação dos LSTAs e a resolução eficiente de SMT.

4. Resultados Experimentais

Os autores avaliaram o AutoQ 2.0 em duas classes de programas quânticos avançados:

1. Algoritmos Repetir-Até-Sucesso (RUS): Usados para gerar portas quânticas não padrão (por exemplo, unitárias específicas como $(2X + \sqrt{2}Y + Z)/\sqrt{7}$).
   • Resultado: Todos os benchmarks RUS foram verificados instantaneamente (0,0s).
2. Busca de Grover Baseada em Medição Fraca: Uma versão do algoritmo de Grover que não requer conhecimento prévio do número de soluções.
   • Resultado: A ferramenta verificou com sucesso instâncias com até 100 qubits (especificamente, 101 qubits na tabela) em aproximadamente 11 segundos (para o caso de 101 qubits) a 20 minutos (conforme declarado no resumo para o caso de 100 qubits, embora a tabela mostre 11s para 101 qubits; o resumo provavelmente se refere a uma configuração específica ou inclui tempo de configuração). O tempo de verificação escala de forma razoável com o número de qubits e portas.

Os experimentos foram conduzidos em um servidor com um processador AMD EPYC 7742 e 1.152 GiB de RAM.

5. Significado e Alegações

O artigo afirma que o AutoQ 2.0 é atualmente a única ferramenta capaz de verificar programas quânticos com tal alto grau de automação. Diferentemente das ferramentas existentes que dependem de assistentes de prova (exigindo esforço humano significativo) ou focam exclusivamente na equivalência de circuitos, o AutoQ 2.0 preenche a lacuna entre a teoria da verificação formal e a programação quântica prática ao lidar com fluxo de controle e medição automaticamente.

Os autores posicionam a ferramenta como um passo significativo em direção à verificação formal de algoritmos quânticos complexos, demonstrando que a verificação dedutiva automatizada é viável para programas que não podem ser expressos como simples circuitos quânticos. Eles observam modestamente que, embora a implementação atual lide com fluxo de controle não aninhado e estados puros, trabalhos futuros visam automatizar a geração de invariantes e estender o suporte a estados mistos decorrentes de loops mais complexos.