Resumo Técnico: A Verificação de Dados é o Futuro dos Copilotos de Computação Quântica

Declaração do Problema

A geração e compilação de programas quânticos exigem um nível de precisão que conflita com o raciocínio estatístico inerente aos Grandes Modelos de Linguagem (LLMs). Tarefas de computação quântica envolvem a travessia de múltiplas camadas de abstração (desde descrições de circuitos de alto nível até arranjos de portas de baixo nível) e a adesão a rigorosas restrições matemáticas (ex: unitariedade, topologia de hardware, fidelidade de porta). Diferente de tarefas de linguagem natural onde erros podem ser tolerados ou suavizados, a geração de programas quânticos demanda tolerância zero para erros; uma única sequência de portas inválida viola leis físicas fundamentais.

As abordagens atuais baseadas em LLM enfrentam três limitações críticas:

1. Soluções Inviáveis: Sem verificação de dados, soluções inviáveis são matematicamente inevitáveis devido à natureza estatística dos LLMs, independentemente da escala do modelo.
2. Escassez de Dados: Conjuntos de dados quânticos abrangentes e verificados são extremamente difíceis de gerar. Datasets existentes (ex: QDataSet) exigiram meses de tempo de HPC para cobrir apenas sistemas pequenos (1-2 qubits).
3. Restrições do Espaço de Busca: O subespaço válido de circuitos quânticos é exponencialmente pequeno em comparação ao total do espaço de design, limitado pela unitariedade e restrições de hardware. As arquiteturas de LLM atuais não conseguem fornecer internamente os mecanismos de verificação necessários para navegar neste espaço.

Metodologia e Estrutura

O artigo propõe uma mudança de paradigma do "apenas inferência" ou "filtragem pós-hoc" para arquiteturas de verificação primeiro (verification-first). Os autores definem três posições centrais apoiadas por argumentos teóricos e experimentos preliminares:

1. Verificação de Dados como um Requisito Mínimo (P1)

Os autores argumentam que os dados de treinamento devem ser formalmente verificados antes da inclusão no conjunto de treinamento.

• Conceito: Um "modelo ciente de verificação" (Verification-aware model) é treinado exclusivamente em dados onde cada exemplo satisfaz restrições de correção específicas do domínio (ex: provadas via provadores de teoremas automatizados como Lean ou Z3).
• Racional: Treinar em dados não verificados (ex: repositórios de código de baixa qualidade) constitui "envenenamento implícito de dados". Diferente da linguagem natural, onde volumes massivos de dados neutralizam o ruído, um único exemplo inválido em dados de circuitos quânticos viola a unitariedade, independentemente dos exemplos válidos ao redor. Isso leva a um fenômeno de "anti-escalonamento", onde mais dados não verificados amplificam erros em vez de diluí-los.
• Mecanismo: Datasets verificados permitem que os modelos internalizem restrições como estruturas aprendidas, em vez de aproximações estatísticas.

2. Restrições A Priori sobre Filtragem A Posteriori (P2)

A verificação deve restringir o processo de geração antes da saída, em vez de filtrar saídas após a geração.

• Racional: No design de circuitos quânticos, a fração de designs válidos diminui exponencialmente conforme o número de componentes (qubits/portas) aumenta. Para um espaço de design que cresce como $O(d^n)$, as restrições reduzem os designs válidos para $O(\delta^n)$ onde $\delta < d$.
• Consequência: Confiar em filtragem pós-hoc (gerar muitos candidatos e rejeitar os inválidos) acarreta custos computacionais exponenciais e possui uma probabilidade de sucesso vanishingly baixa (tendendo a zero). A verificação deve ser incorporada como um primitivo arquitetônico para evitar caminhos inválidos durante a geração de tokens.

3. Paradigma de Verificação Primeiro para AI4Research (P3)

Os autores defendem a extensão desta abordagem de verificação primeiro para outros domínios científicos governados por leis físicas ou axiomas matemáticos (ex: descoberta de fármacos, ciência dos materiais, design de engenharia).

• Conceito: Estes domínios compartilham problemas de "abstração vazante" (leaky abstraction) e "não decomponibilidade", onde escolhas localmente ótimas não garantem a otimalidade global. Arquiteturas cientes de verificação são necessárias para lidar com essas restrições rígidas.

Resultados Experimentais

Para substanciar a Posição 1, os autores conduziram uma avaliação utilizando um dataset derivado de corpora de circuitos MAJ/UMA (Majority/UnMajority-and-Add) verificados.

• Configuração: 34 LLMs publicamente disponíveis (variando de 270M a 120B de parâmetros) foram testados em 70.000 questões de múltipla escolha sobre otimização de somador quântico (2 a 8 qubits). O ground truth era o circuito com o menor score ponderado de contagem de Toffoli, profundidade e total de portas.
• Acurácia: Modelos treinados ou ajustados com conhecimento de verificação (ex: gemma3:12b, gpt-oss:120b) alcançaram acurácia entre 0,60 e 0,79. Em contraste, modelos genéricos sem consciência de verificação orbitaram próximo à linha de base aleatória (0,21–0,29).
• Calibragem: Modelos cientes de verificação demonstraram quantificação de incerteza superior. Modelos gpt-oss atribuíram 60–80% de confiança às respostas corretas, enquanto modelos gemma3 permaneceram na faixa de 20–35%.
• Modos de Falha: Vários modelos (ex: mixtral:8x7b, variantes deepseek-r1) pontuaram abaixo da linha de base aleatória devido a saídas malformadas (recusas verbosas ou explicações em vez de respostas de letra única), reforçando que, sem treinamento de verificação, os modelos não conseguem engajar de forma confiável em tarefas formalmente restritas.
• Análise do Espaço de Busca: Os autores geraram um dataset de 200.000 designs de somadores verificados. Notaram que, embora o total de arranjos de portas possíveis para módulos MAJ/UMA através das profundidades 3–6 exceda 148 trilhões de configurações, a verificação formal identificou apenas ~200.000 designs válidos (uma razão de $\approx 10^{-9}$), ilustrando a natureza proibitiva da filtragem pós-hoc.

Principais Contribuições

1. Definição Formal de Modelos Cientes de Verificação: Distinguindo entre modelos treinados em restrições verificadas versus aqueles treinados em repositórios de código não verificados.
2. Três Posições Centrais: Estabelecendo que a verificação de dados é um requisito mínimo, que as restrições devem ser a priori, e que este paradigma é essencial para a IA científica.
3. Evidência Empírica: Fornecendo dados quantitativos mostrando que, sem verificação de dados, os LLMs falham em atingir alta acurácia ou calibragem adequada em tarefas de otimização quântica, independentemente da escala de parâmetros.
4. Identificação de "Abstração Vazante": Destacando como a geração de programas quânticos exige a fusão de níveis de abstração (ex: design de módulo vs. decomposição de portas) de formas que tornam a otimização local insuficiente para a correção global.

Significância e Direções Futuras

O artigo argumenta que, para a IA ser viável em domínios governados por leis físicas ou matemáticas estritas, a verificação deve ser elevada de um "pensamento posterior" para uma "fundação arquitetônica".

Os autores propõem duas direções específicas de pesquisa futura:

• FD1 (Arquitetura): Arquiteturas de copiloto quântico devem integrar verificação formal (ex: Teoria de Satisfatibilidade de Modos ou especificações simbólicas) diretamente no loop de geração de tokens do LLM, transformando a verificação de um filtro binário em um guia de exploração estruturado.
• FD2 (Benchmarks): A comunidade precisa de benchmarks ricos em restrições pareados com oráculos de verificação executáveis. Estes devem se estender além de somadores simples para incluir multiplicação modular, transformadas de Fourier quânticas e roteamento específico de hardware, permitindo padrões reproduzíveis para comparação entre sistemas.

O artigo conclui que, embora os argumentos foquem em computação quântica, os princípios aplicam-se amplamente a qualquer campo onde a correção é binária, soluções válidas ocupam um subespaço exponencialmente pequeno e métodos de verificação formal existem.