⚛️ física quântica

Discovering formally verified quantum programs with AI

Este artigo demonstra como agentes de modelos de linguagem de grande escala, operando dentro de uma estrutura de verificação formal no provador de teoremas Lean, podem descobrir autonomamente e provar matematicamente a corretude de novos programas quânticos que alcançam melhorias de desempenho significativas em relação às linhas de base existentes em aplicações científicas como aritmética quântica e simulação de fusão.

Autor original: Sergey Shirobokov, Ben Jaderberg, Katerina Hristova, George Tsoukalas, Johannes Bausch, Eric Wieser, Francisco J. H. Heras, Nicholas C. Rubin, Guang Hao Low, Sébastien Racanière, Nenad Tomašev, Lei M.

Publicado 2026-11-09

📖 4 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autor original: Sergey Shirobokov, Ben Jaderberg, Katerina Hristova, George Tsoukalas, Johannes Bausch, Eric Wieser, Francisco J. H. Heras, Nicholas C. Rubin, Guang Hao Low, Sébastien Racanière, Nenad Tomašev, Lei M. Zhang, James Watson, Tanuj Khattar, Aws Albarghouthi, Stavan Jain, Harun Khan, Leopoldo Sarra, Andrew W. Senior, Michael Broughton, Hussain Masoom, Sergio Boixo, Ryan Babbush, Swarat Chaudhuri, Pushmeet Kohli

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelo autor. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Os computadores quânticos prometem resolver problemas que são atualmente impossíveis para as máquinas que usamos todos os dias, desde o design de novos medicamentos até a modelagem do comportamento das estrelas. No entanto, construir uma máquina que possa realmente realizar essas tarefas é incrivelmente difícil. O hardware ainda está em sua infância, propenso a erros e pequeno demais para lidar com os cálculos massivos exigidos pela ciência do mundo real. Para preencher essa lacuna, os cientistas precisam de algoritmos melhores — instruções passo a passo que dizem ao computador quântico como resolver um problema usando o menor número possível de recursos. Por décadas, encontrar essas instruções tem sido um processo lento e manual, dependendo da intuição e do trabalho árduo de especialistas humanos que passam anos refinando uma única ideia.

O desafio é que esses algoritmos são tão complexos que nem mesmo os computadores clássicos mais poderosos conseguem testá-los para ver se funcionam corretamente antes que o hardware quântico esteja pronto. Isso cria um ciclo vicioso: precisamos de algoritmos melhores para tornar o hardware útil, mas não podemos verificar os algoritmos sem o hardware. Uma equipe de pesquisadores do Google agora quebrou esse ciclo combinando inteligência artificial com prova matemática rigorosa. Eles criaram um sistema onde agentes de IA atuam como pesquisadores, escrevendo e testando programas quânticos em uma linguagem que um computador pode verificar quanto à correção absoluta. Essa abordagem permite que eles descubram novos algoritmos altamente eficientes para problemas científicos que são muito grandes para serem simulados em qualquer computador existente.

Os pesquisadores construíram um laboratório digital onde equipes de agentes de IA colaboram para resolver quebra-cabeças científicos específicos. Em vez de apenas adivinhar e verificar, esses agentes trabalham dentro de uma estrutura estrita chamada de provador de teoremas (theorem prover). Pense nesta estrutura como um livro de regras que exige que cada etapa de uma solução proposta seja matematicamente provada como correta antes de ser aceita. Os agentes têm a tarefa de escrever programas quânticos que simulem sistemas físicos, como a interação de partículas em um reator de fusão ou como uma molécula de medicamento se decompõe no corpo. Se um agente propõe um programa que economiza tempo ou usa menos recursos, o sistema verifica imediatamente a matemática. Se a prova se sustentar, a solução é salva; se falhar, o agente aprende com o erro e tenta novamente. Esse processo acontece em um espaço de trabalho compartilhado onde diferentes equipes de agentes podem ver o progresso umas das outras, compartilhar ideias e construir sobre as descobertas umas das outras, de forma muito semelhante aos cientistas humanos em uma conferência.

Usando este método, a equipe abordou cinco grandes desafios científicos. Em um caso, eles melhoraram uma operação matemática fundamental usada em muitos algoritmos quânticos, tornando-a quase trezentas vezes mais eficiente do que o melhor método anterior. Em outro, otimizaram um algoritmo de busca, encontrando soluções que foram até 1,4 vezes mais rápidas do que as alternativas conhecidas mais fortes. Os feitos mais significativos vieram na simulação de fenômenos físicos complexos. Para uma simulação relevante para a fusão nuclear, que envolve rastrear a perda de energia de partículas movendo-se através do hidrogênio, a IA descobriu um programa que reduziu os recursos necessários em quase onze vezes. Para uma simulação de uma reação química envolvida na fotoquímica, a melhoria foi oito vezes melhor. Finalmente, para um modelo de uma enzima chave que ajuda o corpo humano a processar medicamentos, a IA encontrou uma solução que foi quase 2,5 vezes mais eficiente.

Esses resultados não são apenas melhorias teóricas; eles representam uma mudança em como a descoberta científica pode acontecer. Os programas descobertos pela IA são tão complexos que envolvem milhares de componentes lógicos, indo muito além do que os computadores quânticos atuais podem executar. Como o trabalho da IA é respaldado por provas matemáticas formais, os pesquisadores podem confiar que esses programas funcionarão corretamente assim que o hardware alcançar o nível necessário. O sistema efetivamente permite que cientistas projetem algoritmos para máquinas que ainda não existem, encurtando o caminho para a computação quântica prática. Ao automatizar a busca por essas soluções e verificá-las com certeza matemática, os pesquisadores mostraram que a inteligência artificial pode acelerar o desenvolvimento da tecnologia quântica, transformando o que antes era uma luta lenta e manual em um processo de descoberta rápido e colaborativo.

Resumo Técnico: Descoberta de Programas Quânticos Formalmente Verificados com IA

Declaração do Problema

A realização da vantagem quântica prática na ciência depende tanto da melhoria dos algoritmos quanto dos avanços no hardware. Historicamente, o desenvolvimento desses algoritmos exigiu anos de colaboração especializada humana. Embora os modelos de linguagem de grande escala (LLMs) tenham acelerado a descoberta na matemática e em algoritmos clássicos, sua aplicação à computação quântica tem sido limitada. O principal gargalo é a incapacidade de verificar algoritmos quânticos gerais sem hardware tolerante a falhas; a simulação clássica é restrita a conjuntos de portas pequenos ou restritos, limitando o espaço de busca para descobertas. Consequentemente, há uma necessidade de um framework que possa descobrir, verificar e otimizar programas quânticos para aplicações assintóticas de larga escala que vão além do alcance da simulação clássica.

Metodologia

Os autores introduzem um fluxo de trabalho de descoberta multiagente centrado em uma biblioteca de verificação formal construída no provador de teoremas Lean. Este sistema combina agentes de modelos de linguagem de grande escala com provas matemáticas rigorosas para sintetizar e verificar programas quânticos.

1. Biblioteca de Verificação Formal

O núcleo do sistema é uma biblioteca baseada em Lógica de Hoare Quântica (QHL). Ela formaliza:

Estados Clássico-Quânticos: Combinando fluxo de controle clássico com estados quânticos.
Corretude: Expressa como triplas de Hoare (pré-condição, programa, pós-condição), verificadas via cálculo de pré-condição mais fraca.
Contagem de Recursos: Limites formais nos custos de recursos esperados e de pior caso, visando especificamente o custo de espaço-tempo ( $Q \cdot T$ ), definido como o número de qubits lógicos ( $Q$ ) multiplicado pelo número de portas $T$ ( $T$ ). Esta métrica é crítica para arquiteturas tolerantes a falhas, onde a destilação de portas $T$ é o overhead dominante.

2. Arquitetura de Descoberta Multiagente

Pesquisadores definem uma especificação de problema em Lean, declarando o teorema de corretude alvo e os limites de custo com espaços reservados (sorry) para a solução.

Equipes de Agentes: Equipes independentes de agentes de LLM são lançadas para explorar algoritmos candidatos. As equipes podem variar de agentes únicos a estruturas hierárquicas que lidam com sub-rotinas.
Colaboração: As equipes compartilham o progresso por meio de uma wiki compartilhada (armazenando soluções verificadas, lemas reutilizáveis e notas sobre becos sem saída) e conferências agendadas (para discutir conjecturas não verificadas e críticas).
Verificação Independente: Um verificador externo, utilizando o Comparador Lean, checa cada submissão contra uma especificação congelada. Isso evita que os agentes explorem brechas (ex: enfraquecer teoremas ou alterar definições) e garante que apenas provas válidas e verificadas por máquina sejam aceitas.

Principais Contribuições

Framework de Verificação Formal para Algoritmos Quânticos: O artigo apresenta uma biblioteca Lean abrangente que suporta a verificação formal de corretude e custos de recursos para circuitos quânticos dinâmicos, incluindo medições de meio de circuito e controle de fluxo clássico.
Fluxo de Trabalho de Descoberta Multiagente: Um novo paradigma de pesquisa onde pesquisadores humanos definem especificações, e equipes de agentes autônomos colaboram para descobrir, otimizar e provar formalmente algoritmos quânticos.
Soluções Verificadas por Máquina: O sistema produz programas quânticos com provas de corretude e custo verificadas por máquina, eliminando a necessidade de revisão de código manual e permitindo uma colaboração segura e de larga escala.

Resultados

O fluxo de trabalho foi aplicado a cinco problemas distintos, gerando reduções significativas de recursos em comparação com as bases publicadas mais fortes:

Problema	Domínio de Aplicação	Custo Base ( $Q \cdot T$ )	Custo deste Trabalho ( $Q \cdot T$ )	Melhoria
Busca de Grover Paralela	Busca Não Estruturada	Protocolos publicados mais fortes	Circuitos verificados	Até 1,41× de redução nas rodadas de oráculo esperadas
Arcos de Arcsin (Ponto Fixo)	Preparação de Estado	$> 1,08 \times 10^8$	$3,70 \times 10^5$	290× de redução
Poder de Parada de $\alpha$ -partícula	Fusão por Confinamento Inercial	$5,42 \times 10^{15}$	$4,98 \times 10^{14}$	10,9× de redução
Dinâmica Não Born–Oppenheimer	Fotoquímica ( $C_{23}H_{20}N_3O$ )	$4,98 \times 10^{15}$	$6,16 \times 10^{14}$	8,08× de redução
Composto Citocromo P450	Metabolismo de Drogas	$1,09 \times 10^{12}$	$4,37 \times 10^{11}$	2,49× de redução

Melhorias Algorítmicas Específicas

arcsin: Os agentes primeiro otimizaram usando um conjunto de portas "kickmix" restrito (verificável via fuzzing clássico) e depois elevaram a solução para o conjunto completo Clifford+ $T$ usando verificação formal, descobrindo um mecanismo de busca de coeficientes que reduziu as contagens de portas $T$ em 33%.
Poder de Parada (Stopping Power): A solução utilizou uma representação de grade no espaço real para explorar a exclusão de Pauli, reduzindo a norma $\lambda$ da combinação linear de unitárias (LCU). Também introduziu uma técnica para reutilizar o registro de momento eletrônico total entre os passos de caminhada, cortando as contagens de portas $T$ por passo em 10%.
Dinâmica Não Born–Oppenheimer: As melhorias incluíram uncomputation baseada em medição para carregamento de coordenadas, aproximação de potenciais $1/r$ via polinômios de Bernstein (evitando multiplicação cara) e uso de lógica reversível para cargas nucleares em vez de amostragem por alias.
Citocromo P450: A solução substituiu buscas de ângulo binárias por um registro one-hot para vetores orbitais, reduzindo significativamente o custo de portas $T$ da preparação de estado e aplicação de rotação.

Significância e Alegações

O artigo afirma que combinar verificação formal com agentes de LLM desloca a fronteira do desenvolvimento de algoritmos quânticos. Ao mover o esforço humano do design e otimização manual de circuitos para a especificação de problemas e interpretação científica, o fluxo de trabalho permite a descoberta de algoritmos que são:

Além da Simulação Clássica: Capazes de abordar problemas que exigem milhares de qubits e $10^9$ a $10^{15}$ operações lógicas, regimes onde o teste numérico clássico é impossível.
Rigorosamente Verificados: Cada solução vem com uma prova de corretude e custo verificada por máquina, garantindo confiabilidade sem a necessidade de hardware tolerante a falhas para testar os algoritmos.
Colaborativos: O sistema multiagente demonstra que a colaboração entre equipes (via wikis e conferências) é essencial, sendo que as melhores soluções frequentemente emergem da síntese de ideias entre múltiplas equipes.

Os autores enfatizam que, embora essas melhorias sejam substanciais, as simulações de ponta a ponta ainda demandam recursos além das projeções atuais de hardware inicial tolerante a falhas. No entanto, este trabalho estabelece um caminho para reduções cumulativas de recursos, estreitando a lacuna para a computação quântica prática pelo lado algorítmico enquanto o hardware escala pelo lado físico. O artigo conclui que esta abordagem permite que pesquisadores projetem algoritmos que os computadores clássicos e quânticos de hoje não podem testar, encurtando o caminho para a computação quântica prática.