Resumo Técnico: Formalizar uma Vez, Editar o Restante (BASE)

1. Definição do Problema

À medida que os Grandes Modelos de Linguagem (LLMs) são cada vez mais aplicados ao raciocínio matemático, eles frequentemente geram múltiplos caminhos de raciocínio distintos e respostas candidatas para um único problema. Um desafio crítico surge na seleção de respostas: como verificar qual candidata é correta sem acesso a rótulos de verdade fundamental (ground-truth) durante o escalonamento em tempo de teste.

Embora abordagens existentes, como votação majoritária ou modelos de recompensa aprendidos, ofereçam sinais estatísticos, elas carecem de garantias formais. Trabalhos recentes utilizaram assistentes de prova formais (especificamente o Lean 4) para verificar candidatos. Nesse paradigma, um "autoformalizador" traduz um problema e uma resposta candidata em uma declaração de teorema em Lean que afirma a correção da resposta. Um provador então tenta verificar essa declaração.

No entanto, um gargalo significativo existe: para verificar $K$ respostas candidatas, o autoformalizador deve ser invocado $K$ vezes de forma independente. Isso incorre em um custo computacional de $\Theta(K)$, que escala linearmente com o número de amostras. Os autores observam que, para um único problema, as $K$ declarações formais são quase idênticas, compartilhando a mesma estrutura de problema e diferindo apenas na expressão da resposta. O problema central é como explorar essa estrutura compartilhada para reduzir os custos de formalização de $\Theta(K)$ para $\Theta(1)$ sem sacrificar a precisão da seleção.

2. Metodologia: O Pipeline BASE

Os autores propõem o BASE (Base-and-Substitute-Edit), um pipeline projetado para formalizar um único candidato "base" e derivar as $K-1$ declarações restantes através de edição localizada.

2.1 Descoberta da Base

O pipeline começa com um resolvedor (solver) de nível superior gerando uma lista ranqueada de $K$ respostas candidatas, $S(x) = (a_1, \dots, a_K)$, ordenada pela confiança do solver.

• O sistema itera através dos candidatos em ordem de ranking.
• Para cada candidato $a_i$, ele tenta formalizar o par problema-resposta $(x, a_i)$ em uma declaração Lean $F_i$.
• O processo para no primeiro candidato $a_b$ cuja formalização $F_b$ consegue realizar a checagem de tipos (type-check) com sucesso no Lean.
• $F_b$ torna-se a formalização base, e $a_b$ é a resposta base.
• Se nenhum candidato passar na checagem de tipos, o sistema recorre ao candidato de maior ranking, $a_1$.

2.2 Cascata de Substituição

Uma vez estabelecida uma base válida $F_b$, o sistema gera as $K-1$ declarações restantes editando $F_b$ no local para refletir os outros candidatos. Isso é tratado por uma cascata de dois níveis:

1. Nível 1 (R1): Localização Direta Baseada em Regras

   • O sistema tenta localizar a expressão da resposta em $F_b$ via correspondência exata de strings dentro de uma "região de portão" (o corpo do teorema, excluindo comentários/cabeçalhos).
   • Se uma correspondência única for encontrada, o sistema realiza uma substituição direta da string da resposta.
   • Se ocorrerem múltiplas correspondências, um modelo de desambiguação pequeno seleciona o slot correto.
   • Este nível é eficiente, mas falha quando o autoformalizador codifica a resposta em uma forma sintaticamente diversa (por exemplo, uma tupla (3, 5) codificada como bindings separados ou um valor Prod) em vez de uma string literal.

2. Nível 2 (R2): LEANSCRIBE (Reescritor Aprendido)

   • Para casos onde o R1 falha, o sistema invoca o LEANSCRIBE, um LLM especializado e ajustado (fine-tuned).
   • Entrada: O problema $x$, a formalização base $F_b$ e a resposta base $a_b$.
   • Saída:
     • Um bloco local $s$: Um segmento contíguo de $F_b$ contendo a expressão dependente da resposta.
     • Uma função de preenchimento $f$: Uma função Python leve que mapeia qualquer resposta informal $a_i$ para a expressão Lean correspondente que substitui $s$.
   • Execução: O LEANSCRIBE roda uma vez por problema. A função gerada $f$ é então aplicada a todos os candidatos restantes $a_i$ para produzir suas declarações formais $F_i = f(a_i)$. Isso amortiza o custo da chamada do modelo entre todos os $K-1$ candidatos.

2.3 Verificação e Seleção

O pipeline depende da checagem de tipos ao nível da declaração como o principal sinal de seleção.

• Um candidato é considerado "verificado" se sua declaração formal $F_i$ passa na checagem de tipos no Lean (ou seja, é uma proposição bem formada).
• O sistema seleciona o candidato de maior ranking $a_j$ tal que $F_j$ passe na checagem de tipos.
• Se nenhum candidato passar na checagem de tipos, ele recorre ao primeiro colocado $a_1$.
• Os autores observam que, embora a verificação ao nível de prova (executando um provador) seja mais rigorosa, os provadores atuais possuem baixas taxas de pass@1, tornando a checagem de tipos ao nível da declaração um sinal mais prático para seleção neste cenário de orçamento restrito.

3. Principais Contribuições

1. Pipeline BASE: O primeiro trabalho a amortizar os custos de formalização ao compartilhar uma única declaração base verificada entre múltiplos candidatos, reduzindo as chamadas do autoformalizador de $\Theta(K)$ para $\Theta(1)$.
2. Modelo LEANSCRIBE: Um reescritor aprendido treinado para localizar blocos dependentes da resposta e gerar funções de edição reutilizáveis, lidando com variações sintáticas que a substituição baseada em regras não consegue tratar.
3. Melhoria de Pareto: O método alcança maior precisão de seleção enquanto reduz significativamente o custo computacional em todas as configurações testadas.

4. Resultados Experimentais

Os autores avaliaram o BASE em quatro benchmarks (MATH-500, OlympiadBench, AMC-AIMO, AIME 2024) usando três diferentes solvers de nível superior (Gemini 3 Pro, Qwen3-8B, DeepSeek-R1-Qwen3-8B) com $K=8$ candidatos.

• Precisão: O BASE melhorou a precisão de seleção (Acc) em todas as 12 configurações (dataset, solver) em comparação com a formalização independente, com ganhos variando de +0,7 a +23,3 pontos percentuais.
• Robustez: A taxa de "Passagem da Resposta de Ouro" (GT-pass) — a fração de problemas onde a declaração da resposta correta passa na checagem de tipos — aumentou significativamente (até +33,3 pontos), atingendo 96–100% em muitos casos. Isso indica que compartilhar uma base verificada torna a formalização da resposta correta mais robusta.
• Eficiência de Custo: Com $K=8$, o BASE reduziu o número de chamadas do autoformalizador em aproximadamente 5,4× (redução média de 4,7–6,5×). O custo escala como $\Theta(1)$ em vez de $\Theta(K)$.
• Ablação: Remover o reescritor aprendido (LEANSCRIBE) e depender apenas da substituição baseada em regras (R1) resultou em uma queda significativa na cobertura de candidatos (8–22 pontos percentuais), demonstrando a necessidade do componente aprendido para lidar com diversas codificações sintáticas.
• Análise de Nível de Prova: Mesmo quando utilizando um provador (DeepSeek-Prover-V2) com uma única tentativa por candidato, o BASE melhorou a precisão ao nível de prova em 11 de 12 configurações, sugerindo que declarações estruturadas de forma melhor auxiliam os provadores subsequentes.

5. Significância e Alegações

O artigo afirma que o BASE representa uma melhoria de Pareto para a seleção de respostas baseada em Lean. Ao formalizar uma vez e editar o restante, o método simultaneamente:

• Reduz o Custo: Diminui drasticamente o custo de inferência da verificação formal, tornando o escalonamento em tempo de teste com um grande $K$ mais viável.
• Melhora a Precisão: Aumenta a confiabilidade da seleção da resposta correta, provavelmente porque a estrutura base compartilhada reduz a variância e a taxa de falha do autoformalizador para o candidato correto.

Os autores enfatizam que esta abordagem é um "substituto direto" (drop-in replacement) para a etapa de formalização em pipelines existentes (demonstrado pela integração no pipeline FANS) e que os ganhos são impulsionados pela capacidade do verificador de reter respostas corretas de forma mais eficaz quando um arcabouço (scaffold) compartilhado e verificado é utilizado, em vez de mudanças no solver de nível superior.

O trabalho reconhece limitações, observando que foca na checagem de tipos ao nível da declaração devido às limitações atuais dos provadores e assume que as respostas candidatas compartilham uma estrutura do lado do problema. Não se propõe a resolver a fidelidade da autoformalização (onde uma resposta incorreta ainda pode passar na checagem de tipos), mas sugere que a combinação de sinais formais com rankings de solvers mitiga esse risco.