Compilação em Lean superestima a precisão da formalização: diferença de até 29,5 p.p.

O Lean aceita uma declaração se ela estiver corretamente tipada. O que ela significa, o compilador não verifica. Os autores do trabalho «Beyond Compilation» mediram quanto a métrica «compilou» superestima a qualidade da autoformalização, isto é, da tradução de enunciados matemáticos da linguagem natural para o Lean. O número mais expressivo: o agente com ferramentas compila 87,2% dos 227 enunciados universitários, mas o critério semântico aprova só 57,7%. A diferença de 29,5 pontos percentuais corresponde a código Lean que parece impecável e formula algo diferente do que foi pedido.

Como funciona a verificação

A maioria das tarefas não tem uma tradução de referência em Lean, então não é possível comparar com uma resposta «de ouro». Os autores propõem um critério composto: o enunciado é aceito se compilar em Lean e se dois LLMs de famílias diferentes o considerarem, de forma independente, uma tradução fiel da formulação original.

O critério foi testado em uma auditoria aleatória independente. Ele coincidiu com a opinião da maioria dos anotadores humanos em 91,5% dos casos. Seus erros são assimétricos: raramente deixa passar uma tradução incorreta, mas rejeita parte das corretas. Ou seja, a avaliação é conservadora e tende a subestimar o resultado dos sistemas.

Principais resultados nos oito sistemas:

• diferença entre a fração de enunciados compilados e a de aceitos: de 1,3 a 29,5 p.p.;
• agente com ferramentas: 87,2% de compilação contra 57,7% de aceitação;
• humanos revisaram todas as rejeições do agente: 23,8 dos 29,5 p.p. eram erros reais de tradução;
• em seis dos sete sistemas de passagem única (one-shot), de 78% a 100% da diferença corresponde a erros reais de tradução, segundo a revisão em duas etapas feita por Claude Opus 5.5 com Lean e GPT-6.1 Sol, conferida com a anotação humana.

Quando o juiz erra

A parte mais inesperada diz respeito aos modelos novos. O GPT-5.2 foi um dos dois juízes. Os autores pediram que ele avaliasse as traduções de dois modelos mais recentes, GPT-6 Astra e Claude Opus 5.5. O juiz aceitou 83% dos enunciados de cada um. Já o resultado one-shot do próprio GPT-5.2 é de 21%.

Em seguida, a revisão em duas etapas analisou as rejeições desses dois modelos. Dos 54 enunciados rejeitados, apenas 4 eram erros reais de tradução, ou 7%. As demais rejeições foram falhas do juiz. Isso é coerente com uma lógica simples: quanto menos o sistema erra, menos erros genuínos aparecem entre suas rejeições e mais evidente fica o ruído do próprio juiz. Um juiz que não evolui junto com os modelos avaliados vira o gargalo do benchmark.

Para o setor, a conclusão é incômoda. Uma métrica baseada em LLM-juiz é quase justa com sistemas fracos, mas passa a subestimar a qualidade dos fortes. Não dá para comparar modelos de gerações diferentes com ela sem reverificar as rejeições.

O que a ablação de ferramentas mostrou

Os autores submeteram o agente a uma ablação 2^3, ligando e desligando três ferramentas nas oito combinações possíveis. O principal ganho de compilação vem do feedback do Lean: o agente vê os erros e corrige o código. Mas quase metade desse ganho não passa no critério semântico. O agente aprende a fazer o código compilar, não a preservar o sentido. Um efeito típico: para eliminar o erro, o enunciado perde uma condição, o quantificador é enfraquecido ou a estrutura é substituída.

O que mudar na prática

Se você constrói um pipeline de autoformalização ou treina um modelo com o sinal do Lean, usar a compilação como única recompensa produz uma estimativa enviesada e empurra o modelo para formulações degeneradas. É preciso ao menos uma camada semântica: juízes de famílias diferentes e verificação humana por amostragem das rejeições.

Ao trabalhar com modelos novos, vale checar se o juiz não ficou para trás em relação ao sistema avaliado. Se a maior parte das rejeições for erro do juiz, e não da tradução, é hora de rever a métrica. O código e os dados foram publicados no GitHub (grenadeComing/beyond-compilation), então a abordagem pode ser reproduzida com enunciados próprios.