Resumo Técnico: Ax-Prover

Declaração do Problema

O desenvolvimento de Modelos de Linguagem de Grande Escala (LLMs) capazes de raciocínio formal confiável em diversos domínios científicos permanece um desafio significativo. As abordagens atuais enfrentam uma dicotomia:

1. Provers Especializados: Modelos como DeepSeek-Prover, Kimina-Prover e Goedel-Prover são treinados especificamente para prova de teoremas em Lean. Embora alcancem resultados state-of-the-art em benchmarks de competições matemáticas (por exemplo, MiniF2F, PutnamBench), sofrem com generalização limitada. Eles lutam para se adaptar a domínios fora de seus dados de treinamento (por exemplo, física quântica ou álgebra abstrata) e são frágeis a atualizações na biblioteca Mathlib em evolução, frequentemente exigindo retreinamento frequente. Além disso, carecem da capacidade de usar ferramentas externas ou colaborar interativamente com especialistas humanos.
2. LLMs de Propósito Geral: Modelos como Claude e GPT possuem conhecimento amplo e fortes capacidades de raciocínio, mas carecem de integração nativa com assistentes de prova formal. Eles não podem interagir nativamente com o ambiente Lean, levando a uma divisão nítida onde são acessíveis, mas incapazes de produzir provas rigorosas verificadas por máquina.

Essa lacuna exige um sistema que combine as capacidades de raciocínio amplo e uso de ferramentas de LLMs de propósito geral com o rigor sintático estrito e o poder de verificação do Lean, sem exigir retreinamento específico de domínio ou infraestrutura pesada.

Metodologia

Os autores apresentam o Ax-Prover, um framework agêntico multiagente projetado para automatizar a prova de teoremas em Lean. O sistema aproveita o Protocolo de Contexto de Modelo (MCP) para equipar LLMs de propósito geral com um conjunto de ferramentas Lean, permitindo que eles interajam dinamicamente com o ambiente formal.

Arquitetura do Sistema

O Ax-Prover emprega um fluxo de trabalho de três agentes, onde cada agente é um LLM com prompts específicos:

1. Orquestrador: Atua como um agendador. Recebe o teorema não provado, atribui tarefas ao Prover, gerencia o roteamento de feedback do Verificador e determina quando encerrar o loop de refinamento.
2. Prover: O núcleo construtivo. Transforma iterativamente teoremas não provados em provas completas. O Prover segue um processo incremental:
   • Identifica teoremas-alvo (marcados com sorry).
   • Gera um esboço de prova em linguagem natural.
   • Formaliza o esboço em declarações Lean (usando have e sorry).
   • Propõe táticas para substituir sorry.
   • Usa ferramentas MCP para inspecionar objetivos, buscar lemas e diagnosticar erros antes de prosseguir para a próxima etapa.
3. Verificador: Um guardião final que compila independentemente o arquivo Lean gerado usando lean diagnostic messages. Relata erros e garante que nenhum sorry ou erros de nível 1 permaneçam antes de certificar a prova.

Integração de Ferramentas

Um componente crítico do Ax-Prover é seu acesso a ferramentas Lean via repositório lean-lsp-mcp. Essas ferramentas permitem que o LLM:

• Gerenciamento de Arquivos: Leia, escreva e edite arquivos .lean.
• Diagnósticos: Compile código e recupere mensagens de diagnóstico para identificar erros de sintaxe ou tipo.
• Inspeção de Contexto: Consulte o objetivo de prova atual (lean goal) e informações de hover.
• Busca: Pesquise na biblioteca Mathlib por teoremas relevantes (lean leansearch) e declarações por assinatura de tipo (lean loogle).
• Execução: Execute código e tente múltiplas estratégias de prova.

Esse raciocínio aprimorado por ferramentas permite que o Prover funcione como um "matemático cauteloso", elaborando planos, explorando ideias incrementalmente e verificando a correção a cada passo.

Contribuições Principais

O artigo delineia três contribuições primárias:

1. Framework Ax-Prover: Um fluxo de trabalho agêntico leve que conecta LLMs de propósito geral a ferramentas Lean via MCP. Demonstra desempenho comparável ou superior tanto a LLMs de propósito geral quanto a provers especializados em matemática e física, sem exigir treinamento ou ajuste fino específico de domínio.
2. Novos Benchmarks: A introdução de dois novos conjuntos de dados para avaliar o raciocínio formal em domínios sub-representados:
   • AbstractAlgebra: 100 problemas do livro didático de Dummit & Foote, focando em conceitos de pesquisa de nível de pós-graduação (grupos, anéis, corpos) em vez de quebra-cabeças no estilo de competições.
   • QuantumTheorems: 134 problemas cobrindo mecânica quântica fundamental (matrizes de densidade, observáveis, limites de entropia), conectando física teórica com verificação formal.
3. Verificação Amigável ao Pesquisador: Uma demonstração do Ax-Prover como assistente interativo. Através de estudos de caso em criptografia clássica e quântica, o sistema colabora com especialistas de domínio para formalizar e verificar garantias de segurança complexas, reduzindo a barreira de entrada para pesquisadores sem expertise em Lean.

Resultados

Os autores avaliaram o Ax-Prover (acionado por Claude Sonnet 4) contra provers especializados (DeepSeek-Prover-V2-671B, Kimina-Prover-72B) e LLMs de propósito geral (Sonnet) em vários benchmarks.

• Novos Benchmarks (AbstractAlgebra & QuantumTheorems):

  • AbstractAlgebra: O Ax-Prover alcançou 64% de precisão, superando significativamente o DeepSeek-Prover (24%) e o Kimina (13%). Os modelos especializados lutaram devido à natureza fora da distribuição dos conceitos algébricos de nível de pesquisa.
  • QuantumTheorems: O Ax-Prover alcançou 96% de precisão geral (100% em fácil, 92% em intermediário), comparado a 61% para DeepSeek-Prover e 57% para Kimina. Os modelos especializados falharam em generalizar para definições personalizadas de física (por exemplo, bra/ket, matrizes de densidade) ausentes da Mathlib padrão.
  • NuminaMath-LEAN: O Ax-Prover pontuou 51% no geral, superando DeepSeek-Prover (28%) e Kimina (31%), enquanto o LLM base (Sonnet) pontuou apenas 5%.

• PutnamBench:

  • Neste benchmark desafiador de competição universitária, o Ax-Prover alcançou 14% de precisão, classificando-se como o modelo de código aberto principal e terceiro no geral. Resolveu 92 problemas, superando outros modelos de código aberto como Goedel-Prover-V2 (13%) e DeepSeek-Prover-V2 (7%).
  • Notavelmente, o Ax-Prover alcançou isso com um orçamento computacional significativamente menor (pass@1 com tempo limite de 25 minutos) em comparação com modelos especializados que frequentemente dependem de tentativas paralelas massivas (por exemplo, pass@1024).

• Análise de Uso de Ferramentas:

  • O Prover fez uma média de ~100 chamadas de ferramentas por execução, com altas taxas de sucesso (>99%).
  • O Ax-Prover utilizou um conjunto mais amplo de táticas (incluindo change, suffices, norm_cast) em comparação com modelos especializados, que dependiam fortemente de reescrita local. Isso sugere que a integração de ferramentas aprimora a exploração criativa e a capacidade de gerenciar definições personalizadas.

• Implantação e Custo:

  • O Ax-Prover requer apenas acesso à API, enquanto modelos especializados exigem clusters de GPU de ponta (por exemplo, H200/A100) e expertise em MLOps.
  • Embora os custos de API do Ax-Prover fossem mais altos do que executar modelos especializados em uma única tentativa pass@1, a diferença de custo diminui significativamente quando modelos especializados são executados com altos valores pass@n necessários para desempenho competitivo (por exemplo, DeepSeek-Prover em pass@1024 custaria ~$307k para 1000 pontos de dados vs. ~$4k para Ax-Prover).

Significado e Alegações

O artigo afirma que o Ax-Prover oferece uma metodologia generalizável para verificação formal em diversos domínios científicos, abordando as limitações de sistemas especializados que lutam para generalizar além de seus dados de treinamento.

• Generalização: Ao contrário de provers especializados que são frágeis a mudanças na biblioteca e deslocamentos de domínio, a abordagem baseada em ferramentas do Ax-Prover permite que ele se adapte a novas definições (por exemplo, em física quântica) e versões em evolução do Mathlib sem retreinamento.
• Colaboração: O sistema preenche a lacuna entre IA e pesquisadores humanos. Ao atuar como um assistente interativo, permite que especialistas de domínio se envolvam em verificação formal sem necessidade de profunda expertise em Lean, conforme demonstrado nos estudos de caso de criptografia onde ajudou a identificar lacunas sutis em argumentos informais.
• Eficiência: O framework alcança desempenho competitivo ou superior com um orçamento de computação "mais leve", evitando a necessidade de infraestrutura especializada e cara.

Os autores concluem que o Ax-Prover representa um passo em direção à inteligência artificial científica verificável, onde sistemas de IA podem contribuir para a descoberta científica através de raciocínio formalmente validado, apoiando tanto a prova de teoremas autônoma quanto a pesquisa colaborativa humano-IA.