Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving

Resumo Técnico: Mechanic – Fluxo de Trabalho de Decomposição Formal Orientado por Sorrifier

1. O Problema

O provamento automático de teoremas (ATP), especialmente em linguagens formais como o Lean, enfrenta um dilema significativo ao lidar com problemas de raciocínio matemático complexo:

• Ineficiência da Regeneração Total: Quando uma tentativa de prova falha, os sistemas existentes frequentemente descartam toda a prova gerada e tentam regenerá-la do zero. Isso é computacionalmente custoso e desperdiça partes da prova que já estavam corretas.
• Degradação de Contexto na Correção Iterativa: Abordagens que tentam corrigir erros localmente dentro de uma prova longa tendem a acumular contextos excessivamente grandes. À medida que o contexto cresce, a capacidade do modelo de linguagem (LLM) de focar nos subproblemas não resolvidos diminui, levando a uma degradação progressiva do desempenho.
• Fragilidade de Linguagens Formais: Mesmo que a estrutura lógica de alto nível de uma prova informal seja correta, erros sintáticos ou lógicos menores no Lean podem causar falhas de compilação em cascata, invalidando blocos de código subsequentes que, de outra forma, estariam corretos.

2. Metodologia: O Agente Mechanic

O Mechanic é um sistema de agente proposto que introduz uma estratégia de decomposição formal orientada por "sorrifier". A metodologia baseia-se na preservação da estrutura da prova formal, isolando apenas os erros localizados em vez de descartar o trabalho completo.

O fluxo de trabalho consiste em quatro etapas principais (ilustradas na Figura 2 do artigo):

1. Prova Informal (Informal Prove):

   • Um modelo LLM (Reasoner) gera um esboço de prova em linguagem natural.
   • Um Verificador avalia a lógica e a correção desse esboço.
   • O Reasoner refina iterativamente a prova baseada no feedback, até que uma solução informal coerente seja aceita.

2. Prova Formal (Formal Prove):

   • O Prover traduz o esboço informal para o código Lean.
   • O sistema tenta compilar e, se houver erros, utiliza ferramentas de busca (Mathlib) e feedback do compilador para correções iterativas.

3. Divisão de Subobjetivos via Sorrifier (Subgoal Split):

   • Se a prova falhar após várias tentativas de correção, o componente central, o Sorrifier, entra em ação.
   • Mecanismo do Sorrifier: Em vez de rejeitar a prova, o Sorrifier identifica o erro mais interno (innermost) e substitui o bloco de prova falho pelo placeholder sorry do Lean.
   • O compilador é reexecutado imediatamente. Isso remove erros em cascata (que ocorriam porque o contexto estava corrompido pelo erro original).
   • O processo repete-se até que a prova compile com sucesso, contendo apenas alguns sorry isolados.
   • Extração: Cada sorry é extraído como um novo subobjetivo (subgoal) autônomo, com seu próprio contexto de hipóteses e objetivo, criando um teorema menor e independente.

4. Processamento de Subobjetivos (Subgoal Process):

   • Cada subobjetivo extraído passa pelo mesmo pipeline (Prova Informal -> Formal -> Sorrifier) recursivamente.
   • Uma vez provado, o subobjetivo é reintegrado à prova original usando a tática apply, substituindo o sorry.
   • O processo termina quando todos os subobjetivos são resolvidos ou quando um limite de recursão é atingido (indicando que o problema é intratável com a estratégia atual).

Componentes do Sistema:

• LLMs Especializados: Reasoner (raciocínio), Verifier (avaliação) e Prover (geração de código Lean).
• Ferramentas Lean: Verificador de compilação e ferramentas de busca de teoremas (LeanDex, Loogle).
• Sorrifier: O algoritmo que realiza a substituição cirúrgica de erros por sorry para isolar falhas.

3. Contribuições Principais

• Decomposição Formal Preservadora: Diferente de abordagens anteriores que voltam para o nível informal ao falhar, o Mechanic mantém a estrutura formal válida, substituindo apenas os blocos falhos por sorry. Isso evita a perda de progresso e reduz o tamanho do contexto.
• Isolamento de Erros em Cascata: O algoritmo do Sorrifier lida especificamente com a natureza de tipos dependentes do Lean, onde um erro inicial corrompe o contexto subsequente. Ao corrigir iterativamente o erro mais interno, ele "limpa" os erros derivados.
• Eficiência Computacional: Ao decompor problemas complexos em subobjetivos menores e independentes, o sistema permite a paralelização de esforços de prova e reduz a carga cognitiva sobre o LLM em cada etapa.
• Arquitetura de Agente Híbrida: Combina raciocínio informal (para estrutura lógica) com verificação formal rigorosa e decomposição automática de falhas.

4. Resultados Experimentais

O sistema foi testado em benchmarks de competições matemáticas de alto nível: Putnam 2025 (12 problemas) e IMO 2025 (4 problemas).

• Desempenho no Putnam 2025:

  • O Mechanic resolveu 11 de 12 problemas.
  • Eficiência: Foi significativamente mais rápido e barato que as baselines (Hilbert, Aristotle, Axiom, Seed-Prover, Numina).
  • Custo: Custo médio de $18.50 e tempo médio de 114 minutos para os problemas resolvidos, comparado a centenas de minutos e custos muito mais altos nas outras abordagens.
  • Qualidade da Prova: Gerou provas com menos linhas e menos teoremas auxiliares (lemmas), indicando um estilo de prova mais disciplinado e focado.

• Desempenho no IMO 2025:

  • Demonstrou vantagem de eficiência crescente conforme a dificuldade do problema aumentava.
  • No problema mais difícil (P1), o tempo de execução foi de aproximadamente um terço do tempo gasto pelo sistema Seed.
  • Estrutura de Árvore de Prova: As árvores de prova geradas pelo Mechanic são mais largas e mais rasas (shallow) em comparação com as árvores profundas e aninhadas de outros métodos. Isso permite maior paralelização e menor latência de espera entre etapas.

• Estudos de Ablação:

  • A etapa de prova informal é crucial para problemas complexos, reduzindo erros na formalização e o tamanho da árvore de prova.
  • O pipeline é escalável, funcionando bem com diferentes modelos de base (Gemini, Claude), embora modelos com menor capacidade de raciocínio Lean tenham desempenho inferior.

5. Significado e Conclusão

O artigo Mechanic representa um avanço significativo na interseção entre raciocínio matemático de IA e verificação formal. Ao introduzir o conceito de decomposição orientada por sorry, o trabalho resolve o dilema entre "regenerar tudo" e "corrigir tudo", oferecendo uma via intermediária eficiente que preserva o progresso válido.

A principal implicação é que a eficiência em provadores automáticos não depende apenas da força bruta do modelo de linguagem, mas da gestão inteligente do estado de falha. A capacidade de isolar erros localmente e transformar uma prova falha em uma série de subproblemas gerenciáveis permite que sistemas de IA atinjam níveis de desempenho (como medalhas de ouro simuladas no IMO) com recursos computacionais drasticamente reduzidos. O trabalho sugere que futuros agentes de prova devem adotar fluxos de trabalho modulares e iterativos que respeitem a estrutura formal existente, em vez de tratá-la como descartável.