Resumo Técnico: Otimização Eficiente de Tempo de Teste para Autoformalização de Provas Multi-Agente

1. Declaração do Problema

A autoformalização de prova completa visa traduzir extensas provas matemáticas em linguagem natural para o raciocínio formalmente validado dentro de assistentes de prova como o Lean. Diferente da formalização ao nível de enunciado, que foca na tradução de um único teorema, a autoformalização de prova completa é um desafio de longo horizonte. Ela requer a coordenação de alegações, contextos e dependências através de inúmeros passos de prova para construir um todo globalmente verificável.

As abordagens atuais enfrentam duas limitações primárias:

1. Custo de Treinamento: Muitos métodos dependem de ajuste fino supervisionado em larga escala, o que é difícil devido à escassez de dados de supervisão pareados ao nível de prova.
2. Otimização de Tempo de Teste Ineficiente: Métodos de inferência existentes frequentemente aplicam reparos excessivos e não guiados ou refinamento iterativo em todo o pipeline. Em configurações de prova completa, o feedback do verificador (ex: erros do Lean) chega apenas após uma longa cadeia de geração, raramente revelando qual decisão anterior causou a falha. Isso torna desafiador direcionar o computação de tempo de teste limitada para melhorias direcionadas em vez de tentativas de retentativa não guiadas.

2. Metodologia: O Framework TOMAP

Os autores introduzem o TOMAP (Test-time Optimization for Multi-Agent Proof autoformalization), um framework que estrutura a tarefa como um pipeline Decompositor-Formalizador-Provador. A inovação central é uma estratégia de otimização de tempo de teste eficiente que identifica e visa o gargalo crítico do sistema.

2.1 Pipeline Multi-Agente

O sistema consiste em três agentes especializados:

• Decompositor ($D$): Divide a prova informal em subproposições atômicas e autocontidas (unidades de prova) com dependências explícitas.
• Formalizador ($F$): Traduz cada subproposição de linguagem natural em uma declaração formal em Lean.
• Provador ($P$): Gera scripts de táticas para provar cada objetivo formalizado.
• Verificador ($V$): Um verificador externo do Lean que valida o arquivo de prova montado.

2.2 Análise de Elo Fraco

Antes da otimização, os autores realizam uma "análise de elo fraco" para determinar onde a computação de tempo de teste gera o maior retorno. Ao intervir em cada estágio (Decompositor, Formalizador, Provador) individualmente enquanto mantém os outros fixos, eles medem a recuperabilidade do sucesso de verificação de ponta a ponta.

• Descoberta: O Decompositor é o gargalo crítico. Revisar a especificação da unidade de prova em linguagem natural (alegações, suposições, dependências) produz ganhos significativamente maiores no sucesso de verificação final (51,1% de acurácia) em comparação com a revisão de declarações formais (45,1%) ou scripts de prova (33,7%).
• Implicação: Unidades de prova atômicas e de alta qualidade reduzem a formalização e a prova subsequentes para tarefas locais dentro das capacidades do Formalizador e do Provador.

2.3 Estratégia de Otimização de Tempo de Teste

O TOMAP foca toda a computação de tempo de teste no refinamento do Decompositor, tratando o Formalizador e o Provador como executores subsequentes fixos. A otimização segue um loop de estilo GEPA (Evolução de Prompt Reflexiva):

1. Pool de Candidatos: Mantém um pool de decomposições candidatas para uma determinada entrada.
2. Pontuação por Rubrica: Em vez de chamar imediatamente o caro verificador Lean, os candidatos são pontuados por um "Juiz de Rubrica" baseado em LLM contra três dimensões:
   • Fidelidade Semântica: Alinhamento com a prova original em linguagem natural.
   • Provabilidade: Se cada unidade é autocontida e logicamente completa.
   • Amigabilidade ao Lean: Clareza, explicidade de suposições e evitar ambiguidades.
3. Evolução Guiada por Pareto: Os candidatos são avaliados em uma fronteira de Pareto baseada nas pontuações da rubrica. Um proponente de LLM reflexivo seleciona candidatos de alto desempenho, critica-os com base no feedback da rubrica e propõe decomposições revisadas.
4. Portão de Verificação: Apenas candidatos que atendem a um limiar de alta qualidade (passando pelo portão da rubrica) são comprometidos ao pipeline Formalizador-Provador para a verificação cara e fiel do Lean.

Este design de dois níveis equilibra o feedback de proxy barato e denso (rubricas) para guiar a busca com a verificação fiel e custosa reservada apenas para candidatos promissores.

3. Principais Contribuições

• Identificação de Gargalo: O artigo fornece evidência empírica via análise de elo fraco de que a qualidade da decomposição da prova é o determinante primário do sucesso na autoformalização de prova completa, deslocando o foco de otimização de todo o pipeline para a interface do Decompositor.
• Framework TOMAP: Um novo método de otimização de tempo de teste que desacopla a busca da verificação. Ele evolui as decomposições de prova usando feedback de rubrica multi-objetivo e seleção de Pareto, reduzindo significativamente a dependência de chamadas caras ao Lean durante a fase de busca.
• Eficiência e Desempenho: A abordagem alcança resultados de estado da arte sem exigir treinamento em larga escala, baseando-se, em vez disso, na otimização eficiente de tempo de inferência.

4. Resultados Experimentais

Experimentos foram conduzidos no PROOFFLOWBENCH (184 problemas de nível de graduação) e miniF2F (244 problemas de nível de ensino médio).

• Desempenho: O TOMAP supera tanto os baselines baseados em treinamento (ex: ProofBridge) quanto os baselines livres de treinamento (ex: PROFFLOW, Monotonic).
  • No PROOFFLOWBENCH, o TOMAP (usando Gemini3-Pro) melhorou a pontuação conjunta de Correção Sintática e Fidelidade Semântica em 19,0% sobre o melhor método anterior.
  • No miniF2F, alcançou uma melhoria de 8,2% na métrica conjunta.
• Fidelidade Semântica: O TOMAP supera significativamente os geradores monolíticos na preservação da estrutura semântica da prova original, evitando a tendência de outros métodos de gerar código Lean semanticamente incorreto, mas sintaticamente válido.
• Eficiência de Custo: Embora o TOMAP exija mais computação de tempo de teste do que os baselines ingênuos, ele alcança taxas de sucesso mais altas com menor custo total em comparação com métodos que dependem de retentativas iterativas extensas de todo o pipeline.
• Análise de Escala: Estudos de ablação revelam que a maioria dos ganhos de desempenho ocorre nas primeiras iterações da evolução da decomposição, fornecendo orientação prática para selecionar o orçamento de tempo de teste.

5. Significância e Alegações

O artigo afirma que a autoformalização de prova completa é fundamentalmente um problema de qualidade de decomposição. Ao identificar o Decompositor como o estágio de maior recuperação de feedback, os autores demonstram que a otimização eficiente de tempo de teste pode ser alcançada focando recursos no refinamento da estrutura da prova em linguagem natural, em vez de tentar repetidamente a formalização ou a prova.

A significância do TOMAP reside em sua capacidade de:

1. Elevar o teto do raciocínio matemático verificável, preenchendo a lacuna entre provas informais e verificação formal de forma mais fiel.
2. Fornecer uma alternativa escalável e livre de treinamento para abordagens complexas de ajuste fino.
3. Oferecer um framework prático para alocação de computação de tempo de teste limitada em sistemas multi-agente, priorizando o "elo fraco" identificado através de análise causal.

Os autores observam limitações, incluindo a restrição a provas de escala de benchmark em vez de matemática de nível de pesquisa e a suposição de que as provas informais de entrada são corretas. Eles deixam a detecção e o reparo de passos de prova incorretos como trabalho futuro.