Resumo Técnico: Otimizando o Tradeoff Custo-Qualidade de Provadores de Teoremas Agênticos em Lean

Declaração do Problema

Modelos de linguagem de grande escala (LLMs) alcançaram progressos significativos na prova automática de teoremas dentro do assistente de prova Lean ao empregar fluxos de trabalho agênticos. Esses fluxos de trabalho tipicamente decompõem problemas complexos em lemas menores, geram inúmeras tentativas de prova e utilizam o feedback do compilador para guiar a busca. Embora essa abordagem resulte em alto desempenho em benchmarks desafiadores como o PutnamBench, ela sofre com custos computacionais proibitivos. Os sistemas atuais frequentemente alocam orçamentos fixos e pré-especificados para decomposição e geração de provas para cada problema, independentemente da dificuldade. Essa política de "passo fixo" leva a um desperdício substancial, pois os agentes frequentemente gastam muito processamento em problemas infactíveis ou enunciados mal formalizados que dificilmente terão sucesso. O desafio central abordado é a falta de consciência de custo dinâmica nos agentes existentes, que falha em otimizar o tradeoff entre o gasto computacional e as taxas de sucesso das provas.

Metodologia

Os autores propõem uma nova arquitetura de Agente de Roteamento de Ações (Action Routing Agent) projetada para substituir políticas estáticas por decisões de roteamento dinâmicas e baseadas em dados. O sistema é conceitualmente dividido em dois planos:

1. Plano de Dados (Geração de Provas)

Inspirado em trabalhos anteriores (ex: Chen et al., 2025c; Varambally et al., 2025), o plano de dados lida com a geração real das provas. Ele opera através de quatro módulos:

• Módulo de Decomposição (Breakdown Module): Um modelo de propósito geral (GPT-OSS-20B) decompõe o problema original em lemas de linguagem natural e esboços de prova.
• Formalizador: O agente formaliza esses lemas em código Lean usando GOEDEL-FORMALIZER-V2-8B, selecionando o melhor candidato que compile sem erros de sintaxe ou de tipo.
• Provador de Decomposição Formal (Formal Breakdown Prover): O sistema tenta provar o teorema de nível superior utilizando os lemas formalizados como axiomas, guiado pelo esboço em linguagem natural.
• Provador de Lemas (Lemma Prover): Uma vez que a decomposição é provada, o agente tenta recursivamente provar os lemas individuais necessários para a prova, empilhando novas dependências em uma pilha.

2. Plano de Controle (Roteamento Custo-Qualidade)

O plano de controle observa a trajetória das tentativas de prova falhas e decide se deve continuar tentando o alvo atual ou encerrar a trajetória para reiniciar com uma nova decomposição. Ele utiliza uma política de roteamento leve baseada em um tradeoff custo-qualidade:

• Estado ($s$): Resume o histórico de tentativas falhas, incluindo tentativas de prova, resultados de compilação, mensagens de erro e comprimentos de saída.
• Espaço de Ação: $\{ \text{TENTAR (ATTEMPT)}, \text{ENCERRAR (TERMINATE)} \}$. O agente ou amostra outra prova para o alvo atual ou descarta a decomposição atual.
• Função de Utilidade: O roteador calcula uma pontuação de utilidade $\tau(s) = \hat{q}(s) - \lambda\hat{c}(s)$, onde:
  • $\hat{q}(s)$ é a probabilidade prevista de sucesso para a próxima tentativa (Qualidade).
  • $\hat{c}(s)$ é o custo previsto da próxima tentativa (medido em tokens de geração de LLM/SFLOPs).
  • $\lambda$ é um hiperparâmetro que controla a penalidade pelo custo computacional.
• Regra de Decisão: Se $\tau(s) > 0$, o agente continua; caso contrário, ele encerra a trajetória atual.

Estimadores:

• Estimador de Custo: Assume que os custos das tentativas são independentes e identicamente distribuídos, utilizando a média do custo das tentativas anteriores na trajetória.
• Estimador de Qualidade: Um modelo de regressão logística treinado para prever a probabilidade de sucesso com base em características da trajetória, especificamente:
  • Similaridade de Prova: A razão média de similaridade de strings difusa (fuzzy string ratio) de provas normalizadas (baixa similaridade sugere confusão).
  • Diversidade de Erros: A razão de erros de compilação únicos em relação ao total de erros (baixa diversidade sugere um modo de falha persistente).
  • Contagem de Tentativas: O número de tentativas anteriores.

Principais Contribuições

1. Identificação de Ineficiência: O artigo identifica que o escalonamento de passo fixo em agentes Lean é criticamente ineficiente e que reduzir tentativas desnecessárias é essencial para um melhor tradeoff custo-qualidade.
2. Arquitetura Inovadora: O desenvolvimento de um provador de Lean estilo lema equipado com um roteador de custo-qualidade online e adaptativo que avalia dinamicamente o valor marginal de computação adicional.
3. Validação Empírica: Demonstração de que o roteador proposto reduz significativamente o processamento desperdiçado enquanto mantém uma precisão competitiva, provando que trajetórias falhas contêm sinais acionáveis para alocação de recursos.

Resultados Experimentais

O sistema foi avaliado em um subconjunto de 85 problemas do PutnamBench, comparando o agente de roteamento dinâmico contra um baseline de passo fixo e um agente "oráculo" com acesso às probabilidades de sucesso reais.

• Redução de Custo: Em paridade de precisão, o agente proposto reduziu o orçamento necessário em 25,8% em média em comparação ao baseline de passo fixo.
• Melhoria de Precisão: Em paridade de custo, o agente alcançou um aumento de 7,8% na taxa de resolução.
• Tradeoffs Específicos:
  • Para alcançar uma taxa de resolução de ~43,6%, o baseline de passo fixo exigiu 31,6 M SFLOPs, enquanto o agente de roteamento exigiu apenas 22,6 M SFLOPs (uma redução de custo de 28,4%).
  • Em um regime de orçamento médio (~41,6% de taxa de resolução), o agente reduziu os custos em 29,6% (17,5 M vs. 24,9 M SFLOPs).
• Estudos de Ablação:
  • Importância das Características: A "diversidade de erro" foi identificada como a característica mais crítica para a estimativa de qualidade.
  • Impacto do Plano de Dados: A própria arquitetura de decomposição estilo lema melhorou a taxa de resolução em quase 100% sobre uma abordagem de geração de prova completa usando o mesmo modelo de 8B, aproximando-se do desempenho de um modelo de 32B.
  • Gap do Oráculo: Embora o agente de roteamento tenha superado significativamente o baseline de passo fixo, permanece um gap em relação ao agente oráculo (que alcançou uma redução de custo de 59,9%), sugerindo espaço para melhorias na engenharia de características e na arquitetura do estimador.

Significância e Alegações

O artigo afirma que trajetórias de Lean falhas fornecem sinais acionáveis para alocação de recursos consciente de custo na prova de teoremas agêntica. Ao se afastar de políticas estáticas de passo fixo em direção ao roteamento dinâmico, os agentes podem reduzir significativamente o desperdício computacional sem sacrificar o desempenho. Os autores posicionam este trabalho como um passo fundamental em direção ao "controle consciente de custo" para a prova matemática formal, sugerindo que futuros agentes devem alocar computação dinamicamente com base no progresso observado e padrões de falha, em vez de atribuir orçamentos de inferência estaticamente. Os resultados indicam que as políticas de passo fixo deixam um espaço substancial para melhorias de eficiência e que as estratégias de roteamento podem mitigar efetivamente custos desnecessários.