Faithful Autoformalization via Roundtrip Verification and Repair

Resumo Técnico: Autoformalização Fiel via Verificação de Volta e Reparo

Declaração do Problema
O artigo aborda uma lacuna crítica na autoformalização: a falta de um método confiável para verificar se um Modelo de Linguagem de Grande Escala (LLM) capturou fielmente o significado semântico de uma declaração em linguagem natural ao traduzi-la para uma representação formal verificável por máquina. Os métodos de avaliação existentes dependem de validade sintática ou de sucesso em tarefas downstream, o que não testa diretamente a fidelidade semântica. Além disso, quando ocorrem erros, as estratégias de reparo atuais limitam-se à regeneração ponta a ponta, carecendo da capacidade de diagnosticar onde no pipeline de tradução o significado foi perdido. Isso é particularmente desafiador em domínios como o direito estatutário, onde formalizações de verdade absoluta (ground-truth) não estão disponíveis.

Metodologia
Os autores propõem um Framework de Verificação de Volta e Reparo Delimitado que opera sem anotações de verdade absoluta. O mecanismo central envolve um pipeline de tradução em três etapas:

1. T1 (Autoformalização): Traduz a entrada em linguagem natural $x$ para uma expressão formal $y_{orig}$ em um formalismo alvo $\Sigma$.
2. T2 (Tradução Reversa): Traduz $y_{orig}$ de volta para linguagem natural $x'$.
3. T3 (Reformalização): Traduz $x'$ de volta para uma expressão formal $y_{rt}$.

Verificação: O sistema verifica a equivalência lógica entre a formalização inicial ($y_{orig}$) e a formalização de volta ($y_{rt}$) usando uma ferramenta formal (especificamente um solver SMT nos experimentos). Se $y_{orig} \equiv_\Sigma y_{rt}$, o pipeline é considerado autoconsistente.

Diagnóstico e Reparo: Quando a equivalência falha, o framework emprega um procedimento de diagnóstico baseado em etapas. Um juiz LLM examina os artefatos ($x, y_{orig}, x', y_{rt}$) para identificar a primeira etapa onde ocorreu desvio semântico (Etapa 1, 2 ou 3). Crucialmente, o diagnóstico é "delimitado", o que significa que a explicação é restrita a artefatos relevantes apenas para aquela etapa específica.

• Reparo Delimitado: Em vez de regenerar todo o pipeline, um operador de reparo direcionado ($R_i$) corrige apenas a etapa defeituosa identificada. As etapas downstream são então regeneradas para manter a coerência do pipeline.
• Loop Iterativo: Este processo repete-se até um orçamento fixo ($K=3$) até que a equivalência seja alcançada ou o orçamento seja esgotado.

Sinal Semântico Auxiliar: Para avaliar a qualidade semântica das formalizações independentemente do loop de reparo, os autores utilizam um modelo bidirecional de Inferência em Linguagem Natural (NLI). Isso serve como um diagnóstico post-hoc para medir o "desvio" (por exemplo, contradições ou falta de relação) entre o texto original e o texto reconstruído, distinguindo entre regras que são formalmente consistentes, mas semanticamente desviadas.

Principais Contribuições

1. Framework de Verificação de Volta: Um método para sinalizar a fidelidade da autoformalização sem formalizações de verdade absoluta, aplicável a qualquer formalismo que admita uma verificação de equivalência (por exemplo, SMT, verificadores de tipos).
2. Reparo Delimitado Guiado por Diagnóstico: Um procedimento que localiza erros em etapas específicas de tradução, permitindo correções direcionadas em vez de regeneração completa e custosa do pipeline.
3. Análise Empírica de Gargalos: Um estudo em dois domínios estatutários (Código de Transporte do Texas e Código de Parques e Vida Selvagem do Texas) e duas famílias de modelos (Claude Opus 4.6 e GPT-5.2) identificando o passo de diagnóstico como o principal gargalo para o reparo delimitado, e não o pipeline ou os operadores de reparo em si.

Resultados
O framework foi avaliado em 150 regras de trânsito e 77 regras de vida selvagem.

• Eficácia do Reparo: O reparo delimitado guiado por diagnóstico alcançou as taxas mais altas de equivalência verificada ao menor custo quando a função de diagnóstico era confiável.
• Dependência do Modelo: Com o Claude executando o pipeline e o diagnóstico, o reparo delimitado superou as linhas de base (sem reparo, seleção aleatória de etapas, regeneração completa). No entanto, com o GPT, o passo de diagnóstico foi pouco confiável (fortemente enviesado para culpar a Etapa 1), fazendo com que o reparo delimitado tivesse desempenho inferior e se tornasse mais caro do que a regeneração completa.
• Intervenção entre Modelos: Substituir apenas o passo de diagnóstico do GPT pelo Claude (mantendo o GPT para o pipeline e o reparo) restaurou a eficiência e a eficácia do reparo delimitado, provando que a função de diagnóstico é a variável crítica.
• Previsão de Fidelidade: A equivalência formal é um forte preditor de fidelidade semântica. Regras que passaram na verificação de equivalência (UNSAT) mostraram 1,4× a 2,5× menos desvio NLI do que aquelas que falharam (SAT). No entanto, a equivalência formal é necessária, mas não suficiente; aproximadamente 16% das regras formalmente equivalentes ainda exibiram desvio semântico.

Significado e Alegações
O artigo alega que a equivalência formal serve como um sinal prático e livre de verdade absoluta para a fidelidade semântica na autoformalização. Demonstra que o reparo delimitado, impulsionado por um diagnóstico preciso em nível de etapa, é uma estratégia mais econômica e eficiente do que a regeneração completa. Os autores enfatizam que a confiabilidade da função de diagnóstico é o fator determinante para o sucesso dessa abordagem.

O trabalho é modesto em seu escopo, observando que o framework é heurístico e não garante correção contra a intenção original em linguagem natural (já que o pipeline poderia estabilizar em um ponto fixo semanticamente diferente). Os autores afirmam explicitamente que o sistema não é adequado para aplicações críticas de segurança sem revisão independente de especialistas e que a avaliação atual é limitada a texto estatutário em inglês, exigindo estudos adicionais para outros gêneros, como código ou texto científico.