Resumo Técnico: Refinamento Monotônico Livre de Referências para Autoformalização

1. Declaração do Problema

Embora os Modelos de Linguagem de Grande Escala (LLMs) tenham avançado o raciocínio matemático, a autoformalização de teorema completo—a conversão de teoremas em linguagem natural e suas provas acompanhantes em declarações e provas formais completas e mecanicamente verificáveis—permanece pouco explorada. Abordagens existentes frequentemente focam apenas na formalização da declaração, dependendo de espaços reservados "sorry" para as provas, ou tratam a geração da declaração e a prova do teorema como tarefas isoladas.

O desafio central reside na natureza multidimensional da autoformalização de alta qualidade. Uma formalização bem-sucedida deve satisfazer simultaneamente:

1. Validade Formal (VF): Correção sintática e verificação mecânica por um provador de teoremas (por exemplo, Lean4).
2. Preservação Lógica (PL): Alinhamento semântico com a estrutura lógica da declaração original em linguagem natural.
3. Consistência Matemática (CM): Representação precisa de objetos e operações matemáticos.
4. Qualidade Formal (QF): Clareza estrutural, concisão e reutilizabilidade.

Métodos atuais de refinamento iterativo lutam para otimizar conjuntamente essas dimensões, frequentemente melhorando um aspecto (por exemplo, sintaxe) às custas de outros (por exemplo, alinhamento semântico). Além disso, métodos existentes frequentemente dependem de formalizações de verdade fundamental ou intervenção humana para seleção, limitando sua aplicabilidade em cenários livres de referências.

2. Metodologia

Os autores propõem um processo de otimização iterativo, monotônico e livre de referências que opera no momento do teste sem acesso a formalizações de verdade fundamental ou seleção humana. O framework integra feedback de provadores de teoremas e juízes baseados em LLMs para guiar um ensemble de LLMs especializados.

2.1 Função Objetivo

Os autores definem uma função objetivo composta mascarada $J_{OA}(x)$ para equilibrar as quatro dimensões. A Validade Formal ($\pi_{FV}$) atua como uma restrição rígida (uma máscara), enquanto a Preservação Lógica ($\pi_{LP}$), a Consistência Matemática ($\pi_{MC}$) e a Qualidade Formal ($\pi_{FQ}$) são tratadas como dimensões suaves:
$$J_{OA}(x) = \frac{1}{3}\pi_{FV}(x) \left( \pi_{LP}(x) + \pi_{MC}(x) + \pi_{FQ}(x) \right)$$
Esta formulação garante que formalizações inválidas (onde $\pi_{FV}=0$) não sejam selecionadas, independentemente de suas pontuações suaves.

2.2 Juízes LLM e Incerteza

Como as dimensões suaves são intratáveis para cálculo exato, o framework emprega juízes LLM para estimar pontuações. Para lidar com o ruído e o viés inerentes aos LLMs, os autores assumem:

• Estabilidade Assintótica: Os julgamentos se estabilizam após a calibração.
• Incerteza Mensurável: Um Limite Inferior de Confiança (LCB) unilateral pode ser estabelecido para as pontuações verdadeiras.
  O objetivo é otimizado usando um estimador baseado em LCB, garantindo que as decisões de seleção sejam conservadoras e robustas contra ruído de avaliação.

2.3 Papéis do Gerador e Responsividade

O framework decompõe os papéis do LLM em três categorias, guiados por um mapa de responsividade que modela melhorias esperadas por dimensão:

1. Geradores Únicos (OOGs): Geram formalizações iniciais do zero (por exemplo, modelos matemáticos especializados como DeepSeek-Prover).
2. Reparadores de VF (FVRs): Visam e corrigem especificamente candidatos formalmente inválidos (por exemplo, modelos capazes de revisão iterativa de provas).
3. Geradores Recorrentes (REGs): Refinam o melhor candidato atual com base no feedback de juízes LLM sobre dimensões suaves específicas (PL, CM ou QF).

2.4 Política de Aceitação Monotônica

O processo itera através da geração e seleção de candidatos. Uma Política de Aceitação Conservadora é aplicada: um novo candidato é aceito apenas se sua pontuação objetivo estimada (baseada no LCB) for estritamente maior que a melhor atual. Isso garante melhoria monotônica certificada, significando que a qualidade da formalização selecionada nunca diminui ao longo das iterações. O processo é provado para convergir e terminar sob condições específicas.

3. Contribuições Principais

1. Definição Formal e Framework: O artigo é o primeiro a definir formalmente a autoformalização de teorema completo como uma tarefa unificada e propor um processo iterativo monotônico livre de referências para resolvê-la.
2. Função Objetivo Composta Mascarada: Introdução de uma função objetivo que impõe a Validade Formal como uma restrição rígida enquanto otimiza múltiplas dimensões suaves (PL, CM, QF) simultaneamente.
3. Ensemble Especializado por Papel: Decomposição da tarefa de autoformalização nos papéis OOG, FVR e REG, utilizando um mapa de responsividade para selecionar geradores mais eficazes para dimensões de qualidade específicas.
4. Garantias Teóricas: Fornecimento de provas teóricas para monotonicidade certificada, convergência e terminabilidade do processo, garantindo progresso não decrescente mesmo sob ruído realista de juízes.
5. Validação Empírica: Demonstração de que o framework ensembles efetivamente os pontos fortes de LLMs especializados e de propósito geral para alcançar resultados de alta qualidade em benchmarks padrão.

4. Resultados Experimentais

O método foi avaliado em miniF2F-Test e ProofNet-Test usando Lean4. O framework empregou um ensemble de modelos incluindo DeepSeek-Prover-V2-7B, Goedel-Prover-V2-8B, Seed-Coder-8B, Qwen2.5-7B e GPT-4.1-mini (como juízes).

Principais Métricas de Desempenho:

• miniF2F: Alcançou 100,00% de Validade Formal e uma pontuação geral de 90,27%. A taxa de formalizações "perfeitas" (todas as dimensões pontuando 1) atingiu 49,18%.
• ProofNet: Alcançou 77,96% de Validade Formal e uma pontuação geral de 52,45%, com 17,74% de formalizações perfeitas.

Descobertas Comparativas:

• Monotônico vs. Baselines: O processo monotônico superou significativamente tanto o Best-of-k (amostragem de $k$ saídas) quanto o Refinamento Self-Iterativo (ISR) sem políticas de aceitação.
• Ensemble vs. Modelo Único: Embora um modelo único forte (GPT-5.4) tenha mostrado melhoria, o ensemble de modelos menores e especializados atribuídos a papéis específicos alcançou desempenho superior, particularmente na Validade Formal.
• Robustez: A tendência monotônica persistiu mesmo quando avaliada por diferentes famílias de juízes LLM (por exemplo, Qwen vs. GPT) e especialistas humanos, indicando que as melhorias não são artefatos de viés do juiz.

5. Significado e Alegações

O artigo alega que este trabalho oferece um passo prático e teoricamente fundamentado em direção à autoformalização confiável. Ao operar de maneira livre de referências, a abordagem é aplicável mesmo em domínios que carecem de bibliotecas formais extensas, potencialmente auxiliando a formalização de áreas pouco exploradas da matemática e da ciência.

Os autores enfatizam que o framework fornece uma metodologia principiante para autoformalização assistida por IA que:

• Reduz a necessidade de supervisão humana em pipelines de verificação formal em grande escala.
• Quantifica e controla explicitamente a incerteza no julgamento através de suposições de LCB.
• Demonstra que combinar LLMs complementares com feedback de verificadores formais pode produzir formalizações com qualidade comprovadamente não decrescente.

O trabalho conclui que, embora os custos computacionais sejam maiores do que a inferência de passagem única, o trade-off é justificado pelos ganhos significativos em desempenho e estabilidade, abrindo caminho para pesquisas futuras em raciocínio formal assistido por IA seguro e confiável.