Resumo Técnico: FaithformBench

Problema

Sistemas de autoformalização (AF) traduzem passos de raciocínio em linguagem natural para enunciados formais (ex: em Lean) para permitir a verificação por assistentes de prova. Um requisito crítico para esses sistemas, particularmente quando usados para verificar a Cadeia de Pensamento (CoT) de Grandes Modelos de Linguagem (LLMs), é a fidelidade (faithfulness): o output formal deve corresponder semanticamente ao input, preservando tanto estruturas lógicas válidas quanto inválidas.

Os métodos atuais para avaliar a fidelidade da AF enfrentam limitações significativas:

1. Dependência de Verdade Fundamental (Ground Truth): Datasets anotados por humanos (ex: BEq, GTED) são caros e lentos de produzir.
2. Juízes Automatizados Não Confiáveis: Juízes baseados em LLM ou modelos de embedding carecem de garantias de precisão robustas e podem falhar em detectar erros de formalização sutis.
3. Viés em Favor de Inputs Corretos: Benchmarks existentes tipicamente assumem que os inputs estão corretos. Eles falham em avaliar se um sistema de AF consegue preservar fielmente erros em inputs incorretos. Na verificação de CoT, o objetivo principal é frequentemente identificar passos de raciocínio incorretos; se um sistema de AF "corrige silenciosamente" um input inválido para um enunciado provável, ele anula o propósito da verificação.

Metodologia

Os autores propõem o FaithformBench, um benchmark projetado para avaliar a fidelidade da AF ao testar explicitamente dois modos de falha:

1. Indução de Erro: Um input válido é mapeado para um enunciado formal falso.
2. Correção Silenciosa: Um input inválido é mapeado para um enunciado formal verdadeiro (uma forma de sicofancia).

Abordagem Principal

A metodologia baseia-se na validação por perturbação em vez de verdade fundamental anotada por humanos:

1. Construção do Dataset: Partindo do ProcessBench (uma coleção de cadeias de CoT corretas e verificadas por humanos), os autores extraem passos de raciocínio individuais ($x_i$).
2. Perturbação: Uma função de perturbação ($Pert$) gera contrapartes inválidas ($\bar{x}_i$) modificando sutilmente passos válidos (ex: alterando um valor numérico ou um operador lógico) para torná-los matematicamente falsos.
3. Verificação: Um sistema de AF gera enunciados formais tanto para $x_i$ quanto para $\bar{x}_i$. Um provador confiável (DeepSeek-Prover-V2) tenta:
   • Provar o enunciado derivado de $x_i$ (Esperado: Sucesso).
   • Refutar o enunciado derivado de $\bar{x}_i$ (Esperado: Sucesso).
4. Métricas: Os autores definem três estatísticas principais:
   • FNR (Taxa de Falsos Negativos): A taxa na qual inputs válidos são formalizados em enunciados não prováveis (falsos) (Indução de Erro).
   • FPR (Taxa de Falsos Positivos): A taxa na qual inputs inválidos são formalizados em enunciados prováveis (verdadeiros) (Correção Silenciosa).
   • AFFR (Taxa de Falha de Autoformalização): A taxa de falhas sintáticas ou timeouts.
   • UFLB (Limite Inferior de Infidelidade): Uma métrica composta que estima o limite inferior do comportamento infiel, calculada como $UFLB = \frac{1}{2}FNR + \frac{1}{2}FPR + AFFR$.

Esta abordagem é sólida sob suposições fracas: se o provador refuta com sucesso a formalização de um input perturbado, a AF foi fiel; se ele o prova, a AF realizou uma correção silenciosa. Não requer formalizações anotadas por humanos.

Principais Contribuições

1. Formalização da Fidelidade: Os autores definem a fidelidade para abranger tanto a preservação da validade quanto da invalidade, identificando a "indução de erro" e a "correção silenciosa" como modos de falha distintos e detectáveis.
2. Metodologia Escalável: Eles introduzem um método de propósito geral e baixo custo para estimar a prevalência desses modos de falha sem necessidade de verdade fundamental anotada por humanos, baseando-se, em vez disso, em perturbação automatizada e busca de prova.
3. Benchmark FaithformBench: Um dataset de 12.784 passos de raciocínio (e seus respectivos contrapartes perturbados) através de quatro datasets matemáticos (GSM8K, MATH, OlympiadBench, Omni-MATH) de dificuldade crescente.
4. Avaliação Abrangente: O benchmark é utilizado para avaliar oito sistemas de AF: quatro modelos especializados ajustados (Goedel, Herald, Kimina, StepFun) e quatro LLMs de fronteira de propósito geral (Claude Opus 4.7, GPT 5.2, Gemini 3.1 Pro, Qwen Plus).

Resultados Experimentais

A avaliação revela uma tensão pervasiva entre a preservação da validade e a preservação da invalidade:

• Sicofancia Pervasiva em Modelos Ajustados (Fine-Tuned): Modelos de AF especializados exibem altas taxas de correção silenciosa (FPR alto). Eles frequentemente "consertam" inputs inválidos para produzir teoremas prováveis.
  • Goedel, o modelo mais capaz de formalizar CoTs corretos (menor FNR), é também o mais sicofante (maior FPR). Ele corrige silenciosamente inputs inválidos com mais frequência do que qualquer outro modelo.
  • Isso sugere que as estratégias atuais de ajuste fino (fine-tuning) implicitamente confundem "produzir um enunciado provável" com "traduzir fielmente o input".
• Modelos de Propósito Geral: LLMs de fronteira (ex: Claude Opus 4.7, Gemini 3.1 Pro) exibem taxas significativamente menores de correção silenciosa (menor FPR) comparadas aos modelos especializados. Embora possam ter taxas de falha de AF (AFFR) ligeiramente maiores devido a janelas de contexto menores ou falta de treinamento específico, eles são mais fiéis ao valor de verdade do input, preservando erros quando eles existem.
• Análise de Contingência: A análise de pares não perturbados vs. perturbados mostra que, para modelos especializados, as categorias "Fidelidade" e "Sicofancia" dominam, muitas vezes diminuindo juntas conforme a dificuldade do dataset aumenta.

Significância e Alegações

O artigo afirma que o FaithformBench fornece uma ferramenta de diagnóstico necessária para o pipeline de verificação de CoT. O achado principal é que os sistemas de AF mais "bem-sucedidos" (aqueles que melhor formalizam o raciocínio correto) são frequentemente os menos fiéis no que diz respeito à preservação de erros.

• A Tensão: Existe um trade-off fundamental nos sistemas de AF atuais: otim-izar para a capacidade de produzir enunciados prováveis leva à supressão de erros no input.
• Implicação para Verificação: Em aplicações onde o objetivo é identificar passos de raciocínio incorretos (ex: verificar CoTs de LLMs), usar AFs altamente ajustados que corrigem silenciosamente erros é contraproducente. Os autores argumentam que, para tarefas de verificação, preservar a invalidade é tão crucial quanto preservar a valididade.
• Direção Futura: Os autores sugerem que abordar essa tensão requer treinar sistemas de AF com exposição deliberada a inputs inválidos, ensinando-os a preservar erros em vez de repará-los. Eles também propõem estender esta metodologia de perturbação para outras tarefas de tradução de natural-para-formal.

O artigo conclui modestamente, observando que, embora seu método detecte a indução de erro e a correção silenciosa de forma sólida, ele não captura totalmente o "desvio semântico" (onde o output não é nem provável nem refutável, mas está semanticamente desalinhado). Portanto, recomendam que o FaithformBench seja usado como uma medida diagnóstica ao lado de outras métricas, em vez de um certificado completo de confiabilidade.