An Agentic Formalization for Certified Quantum Neural Network Design

Resumo Técnico: Uma Formalização Agêntica para o Design de Redes Neurais Quânticas Certificadas

Definição do Problema
O Aprendizado de Máquina Quântica (QML) baseia-se em Redes Neurais Quânticas (QNNs), cuja utilidade depende do equilíbrio entre dois requisitos frequentemente conflitantes: expressividade (a capacidade de representar funções alvo complexas) e treinabilidade (a capacidade de evitar platôs áridos onde os gradientes desaparecem). As metodologias de design atuais dependem de argumentos matemáticos informais envolvendo processamento de sinal quântico (para expressividade) e teoria da álgebra de Lie dinâmica (DLA) (para treinabilidade). Esses argumentos frequentemente tratam entradas analíticas — como médias de conjunto, identidades de Schur e identificações de métricas — como "folclore" implícito. Consequentemente, a tensão entre expressividade e treinabilidade é difícil de resolver conclusivamente, pois as condições que melhoram a treinabilidade (ex: restringir a DLA) podem inadvertidamente tornar o modelo classicamente simulável, enquanto circuitos altamente expressivos podem sofrer de problemas de treinabilidade. Há uma carência de um framework unificado e verificável por máquina que exponha explicitamente as hipóteses necessárias para essas regras de design.

Metodologia
Os autores apresentam o Lean-QuantumAlg, uma formalização da teoria de QNN em Lean 4 utilizando as bibliotecas mathlib e cslib. O desenvolvimento opera sobre objetos concretos: circuitos parametrizados, suas perdas e suas álgebras de Lie dinâmicas, todos realizados como matrizes explícitas em $M_{2^n}(\mathbb{C})$.

A metodologia central envolve um loop de formalização agêntica:

1. Curadoria de Registro: Especialistas humanos curam um registro de alegações alvo com referências de origem.
2. Síntese por Agente: Um agente de IA decompõe as alegações, sintetiza provas em Lean e itera contra o kernel.
3. Verificação de Kernel: O kernel do Lean verifica cada passo de inferência. Crucialmente, qualquer entrada analítica que não possa ser provada imediatamente não é assumida, mas exposta como uma hipótese nomeada (ex: um campo em um feixe de hipóteses).
4. Auditoria e Fidelidade: Especialistas humanos revisam a "fidelidade da declaração" (garantindo que a declaração formal corresponda à alegação física pretendida) e verificam a "higiene dos axiomas" (garantindo que as provas dependam apenas de um núcleo clássico confiável, evitando axiomas não verificados).

Esta abordagem garante que cada teorema seja totalmente provado ou explicitamente condicional a entradas nomeadas, tornando a "fidelidade" das declarações finais auditável.

Principais Contribuições

1. Formalização da Expressividade (Seção 3):

   • Caracterizações Exatas: Caracterizações de "se e somente se" provadas para QNNs de um único qubit, identificando a classe realizável de polinômios trigonométricos (Teorema 3.1).
   • Processamento de Fase com Contagem de Recursos: Formalização do Processamento de Fase Quântica (QPP) com contagens exatas de recursos (2L consultas controladas, 4L+3 rotações) para transformar unitárias arbitrárias (Teorema 3.4).
   • Classes de Custo: Provou que as coordenadas de perda para ansatzes de múltiplas portas com geradores involutórios são polinômios trigonométricos de frequência um, permitindo gradientes exatos de deslocamento de parâmetro (Proposição 3.2).
   • Teto de Capacidade: Estabeleceu que o posto da Matriz de Informação de Fisher Quântica (QFIM) é limitado pela dimensão da DLA ($\text{rk } F \le \dim \mathfrak{g}$), definindo um teto de sobreparametrização (Teorema 3.6).

2. Formalização da Treinabilidade (Seção 4):

   • Lei da Variância de Perda de Soma Direta: Derivou a lei de variância $\text{Var}[\ell] = \sum_j \frac{P_{\mathfrak{g}_j}(\rho) P_{\mathfrak{g}_j}(O)}{\dim \mathfrak{g}_j}$ através de uma interface de segundo momento "descicularizada". Isso exigiu a construção de um mecanismo de unicidade de Casimir parametrizado para descarregar entradas para famílias de circuitos específicas (Teorema 4.3).
   • Feixes de Hipóteses: Introduziu feixes de hipóteses nomeados (ex: RagoneSecondMoment) que carregam explicitamente as entradas de "dois designs" e identidades de Schur necessárias para cálculos de variância.
   • Análise de Família: Aplicou a lei de variância a quatro famílias de circuitos:
     • Produto Local ($su(2)^{\oplus n}$): Provou não-concentração incondicional (variância $\approx 1/3$).
     • Matchgate ($so(2n)$): Provou não-concentração condicional com dimensão de DLA polinomial.
     • Universal ($su(2n)$) & Ortogonal ($so(2n)$): Provou concentração de perda exponencial condicional (platôs áridos) para $n \ge 3$, com descargas explícitas de identidade de Schur.
   • Correção de Argumentos Informais: A formalização revelou que a lei de variância de Casimir único falha para $so(4)$ (que é redutiva, não simples) e que $gl(2n)$ requer uma lei de dois componentes, corrigindo suposições na literatura informal.

3. O Teorema de Capstone (Seção 4.3):

   • Emparelhou a lei de variância-perda condicional com a reconstrução exata de perda em coordenadas de DLA (Algoritmo 1, $g$-sim). O teorema afirma que, se o observável estiver dentro da DLA, a perda pode ser exatamente reconstruída a partir de $\dim \mathfrak{g}$ valores de expectativa via matrizes de transferência, desde que as hipóteses da lei de variância sejam atendidas (Teorema 4.6).

Resultos e Verificação

• Escala de Desenvolvimento: A biblioteca contém 157 arquivos Lean, ~51.000 linhas de código, 2.403 teoremas/lémas e 62 endpoints principais verificados pelo kernel.
• Descoberta de Correções: O processo de formalização identificou oito correções específicas (rotuladas F1–F8) onde argumentos informais consumiam estrutura implicitamente. Exemplos notáveis incluem a dimensão do espaço invariante para $so(4)$ sendo 2 (não 1) e a necessidade de reverter listas de portas na evolução de Heisenberg para portas não comutativas.
• Higiene de Axiomas: Todos os 62 endpoints principais são verificados para depender apenas do núcleo de axiomas clássicos (excluindo Classical.choice e Quot.sound), garantindo confiança mecânica.

Significância e Alegações
O artigo afirma fornecer uma fundação verificável por máquina para a teoria de QNN. Sua significância reside em:

1. Auditabilidade: Ao expor cada entrada analítica como uma hipótese nomeada, o trabalho torna o escopo das regras de design explícito e auditável, distinguindo resultados provados de suposições importadas.
2. Unificação: Conecta a expressividade (processamento de sinal) e a treinabilidade (álgebra de Lie) em uma única superfície formal, tratando-as como um problema de design acoplado em vez de listas de verificação independentes.
3. Fundação para Automação: O trabalho serve como um passo em direção ao design assistido por IA ou automatizado de algoritmos de QML. Ele fornece um "mapa de design" verificado onde um agente automatizado poderia propor arquiteturas e a biblioteca poderia verificar a expressividade formalizada e as propriedades condicionais de escala de perda.

Os autores são modestos quanto ao escopo atual: a formalização ainda não cobre casos gerais de $su(d)$ ou invariância de permutação, nem inclui uma camada completa de complexidade teórica para provar "vantagem quântica" (pois o teorema de reconstrução não contabiliza custos de aquisição de dados ou tempo de execução). No entanto, estabelece a base algébrica e estrutural necessária para tais extensões futuras.