Resumo Técnico: Além da Compilação: Avaliando a Formalização Fiel de Enunciados de Linguagem Natural para Lean

1. Definição do Problema

O artigo aborda a tarefa de formalização de enunciados de linguagem natural para Lean: traduzir automaticamente enunciados matemáticos informais em declarações de teoremas válidas em Lean 4. Esta tarefa é distinta da prova de teoremas. Em benchmarks de prova de teoremas (ex: MiniF2F, LeanDojo), o enunciado formal é fixo e confiável; o objetivo do sistema é gerar uma prova aceita pelo verificador. Na formalização de enunciados, o sistema deve gerar o próprio enunciado.

O desafio central é que a compilação é uma condição necessária, mas insuficiente para o sucesso. Uma declaração em Lean pode ser tipada (compilar) enquanto:

• Omite hipóteses críticas.
• Altera o domínio de discurso.
• Fortalece ou enfraquece a afirmação.
• Codifica uma versão vazia do resultado.

Trabalhos anteriores frequentemente se basearam em taxas de compilação ou métricas de equivalência baseadas em referência (ex: BEq, back-translation). Este artigo argumenta que a compilação por si só cria um "hiato de compilação-passagem" onde os sistemas parecem bem-sucedidos, mas falham em preservar o sentido matemático pretendido. Os autores definem o problema central como a avaliação da formalização fiel de enunciados: gerar declarações que tanto compilem quanto preservem a intenção semântica do input de linguagem natural.

2. Metodologia

2.1 Construção do Benchmark

Os autores curaram um benchmark de nível de pós-graduação consistindo de 400 enunciados de linguagem natural derivados de notas de aula e livros didáticos de código aberto em LaTeX. O conjunto de dados é equilibrado entre quatro domínios:

• Análise Real (100 entradas)
• Análise Complexa (100 entradas)
• Topologia (100 entradas)
• Álgebra (100 entradas)

Crucialmente, estes enunciados não possuem declarações Lean de referência (gold), garantindo que a tarefa represente uma tradução genuína em vez de recuperação.

2.2 Protocolo de Avaliação

O artigo propõe uma métrica de Consenso de LLM-como-Juiz, calibrada por especialistas humanos, para avaliar a fidelidade. O protocolo envolve duas etapas:

1. Verificação do Compilador: Qualquer código que falhe ao compilar é imediatamente considerado infiel.
2. Consenso Semântico: Para códigos que compilam, dois juízes de LLM independentes (GPT-5.2 e Gemini-2.5-Pro) comparam a declaração Lean gerada contra o enunciado original em linguagem natural. Eles atribuem uma pontuação de fidelidade (0–10).
   • Métrica de Sucesso: Uma tradução é considerada Fiel se, e somente se, ela compilar E ambos os juízes atribuírem uma pontuação $\ge 9$.
   • Esta abordagem de consenso estrito é desenhada como um ponto de operação conservador para comparação de sistemas, não como uma prova formal de equivalência.

2.3 Calibração Humana

Para validar a métrica automatizada, os autores realizaram auditorias humanas:

• Consenso-Positivo: 96,0% das saídas rotuladas como fiéis pelo consenso estrito foram confirmadas como fiéis por revisores humanos.
• Consenso-Negativo (Compilação-Passagem): 82,4% das saídas que compilaram, mas foram rejeitadas pelo consenso, foram confirmadas como falhas semânticas genuínas por humanos.
  Isso confirma que a métrica é um filtro de alta precisão e conservador que identifica efetivamente o desvio semântico.

2.4 Configuração Experimental: Design Fatorial

Os autores avaliaram vários sistemas (LLMs de propósito geral, formalizadores especializados, modelos orientados à prova e agentes aumentados por ferramentas) usando um design fatorial $2^3$ para decompor os efeitos de três intervenções comuns:

1. Rascunho de Especialista Paramétrico (T): Usar um modelo ajustado (Herald) para gerar um rascunho inicial.
2. Busca de Conhecimento (S): Usar ferramentas para consultar a Mathlib (busca de símbolos, resolução de namespace) e realizar buscas na web para fundamentação.
3. Feedback de Elaboração de Lean (F): Usar um REPL para compilar o código iterativamente e receber mensagens de erro para reparo.

A arquitetura do agente usa um orquestrador central (GPT-5.2) que mantém o estado e decide quais ferramentas invocar com base na configuração.

3. Resultados Principais

3.1 O Hiato de Compilação-Passagem

A descoberta empírica mais significativa é a divergência entre as taxas de compilação e a fidelidade semântica:

• Um agente de tempo integral aumentado por ferramentas alcançou uma taxa de compilação de 89,5%.
• No entanto, sob a métrica de consenso estrito, apenas 60,5% das saídas foram consideradas fiéis.
  Isso deixa um hiato de 29,0 pontos onde as saídas compilam, mas falham nos testes semânticos. Auditorias humanas confirmaram que a maioria desses casos de "compilação-passagem, consenso-negativo" são falhas semânticas reais (ex: falta de hipóteses, afirmações vazias).

3.2 Desempenho dos Modelos

• Formalizadores Especializados e Modelos de Prova: Formalizadores de enunciados dedicados (ex: Herald, Kimina-Autoformalizer) e modelos orientados à prova (ex: Goedel-Prover, Kimina-Prover) tiveram um desempenho ruim na geração de enunciados quando o alvo formal não era fornecido. Suas taxas de fidelidade variaram de 4,0% a 12,3%.
• LLMs de Propósito Geral: LLMs de propósito geral de disparo único (one-shot) atingiram 19,8–28,0% de fidelidade.
• Agentes Aumentados por Ferramentas: O framework de agente completo superou significativamente os baselines de disparo único, atingindo 60,5% de fidelidade. No entanto, diferentes orquestradores (Sonnet 4.5, Gemini-2.5-Pro) convergiram para níveis de desempenho semelhantes (60–65%) apesar de diferentes baselines, sugerindo que os ganhos são estruturais à abordagem aumentada por ferramentas e não específicos ao modelo orquestrador.

3.3 Decomposição Fatorial de Intervenções

O estudo isolou o impacto das três ferramentas:

• Feedback de Elaboração (F): Foi o maior motor de validade (compilação), aumentando significativamente a taxa de compilação. No entanto, também expandiu o balde de "compilação-passagem, mas infiel", pois permitiu que mais enunciados sintaticamente corretos, porém com desvio semântico, passassem.
• Busca (S): A busca melhorou primariamente a fundamentação e seletividade. Ela reduziu o hiato de compilação-passagem (ou seja, ajudou a filtrar enunciados semanticamente incorretos que conseguiram compilar) e melhorou a eficiência ao reduzir o número de iterações de REPL necessárias. Seu benefício marginal foi maior quando o feedback estava ausente.
• Rascunho de Especialista (T): O rascunho prévio de fine-tuning foi amplamente substituível uma vez que o feedback e a fundamentação estavam disponíveis. Na verdade, com feedback total, o rascunho prévio prejudicou levemente o desempenho, sugerindo que um orquestrador forte com feedback do compilador pode superar um rascunho especializado neste stack de ferramentas específico.

3.4 Variações de Domínio

• Análise Complexa mostrou os maiores ganhos com o feedback do compilador (+54,2 pontos em fidelidade), provavelmente devido à cobertura madura da Mathlib.
• Análise Real e Álgebra mostraram ganhos menores, indicando suporte limitado da biblioteca ou maior dificuldade intrínseca de formalização.
• Topologia exibiu desafios específicos com conceitos avançados (ex: espaços de recobrimento), onde o feedback frequentemente levava a enunciados válidos, mas semanticamente deslocados.

4. Significância e Alegações

O artigo alega que a formalização de enunciados deve ser avaliada como preservação de significado, não meramente como aceitação pelo Lean. As principais contribuições são:

1. Uma Nova Métrica: Uma métrica baseada em consenso e calibrada por humanos, que expõe o "hiato de compilação-passagem", revelando que muitos sistemas geram enunciados sintaticamente válidos, mas semanticamente incorretos.
2. Decomposição Diagnóstica: Uma análise fatorial mostrando que as ferramentas não são adições monótonas. Enquanto o feedback corrige a sintaxe, ele pode obscurecer erros semânticos; a busca melhora a fundamentação, mas tem retornos decrescentes quando o feedback está presente; e o rascunho especializado não é sempre necessário em um loop rico em feedback.
3. Comparação de Sistemas: Evidência de que os modelos atuais orientados à prova e formalizadores especializados não transferem automaticamente suas capacidades de prova para a geração de enunciados semanticamente fiéis sem treinamento explícito centrado em enunciados ou protocolos aumentados por ferramentas.

Os autores concluem que os sistemas futuros devem parear um feedback forte do Lean com avaliação semântica e políticas que decidam quando buscar, reparar ou parar, em vez de depender apenas de ganhos de precisão média. O artigo evita explicitamente alegar que sua métrica é uma prova formal de equivalência, posicionando-a, em vez disso, como uma fronteira de decisão conservadora e escalável para comparação de sistemas.