Resumo Técnico: ForEx – Um Framework de Verificação Formal para Raciocínio Explicável na Detecção de Falácias Lógicas

1. Definição do Problema

As avaliações atuais de Grandes Modelos de Linguagem (LLMs) na detecção de falácias lógicas baseiam-se predominantemente na precisão da predição (corretude do rótulo). No entanto, essa abordagem falha em verificar se o raciocínio fornecido pelo modelo realmente sustenta o rótulo previsto. Predições corretas podem advir de correlações superficiais em vez de uma derivação lógica genuína, enquanto predições incorretas podem ser acompanhadas por um raciocínio que é formalmente sólido sob uma interpretação específica, mas que diverge das anotações humanas.

Além disso, abordagens simbólicas existentes (ex: NL2FOL) tipicamente formalizam o argumento de entrada para verificar a satisfatibilidade, em vez de formalizar a cadeia de raciocínio gerada pelo modelo. Adicionalmente, as práticas de anotação padrão frequentemente comprimem variações interpretativas em rótulos "gold" únicos, o que pode obscurecer leituras alternativas plausíveis de um argumento. Há uma carência de um framework que analise conjuntamente os rótulos previstos, as explicações geradas e a derivabilidade formal dessas explicações.

2. Metodologia: O Framework ForEx

Os autores propõem o ForEx (Formal Verification for Explainable Reasoning), um framework que traduz as explicações em linguagem natural geradas por LLMs para Lean4 (um assistente de prova formal) para verificar se o racional traduzido é derivável sob premissas codificadas. O fluxo de trabalho consiste em três estágios:

A. Geração de Candidatos de Raciocínio

Um modelo "Reasoner" recebe uma afirmação de entrada e gera até $k$ candidatos. Cada candidato é uma tupla $(f_i, a_i, s_i)$ contendo:

• $f_i$: O tipo de falácia lógica prevista.
• $a_i$: A explicação em linguagem natural (racional).
• $s_i$: A estrutura em Lean4 que formaliza a explicação.

Um "Modifier" converte $s_i$ em código Lean4 inicial.

B. Feedback de Execução e Verificação Lean4

Este estágio emprega um loop de reparo iterativo para garantir que o código Lean4 gerado compile:

1. Tentativa de Compilação: O "Executor" tenta compilar o código Lean4.
2. Loop de Feedback: Se a compilação falhar (estado F), o Executor recebe a mensagem de erro e a explicação original $a_i$ para revisar o código.
3. Restrições: As revisões são estritamente limitadas à explicação original e ao código inicial para evitar o desvio semântico (semantic drift); o Executor não pode introduzir novo conteúdo lógico.
4. Terminação: O loop continua até que o código compile com sucesso (estado T) ou até que o máximo de iterações de reparo ($iter_{max}$) seja esgotado.

C. Avaliação de Consistência de Rótulo

O framework introduz a Matriz de Verificação de Argumento de LLM para desacoplar a corretude do rótulo da status de verificação formal. A matriz classifica as saídas em quatro quadrantes baseados em dois eixos:

1. Verificação Lean4: Passou (compila) vs. Falhou (não compila).
2. Consistência de Rótulo: Correspondência (predição igual à anotação humana) vs. Incorrespondência.

As quatro categorias resultantes são:

• Compilável-Correto (CC): Passou & Correspondência.
• Compilável-Alternativo (CA): Passou & Incorrespondência (indica uma cadeia de raciocínio formalmente válida que sustenta um rótulo diferente da anotação humana).
• Não Compilável-Correto (UC): Falhou & Correspondência.
• Não Compilável-Incorreto (UI): Falhou & Incorrespondência.

D. Pipeline de Anotação Guiada por Consenso

Para lidar com a ambiguidade da anotação, os autores propõem um pipeline que:

1. Representa modelos e anotações humanas como vetores multi-hot sobre categorias de falácias.
2. Utiliza Análise de Componentes Principais (PCA) e distância de Mahalanobis para identificar e filtrar modelos discrepantes (outliers).
3. Calcula distâncias de Jaccard pareadas para identificar afirmações de "alto consenso" (baixa discordância).
4. Augmenta as anotações para afirmações de alto consenso se pelo menos 50% dos modelos retidos atribuírem um rótulo específico sob verificação formal.

3. Principais Contribuições

1. Framework ForEx: Um sistema inovador que traduz explicações geradas por LLM para Lean4, permitindo uma análise verificável por máquina de cadeias de raciocínio formalizadas, em vez de apenas argumentos de entrada.
2. Matriz de Verificação de Argumento de LLM: Uma métrica que separa a consistência do rótulo do status de verificação formal, expondo casos onde modelos fornecem raciocínios formalmente deriváveis que contradizem as anotações humanas existentes (a categoria "Compilável-Alternativo").
3. Pipeline de Anotação Guiada por Consenso: Um método que combina padrões humanos, acordo entre múltiplos LLMs e verificação formal para apoiar a análise de anotação e a augmentação conservadora de rótulos, tratando a discordância de anotação como um sinal de variação interpretativa em vez de ruído.

4. Resultados Experimentais

O framework foi avaliado no conjunto de dados LOGIC-Climate (1.074 instâncias, 13 categorias de falácias), usando um subconjunto amostrado de 10% e 15 modelos Reasoner diferentes (incluindo variantes de pensamento/thinking e não-pensamento).

• Sucesso de Compilação: A taxa média de passagem para compilação em Lean4 aumentou de 36,70% (inicial) para 98,65% após quatro iterações de reparo. A maioria dos ganhos ocorreu após a primeira iteração.
• Verificação vs. Acordo de Rótulo:
  • A taxa combinada de Compilável-Correto (CC) + Compilável-Alternativo (CA) foi consistentemente alta, excedendo 90% para a maioria dos modelos (atingindo o pico de 97,59%). Isso indica que a vasta maioria das saídas de LLM pode ser traduzida em cadeias de raciocínio formal que passam na verificação.
  • No entanto, a taxa CC (acordo com os rótulos humanos) foi significativamente menor, variando aproximadamente entre 17% e 23% entre os principais modelos.
  • A taxa CA foi dominante, sugerindo que muitas cadeias de raciocínio formalmente verificadas sustentam rótulos diferentes das anotações humanas.
• Análise de Erro:
  • As taxas de Não Compilável-Correto (UC) foram muito baixas (<2%), indicando que rótulos corretos raramente surgem sem uma cadeia de raciocínio verificável neste cenário.
  • Falhas Não Compiláveis-Incorretas (UI) foram frequentemente causadas por predições de "Nenhuma Falácia" (NF), potencialmente causadas pela falta de contexto em entradas de frase única isoladas.
• Augmentação de Anotação: O pipeline guiado por consenso identificou um subconjunto de afirmações de alto consenso. As anotações aumentadas alcançaram um recall de 0,77 em relação às anotações humanas originais, preservando a maioria dos rótulos originais enquanto adicionava alternativas formalmente suportadas.

5. Significância e Alegações

O artigo afirma que o ForEx move a avaliação de LLMs além da simples corretude de rótulo em direção a uma análise verificável por máquina de cadeias de raciocínio formalizadas.

• Lacuna Sistemática: Os resultados expõem uma lacuna sistemática entre a derivabilidade formal e o acordo de rótulo. A alta prevalência de saídas "Compilável-Alternativo" sugere que as anotações humanas existentes podem não capturar totalmente as interpretações plausíveis de argumentos de entrada, ou que os modelos estão raciocinando corretamente sob diferentes premissas.
• Além da Predição: O framework demonstra que um modelo pode fornecer uma cadeia de raciocínio que é formalmente válida (derivável sob premissas codificadas) mesmo que discorde do rótulo "gold". Essa distinção é invisível para as métricas padrão baseadas em predição.
• Utilidade da Anotação: O ForEx é apresentado não apenas como uma ferramenta de verificação, mas como um mecanismo para análise de anotação downstream. Ele pode identificar casos onde os rótulos gold podem ser insuficientes ou onde múltiplas interpretações válidas existem, apoiando a augmentação de datasets com rótulos alternativos baseados em consenso.

Os autores permanecem modestos quanto às implicações, observando que a verificação formal em Lean4 certifica a derivabilidade sob premissas codificadas, mas não garante o alinhamento semântico com a afirmação original em linguagem natural. Eles reconhecem que a linguagem natural carece de uma base semântica totalmente especificada e, portanto, os resultados formais podem superestimar a capacidade do modelo se a formalização em si for imperfeita. Um trabalho futuro é proposto para melhorar o alinhamento entre os resultados de verificação e a correção semântica, incorporando estruturas de argumento e informações de contexto mais ricas.