AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language

Resumo Técnico: Agente de Prova de Teoremas sobre Árvore de Sintaxe Abstrata de uma Linguagem Redesenhada

Definição do Problema
A Prova de Teoremas Interativa (ITP) é essencial para a verificação de programas e matemática formalizada, mas sofre com altos custos de trabalho manual e escalabilidade limitada. Embora agentes baseados em Grandes Modelos de Linguagem (LLMs) prometam automatizar esse processo, as implementações atuais enfrentam custos de API e consumo de tokens proibitivos. O artigo identifica duas causas raízes para essa ineficiência:

1. Dependência de Sintaxe Concreta: Os agentes atuais operam sobre texto de origem serializado. Eles emitem provas como texto puro e recuperam estados de prova por meio de consultas separadas baseadas em números de linha. Isso força o deslocamento repetitivo de erros e estados sempre que edições alteram os números das linhas, levando a um uso excessivo de chamadas de ferramentas e de tokens.
2. Incompatibilidade com Novas Linguagens: Uma linguagem de prova recente, Minilang, foi projetada para melhorar a eficiência de LLMs ao delegar o raciocínio de granularidade fina para Provadores Automáticos de Teoremas (ATPs) clássicos e alinhar a sintaxe com o raciocínio de linguagem natural. No entanto, como a Minilang é nova (o corpus foi lançado no final de 2025), os LLMs de propósito geral carecem de dados de treinamento para dominar sua sintaxe concreta, e o ajuste fino (fine-tuning) é frequentemente impraticável devido à escassez de dados e ao custo.

Metodologia: Agente sobre AST (AoA)
Os autores propõem o Agente sobre AST (AoA), um agente de prova que eleva a camada de interação do texto de origem para a Árvore de Sintaxe Abstrata (AST) da Minilang. A metodologia consiste em três componentes principais:

1. Representação Centrada em AST:

   • Em vez de gerar código-fonte, o LLM emite provas como representações JSON da AST da Minilang. Este formato é nativo para LLMs de chamada de ferramenta (tool-calling) e remove a dependência de uma sintaxe concreta específica.
   • A AST é formalizada usando JSON Schema, permitindo que os LLMs foquem na construção semântica das provas em vez da ortografia sintática.

2. Modelo de Prova de Edição de Árvore:

   • O agente interage com o provador por meio de um modelo de edição de árvore que funde operações de prova e estados de prova em uma única árvore de prova evolutiva.
   • Fusão de Estado: Diferente dos agentes convencionais onde o estado é recuperado separadamente, cada nó na árvore de prova carreém o estado de seu subobjetivo (subgoal). Quando uma operação é aplicada, o provador computa o estado resultante (objetivos, hipóteses, erros) e o anexa diretamente ao nó da operação.
   • Operações de Edição: O agente utiliza ferramentas (READ, EDIT, QUERY, SUBAGENT) para manipular a árvore. A ferramenta EDIT suporta o preenchimento de slots, inserção de nós, emenda de operações ou exclusão de subárvores.
   • Sincronização Incremental: Após uma edição, o sistema retorna uma visão comprimida da árvore, mostrando apenas os estados e mensagens alterados, em vez de toda a árvore. Isso elimina a necessidade de o LLM reler todo o contexto ou navegar via números de linha frágeis.

3. Design de Sistema sem Modificação de Modelo:

   • O AoA permite que LLMs de propósito geral construam provas em Minilang sem a necessidade de fine-tuning. Ao abstrair a sintaxe concreta e expor a estrutura semântica via JSON, o sistema permite que modelos sem exposição prévia ao corpus da Minilang atuem de forma eficaz.

Principais Contribuições

• Modelo de Prova de Edição de Árvore: Um modelo de interação inovador que substitui o patch de arquivos de origem pela edição de árvore de prova, eliminando a necessidade de consultas separadas de estado de prova baseadas em números de linha.
• Agente AoA: Uma implementação concreta demonstrando que LLMs de propósito geral podem construir provas formais em uma nova linguagem (Minilang) puramente através do design do sistema, sem exposição de escala de corpus ou fine-tuning do modelo.
• Avaliação Empírica: Uma avaliação abrangente contra o Isabelle Agent da Amazon nos benchmarks miniF2F (matemática) e NTP4VC-Pearl (verificação de programas).

Resultados
Avaliado nos conjuntos de sucesso comuns do miniF2F e NTP4VC-Pearl, o AoA demonstra ganhos significativos de eficiência sobre o Isabelle Agent da Amazon:

• Redução de Custo: Alcança 2,3–4,7× menores custos de API (normalizados para reutilização de cache de entrada).
• Eficiência de Tokens: Utiliza 2,9–6,9× menos tokens totais e 3,9–8,9× menos chamadas de ferramenta.
• Velocidade: Conclui casos 1,4–2,0× mais rápido.
• Desempenho:
  • miniF2F: Alcança uma taxa de sucesso de 99,6% (correspondendo ao estado da arte SeedProver).
  • NTP4VC-Pearl: Alcança uma taxa de sucesso de 89,2%, estabelecendo um novo estado da arte para prova de condições de verificação.
• Generalização: Quando testado no Claude Opus 4.5 (lançado antes do corpus público da Minilang), o AoA manteve uma taxa de sucesso de 98,6%, confirmando que a abordagem funciona sem exposição prévia de escala de corpus à linguagem.

Significância e Alegações
O artigo alega que o alto custo dos agentes de prova atuais decorre de operar sobre sintaxe concreta serializada. Ao redesenhar a linguagem de prova (Minilang) e expor sua AST dentro de um modelo de edição de árvore, é possível:

1. Reduzir drasticamente o custo de API e o consumo de tokens dos agentes de prova.
2. Permitir que LLMs de propósito geral operem em novas linguagens formais sem a necessidade de fine-tuning caro ou massivos corpora de treinamento.

Os autores enfatizam que esta abordagem abstrai a informação semântica da linguagem de prova e a reexpressa em um formato nativo para LLMs (JSON/AST), permitindo que o agente foque na lógica de construção da prova em vez da navegação sintática. O artigo conclui que esta metodologia oferece um caminho escalável para integrar LLMs na verificação formal e sugere que abordagens semelhantes baseadas em AST poderiam beneficiar agentes de codificação para novas linguagens de programação.