Resumo Técnico: O Hiato de Fidelidade na Autoformalização por LLM

1. Definição do Problema: O Hiato de Fidelidade

Os sistemas modernos de autoformalização, que traduzem matemática em linguagem natural (LN) para assistentes de prova formais (ex: Lean 4, Isabelle/HOL), são atualmente limitados não pela fluência da tradução, mas pela fidelidade. Embora uma afirmação formal gerada possa ser sintaticamente bem formada (passar no typecheck) e até mesmo provável, ela pode codificar um teorema semanticamente distinto da afirmação original em LN.

Os autores identificam isso como o hiato de fidelidade. Diferente do código, onde testes unitários fornecem um oráculo executável, a formalização matemática carece de uma ponte direta entre a LN (interpretada sob convenções tácitas) e a lógica formal (interpretada sob teoria de tipos dependentes). Métricas de avaliação padrão — como pontuações BLEU contra uma referência, verificações pontuais de especialistas ou sucesso de prova downstream — falham em detectar falhas "insidiosas" onde a formalização é fluente e provável, mas semanticamente errada.

O artigo formaliza este problema via uma distribuição de interpretação ($D_N$), representando o conjunto de afirmações formais que matemáticos competentes aceitariam como expressando uma determinada afirmação em LN $N$. Uma formalização candidata $F$ é $\epsilon$-fiel se for provadamente equivalente a $1-\epsilon$ das afirmações em $D_N$. Os autores categorizam o desvio semântico em quatro classes canônicas:

1. $\Delta\forall$ (Inversão de Quantificador): Troca da ordem dos quantificadores (ex: $\forall x \exists y$ vs. $\exists y \forall x$).
2. $\Delta H$ (Omissão de Hipótese): Dropar uma premissa, tornando a afirmação formal estritamente mais forte do que o pretendido.
3. $\Delta C$ (Generalização de Conclusão): Fortalecer a conclusão de tal forma que $F \Rightarrow N$, mas $N \not\Rightarrow F$.
4. $\Delta T$ (Coerção de Tipo): Reetiquetagem silenciosa de tipos (ex: $\mathbb{R} \to \mathbb{Q}$), frequentemente a mais difícil de detectar sintaticamente.

2. Metodologia: Assinatura de Provabilidade Bidirecional (BPF)

A contribuição central é a Assinatura de Provabilidade Bidirecional (BPF - Bidirectional Provability Fingerprinting), um framework sem referência que certifica a fidelidade comparando os "vizinhanças de consequência" da afirmação em LN e da formalização candidata.

2.1. O Mecanismo Central

A BPF opera no insight de que o significado de uma afirmação é definido pelo que ela implica e pelo que a implica.

• Assinatura Direta ($\Phi^+_F$): O conjunto de sondas (probes) implicadas pelo candidato $F$.
• Assinatura Reversa ($\Phi^-_F$): O conjunto de sondas que implicam $F$.
• Equivalência: Duas afirmações são semanticamente equivalentes se suas assinaturas direta e reversa coincidem sobre um conjunto suficientemente rico de sondas.

O pipeline envolve:

1. Geração de Sondas: Sintetizar um conjunto de sondas semânticas ($P$) a partir da afirmação em LN $N$.
2. Autoformalização: Converter essas sondas em afirmações formais.
3. Verificação de Implicação: Usar um assistente de prova (Lean 4 + mathlib4) como um oráculo para computar as relações de implicação entre $F$ e as sondas.
4. Comparação de Assinaturas: Comparar a assinatura do candidato contra a assinatura prevista derivada de $N$.

2.2. Componentes Principais

O framework introduz quatro componentes inovadores para aumentar a detecção e a eficiência:

1. Geração de Sondas Contrafatuais (CPG):
   Em vez de amostragem genérica, a CPG utiliza um procedimento contrastivo. Ela gera mecanicamente "gêmeos desviados" ($N^D$) para cada uma das quatro classes de desvio (ex: trocando quantificadores). Um LLM é então instruído a gerar sondas que especificamente distingam $N$ de $N^D$. Isso visa os modos de falha específicos que o certificador pretende detectar.

2. O Espectro de Equivalência ($E(F, N)$):
   Substituindo vereditos binários frágeis (Fiel/Desviado) por uma pontuação contínua em $[0, 1]$. Esta pontuação é calibrada contra anotações de especialistas para definir três regiões de decisão:

   • ACEITAR (ACCEPT): $E \ge 0.93$
   • REVISAR (REVIEW): $0.78 \le E < 0.93$ (requer triagem humana)
   • REJEITAR (REJECT): $E < 0.78$

3. Alocação Adaptativa de Orçamento de Sondas (APBA):
   Um roteador de teoria da informação que aloca dinamicamente o "orçamento de tática" (tempo/custo de busca de prova) limitado. A APBA seleciona sondas que maximizam a redução esperada de entropia em relação ao status de desvio, em vez de amostrar uniformemente. Isso alcança a mesma precisão de detecção com significativamente menos sondas.

4. Decodificação Guiada pela Fidelidade (FGD):
   Um loop de feedback onde as pontuações BPF são usadas como um sinal de recompensa durante o processo de autoformalização. Em uma configuração de amostragem e reclassificação (sample-and-rerank), os candidatos são pontuados por BPF. Se os principais candidatos caírem nas zonas "REVISAR" ou "REJEITAR", a "sonda testemunha" de maior pontuação (a sonda específica que revelou o desvio) é alimentada de volta ao LLM como uma dica de contexto para reparar o erro.

3. Garantias Teóricas

O artigo fornece dois resultados teóricos principais:

• Teorema de Detecção de Desvio: Prova que para qualquer classe de desvio específica $D$, se o gerador de sondas tiver uma "taxa de testemunhabilidade" ($\alpha$) não nula, a BPF pode detectar o desvio com probabilidade $1-\delta$ usando um orçamento de sondas de $k \ge \frac{1}{\alpha} \log(1/\delta)$.
• PAC-Fidelidade: Estabelece que a classe de equivalência de uma afirmação em LN é aprendível de $O(\log(1/\delta)/\epsilon)$ sondas, assumindo que a distribuição de sondas possa testemunhar qualquer desvio alcançável.

Os autores também reconhecem limitações: a BPF não pode detectar desvio de convenção (onde a notação muda, mas o conteúdo lógico permanece idêntico) e depende da completude do oráculo de prova (provas incompletas podem levar a falsos negativos).

4. Resultados Experimentais

Os autores lançaram o DRIFTBENCH, um benchmark de 2.183 pares LN/Lean 4 com rótulos de desvio controlados através de seis subcampos matemáticos.

Desempenho de Detecção:

• BPF + CPG detecta 89,6% das formalizações desviadas com uma taxa de falso-positivo de 3,0%.
• Isso supera significativamente os baselines:
  • Apenas typecheck: 11,4% de detecção.
  • Provabilidade (flag de improvabilidade): 41,2% de detecção.
  • LLM-judge (verificação direta de fidelidade): 63,3% de detecção.
  • Back-translation: 58,9% de detecção.
• APBA reduz o custo computacional (tempo de execução) em 3,2× em comparação com a amostragem uniforme, mantendo as taxas de detecção.

Impacto do FGD:
Quando aplicado como um passo de pós-processamento a um autoformalizador de última geração, o FGD reduziu a taxa de afirmações emitidas com desvio de 19,4% para 10,3% (uma redução relativa de 47%), principalmente ao re-instruir sobre erros de omissão de hipótese e generalização de conclusão.

5. Significância e Alegações

O artigo alega que o hiato de fidelidade é o principal gargalo para a autoformalização confiável em escala para bibliotecas matemáticas completas. A significância deste trabalho reside em:

1. Certificação Sem Referência: Fornece um método para verificar a fidelidade sem exigir uma formalização "padrão ouro", que muitas vezes está indisponível.
2. Operacionalização de Semântica: Desloca o paradigma de avaliação da sobreposição sintática (BLEU) ou provabilidade para a semântica inferencial (vizinhanças de consequência), alinhando-se com a semântica de prova.
3. Escalabilidade: Ao introduzir a APBA e o Espectro de Equivalência, oferece uma ferramenta de triagem prática e de baixo custo que pode priorizar a revisão por especialistas humanos em vez de substituí-los.
4. Benchmarking: O DRIFTBENCH é apresentado como o primeiro benchmark com rótulos de desvio controlados, permitindo a avaliação sistemática da fidelidade, em vez de apenas da capacidade de prova.

Os autores posicionam a BPF não como uma solução perfeita que elimina todos os erros (notando especificamente a limitação em relação ao desvio de convenção), mas como um passo concreto para fechar o hiato de fidelidade, permitindo a integração segura de matemática gerada por IA em bibliotecas rigorosas.