Benchmarking Agents for Proving Theorems in Quantum Algorithms and Quantum Information

Resumo Técnico: Benchmarking de Agentes para Prova de Teoremas em Algoritmos Quânticos e Informação Quântica

Definição do Problema
Embora a verificação formal esteja se tornando cada vez mais prática para a computação quântica, a capacidade de agentes de IA em construir provas verificáveis por máquina neste domínio permanece não quantificada. A formalização quântica apresenta desafios únicos: estados e operadores quânticos possuem estruturas de dimensão finita e de nível de tipo; cálculos de circuitos exigem a vinculação de transformações sintáticas a semânticas de álgebra linear; e desigualdades informacionais dependem de domínios específicos, condições de suporte e hipóteses de positividade. Além disso, a notação de livros didáticos suprime coerções, escolhas de base e ordenação de fatores de tensor, que devem ser explícitas em um provador de teoremas como o Lean. Benchmarks existentes (ex: miniF2F, PutnamBench) focam em matemática geral ou problemas de competição, enquanto avaliações de domínios específicos carecem de acesso controlado a bibliotecas ou de validação semântica rigorosa contra as reivindicações matemáticas pretendidas. Há uma necessidade de uma linha de base reprodutível para avaliar o quão bem os agentes de IA podem navegar pelas interfaces específicas e estruturas tipadas exigidas por algoritmos quânticos e teoria da informação quântica (QIT).

Metodologia
Os autores introduzem dois conjuntos de benchmarks coordenados em Lean 4: Lean-QuantumAlg-Bench (QAlg-Bench) e Lean-QIT-Bench (QIT-Bench).

1. Construção do Benchmark:

   • Escopo: Os conjuntos contêm um total de 76 tarefas de conclusão de teoremas (36 para QAlg-Bench, 40 para QIT-Bench).
   • Campos: As tarefas são organizadas em seis campos distintos:
     • Algoritmos Quânticos: Métodos de Estado e Operador (SOM), Algoritmos de Circuito e Algébricos (CAA), e Simulação, Processamento de Sinais e Aprendizado (SSL).
     • Informação Quântica: Canais Quânticos e Representações (QCR), Geometria/Simetria/Distinguibilidade de Operadores e Estados (GSD), e Medidas de Informação Quântica e Emaranhamento (IME).
   • Fluxo de Validação: Os problemas são selecionados da literatura estabelecida, traduzidos para Lean por agentes sob supervisão de pesquisadores e submetidos a verificações automatizadas. Cada tarefa deve compilar em um ambiente Lean fixo. Para declarações de alto risco, uma revisão semântica manual direcionada garante que a assinatura formal capture fielmente a reivindicação matemática, verificando omissões de hipóteses, codificações de tipo incorretas ou conclusões enfraquecidas.
   • Formato da Tarefa: As tarefas fornecem enunciados de teoremas e definições de suporte, mas não oferecem dicas. O sucesso é definido estritamente pelo fato de o corpo do teorema submetido compilar no ambiente fixo sem novos axiomas, marcadores sorry ou modificações em arquivos externos.

2. Estrutura de Avaliação:

   • Modelos: Quatro modelos foram avaliados: GPT-5.5, Kimi K3, DeepSeek V4-Pro e MiniMax M3.
   • Configurações: Duas condições foram testadas:
     • Linha de Base Apenas com a Tarefa (Task-only Baseline): O agente recebe apenas o enunciado do teorema e as definições.
     • Dedução Aumentada por Biblioteca (Library-Augmented Deduction - LAD): O agente recebe a tarefa mais o acesso a uma biblioteca de domínio verificada para consulta.
   • Métricas:
     • Pontuação Ponderada pela Dificuldade: $100 \times \frac{\sum d_i v_i}{\sum d_i}$, onde $d_i$ é a dificuldade pré-atribuída (1–10) e $v_i$ é o indicador binário de aceitação.
     • Taxa de Conclusão: A fração não ponderada de tarefas resolvidas.
     • Eficiência de Custo: Custo econômico (USD por ponto de pontuação) e custo de tempo (segundos por ponto de pontuação).

Principais Contribuições

• Primeiros Benchmarks de Domínio Específico: A introdução do QAlg-Bench e QIT-Bench, os primeiros benchmarks especificamente projetados para avaliar agentes de IA em provas verificáveis por máquina em algoritmos quânticos e teoria da informação quântica usando Lean 4.
• Protocolo de Validação Rigoroso: Um fluxo de construção que combina verificações de compilação automatizadas universais com validação semântica direcionada para garantir que as tarefas formais reflitam com precisão a matemática subjacente, abordando a lacuna "informal–formal".
• Análise Empírica de Acesso à Biblioteca: Uma avaliação sistemática da configuração de "Dedução Aumentada por Biblioteca" (LAD), demonstrando como o acesso a bibliotecas de domínio verificadas impacta o desempenho do agente.
• Perfil de Desempenho Granular: Uma análise que decompõe o desempenho por campo matemático, revelando forças e fraquezas específicas nas capacidades dos agentes através de diferentes subdomínios quânticos.

Resultos

• Pontuações de Desempenho: As pontuações mais altas ponderadas pela dificuldade foram 60.4/100 no QAlg-Bench e 59.6/100 no QIT-Bench.
• Impacto do LAD: Em todas as oito comparações de modelo–benchmark, a configuração LAD melhorou tanto a pontuação quanto a taxa de conclusão em comparação com a linha de base. Os ganhos variaram até 15.9 pontos (ex: o DeepSeek V4-Pro no QAlg-Bench viu um aumento relativo de +42.5%).
• Variância de Modelos: O GPT-5.5 alcançou as pontuações observadas mais altas em todas as combinações de conjunto–condição. No entanto, a eficiência de custo variou significamente; o DeepSeek V4-Pro exibiu o menor custo econômico por ponto de pontuação, enquanto o GPT-5.5 teve o menor custo de tempo.
• Fraquezas por Campo: O desempenho foi irregular entre os campos. Os agentes tiveram dificuldades consistentes com Simulação Quântica, Processamento de Sinais e Aprendizado (SSL) no QAlg-Bench e Medidas de Informação Quântica e Emaranhamento (IME) no QIT-Bench. Por outro lado, o desempenho foi relativamente mais forte em áreas como Canais Quânticos (QCR) e Algoritmos Algébricos de Circuito (CAA).
• Trocas de Custo (Trade-offs): O artigo destaca trocas significativas entre capacidade e eficiência. Por exemplo, o MiniMax M3 dobrou sua pontuação no QAlg-Bench (de 6.4 para 12.8) sob LAD, mas isso partiu de uma base baixa, enquanto o GPT-5.5 alcançou ganhos absolos maiores.

Significância e Alegações
O artigo afirma que estes benchmarks estabelecem uma linha de base reprodutível para o desenvolvimento de agentes de prova mais capazes e confiáveis. Ao isolar os efeitos do acesso à biblioteca e fornecer um ambiente controlado para avaliação, o trabalho permite a medição do progresso na prova agêntica para a ciência quântica. Os resultados sugerem que bibliotecas verificadas são um componente crítico para fortalecer agentes de prova de domínio específico, particularmente em áreas complexas como simulação quântica e teoria do emaranhamento. Os autores posicionam este trabalho como um passo em direção a "cientistas de IA autoevolutivos" capazes de avançar a ciência da informação quântica, embora notem que os agentes atuais ainda exibem fraquezas recorrentes em subcampos específicos. O artigo não alega ter resolvido a verificação formal para todos os problemas quânticos, mas sim fornece a infraestrutura necessária para medir e melhorar o desempenho dos agentes neste domínio.