Resumo Técnico: VERITAS: Busca de Prova Guiada por Verificador para Prova de Teoremas Formal com Zero-Shot

Declaração do Problema

Os atuais provadores de teoremas formais baseados em Grandes Modelos de Linguagem (LLMs) tipicamente colapsam sinais estruturados e ricos de verificadores formais (como o Lean 4) em um resultado binário de passar/falhar. Os verificadores fornecem feedback granular, incluindo erros de sintaxe, incompatibilidades de tipo, progresso parcial de objetivos e status de conclusão da prova. No entanto, os pipelines padrão descartam esses artefatos intermediários, resumindo-os em recompensas escalares ou descartando-os inteiramente. Isso força o algoritmo de busca a "reaprender" informações que o verificador já forneceu explicitamente, uma limitação que se torna particularmente custosa em provas que exigem cadeias de táticas dependentes, onde a correção de cada etapa depende do efeito da etapa anterior sobre o objetivo.

Metodologia: O Framework VERITAS

O VERITAS é um framework zero-shot projetado para rotear cada sinal do verificador de volta para o processo de geração de prova. Ele emprega uma arquitetura de quatro agentes coordenada por um estado de prova compartilhado e um protocolo de busca de duas fases.

1. Quatro Agentes Especializados

Todos os agentes operam em um ProofState compartilhado contendo o teorema, o objetivo atual, hipóteses, histórico de táticas e quatro sinais estruturados do Lean:

• Estrategista (Strategist): Mapeia o estado da prova para uma de seis estratégias de alto nível (direta, indução, contradição, casos, reescrita, apply_lemma) e estima a profundidade, restringindo a busca a um subespaço relevante.
• Recuperador (Retriever): Apresenta premissas relevantes da Mathlib pontuando a sobreposição de palavras-chave contra tokens do objetivo, nomes de lemas e assinaturas.
• Crítico (Critic): Um modelo leve que pontua estados de prova parciais, sugerindo próximas táticas e recomendações de poda. Ele substitui rollouts aleatórios em MCTS por uma estimativa de valor que integra o feedback de quatro vias do Lean.
• Tático (Tactician): Gera $K$ candidatos de tática condicionados à estratégia, premissas recuperadas, orientação do Crítico e, crucialmente, uma lista de táticas falhas anteriores com suas mensagens de erro específicas do Lean injetadas como exemplos negativos.

2. Protocolo de Duas Fases com Garantia de Monotonicidade

O framework utiliza um protocolo conservador de duas fases para garantir que os ganhos sejam atribuíveis à busca impulsionada pelo feedback:

• Fase 1 (Best-of-N): Uma varredura padrão Best-of-N (ex: $N=5$) gera táticas em um único lote. Se qualquer uma tiver sucesso, o teorema é resolvido imediatamente.
• Fase 2 (MCTS Guiado pelo Crítico): Ativado apenas se a Fase 1 falhar. O conjunto de falhas da Fase 1 (táticas e seus erros) é injetado no prompt de sistema do Tático como exemplos negativos. O Crítico guia um Monte Carlo Tree Search (MCTS) onde:
  • Seleção: Utiliza uma fórmula UCB estendida incorporando o valor do Crítico e o alinhamento da estratégia.
  • Expansão: Os agentes rodam sequencialmente; os candidatos são validados via um truque de Validação em Lote do Lean.
  • Simulação: Substitui rollouts aleatórios pelo valor do Crítico aumentado por sinais estruturados ($\sigma_A$ sintaxe, $\sigma_B$ tipo, $\sigma_C$ progresso, $\sigma_D$ conclusão).
  • Retropropagação: Carrega os sinais estruturados para cima em vez de colapsá-los em win/loss binário, preservando o crédito para o progresso parcial.

Validação em Lote do Lean: Em vez de invocar o Lean $K$ vezes por expansão, os candidatos são compilados em um único arquivo .lean como teoremas privados e validados em uma única chamada. Isso reduz o custo de verificação de $O(K)$ para $O(1)$, gerando um aumento de velocidade de aproximadamente $\sim10\times$.

Monotonicidade: O protocolo garante que o conjunto final de teoremas resolvidos seja um superconjunto daqueles resolvidos apenas pela Fase 1 ($S \supseteq S_1$). Isso isola a contribuição da Fase 2, garantindo que quaisquer soluções adicionais sejam estritamente devidas à busca guiada pelo verificador.

Principais Contribuições

1. Framework de Quatro Agentes Zero-Shot: Um sistema que roteia o feedback estruturado do Lean (sintaxe, tipo, progresso, conclusão) para cada decisão de geração sem fine-tuning de traço.
2. Protocolo de Duas Fases: Um design Best-of-N $\to$ Critic-MCTS com uma garantia interna de monotonicidade que permite uma atribuição limpa das contribuições de busca.
3. Otimização de Eficiência: Um truque de validação em lote do Lean que reduz o overhead de verificação em aproximadamente $10\times$.
4. VERITAS-CombiBench: Um novo benchmark de 55 teoremas de combinatória de autor verificados em Lean 4, lançado para expor as limitações da amostragem não guiada.
5. Análise de Atribuição: Evidência empírica mostrando que 11 teoremas do miniF2F foram unicamente solucionáveis pela fase MCTS, que a amostragem plana não conseguiu alcançar.

Resultados Experimentais

Os experimentos foram conduzidos no miniF2F (244 teoremas) e VERITAS-CombiBench (55 teoremas).

• Desempenho no miniF2F: O VERITAS alcançou uma taxa de solução de 40,6% (99/244), superando a linha de base independente de Best-of-5 (36,9%) e um Portfólio artesanal (26,2%).
  • A Fase 2 contribuiu com 11 soluções únicas que a amostragem plana não conseguiu alcançar, principalmente em problemas que exigem 2 a 4 táticas dependentes.
  • Em problemas "difíceis" sem sorry, o VERITAS atingiu 28,9% contra 25,9% para o Best-of-5.
• Desempenho no VERITAS-CombiBench: Este benchmark destacou a falha da amostragem não guiada. O Best-of-5 alcançou apenas 1,8%, ficando abaixo do Portfólio (3,6%) porque os LLMs alucinaram nomes incorretos de lemas da Mathlib. O VERITAS atingiu 7,3% ao corrigir iterativamente esses nomes usando o feedback de erro do Lean.
• Eficiência: O VERITAS domina a fronteira de Pareto para métodos de inferência pura, alcançando 40,6% de taxa de solução com cerca de 27 chamadas de Lean por teorema a um custo de API de ~$150 por varredura.
• Modos de Falha: A análise mostrou que 32% das falhas foram de nível de sintaxe (alucinação de nomes), 17% eram corretas de tipo mas erradas, e 10% foram "quase acertos" (progresso parcial de objetivo) onde o Crítico poderia fornecer orientação de alto valor.

Significância e Alegações

O artigo propõe um princípio de design geral: quando um verificador determinístico emite sinais intermediários estruturados, dobrá-los de volta na geração amplifica o LLM substancialmente mais do que a amostragem adicional faz.

O VERITAS demonstra que:

1. Sinais do Verificador como Estado: Sinais determinísticos do verificador podem servir como estado de tempo de inferência, não apenas verificações finais.
2. Sinergia de Componentes: Acoplar o verificador com a geração é mais eficaz do que escalar o LLM ou o componente de busca isoladamente.
3. Correção Iterativa: Para domínios que exigem recuperação precisa de lemas (como combinatória), a correção iterativa a partir dos erros do verificador é superior à amostragem plana, que tende a alucinar nomes lexicalmente incorretos.

Os autores concluem que, embora o VERITAS não seja uma cura para a criatividade de nível IMO ou latência interativa, sua principal contribuição é o roteamento: coletar eficientamente provas fáceis na Fase 1 e gastar o orçamento computacional na Fase 2 apenas onde as falhas do verificador podem guiar a próxima tática. O trabalho futuro é identificado como a melhoria da recuperação, criação de críticos mais baratos e destilação de traços da Fase 2 para escalar este princípio para a cauda restante de problemas difíceis.