Resumo Técnico: SymDiag – Diagnóstico Explicável para o Raciocínio de LLMs via Verificação Neuro-Simbólica

1. Declaração do Problema

Modelos de Linguagem de Grande Escala (LLMs) demonstraram fortes capacidades de raciocínio de múltiplos passos, mas suas Cadeias de Pensamento (CoT - Chain-of-Thought) frequentemente sofrem de uma lacuna crítica entre a correção do resultado e a validade do processo. Um modelo pode chegar à resposta final correta através de etapas intermediárias não fiéis, incluindo lógica inconsistente, suposições ocultas ou transformações que não implicam o resultado.

Os métodos de verificação existentes falham em fornecer insights diagnósticos necessários para reparos direcionados:

• Verificação baseada apenas no resultado (Correspondência de Resposta): Pode apenas detectar se a resposta final está correta ou incorreta, falhando em localizar erros em derivações longas ou identificar traços fiéis, porém corretos.
• LLM-como-Juiz (LLM-as-Judge): Fornece críticas em linguagem natural que são subjetivas, inconsistentes e difíceis de auditar ou converter em ações de reparo específicas.
• Recompensas Escalares (PRMs/RMs): Reduzem modos de falha ricos a um único escore, oferecendo pouca orientação sobre onde ou por que uma derivação falhou.
• Abordagens Neuro-Simbólicas: Embora métodos como Logic-LM ou SymbCoT introduzam estruturas simbólicas, eles frequentemente lutam para distinguir entre defeitos genuínos de raciocínio e artefatos de tradução neuro-simbólica (ex: ruído de parsing). Sem essa distinção, os verificadores podem "diagnosticar erroneamente" erros de tradução como falhas lógicas, levando a feedbacks pouco confiáveis.

O desafio central é ir além da pontuação ou do julgamento subjetivo em direção a um diagnóstico de falha estruturado que localize erros, atribua suas causas e produza evidências verificáveis para o reparo.

2. Metodologia: Estrutura SymDiag

O SymDiag é uma estrutura neuro-simbólica de dois estágios projetada para reformular a verificação de raciocínio como um problema de diagnóstico de falha explicável.

Estágio I: Diagnóstico de Falha Explicável

Este estágio transforma a CoT em linguagem natural em restrições simbólicas verificáveis e realiza a validação ao nível de passo.

1. Gerador Neuro-Simbólico (Codificação de Dupla Ramificação):
   Para mitigar a fragilidade da tradução, o sistema gera duas codificações simbólicas independentes para cada passo da CoT:

   • Ramificação de Tradução Formal: Compila o problema de entrada e a CoT em uma representação formal (usando Prolog como backend), normalizando entidades, predicados e relações.
   • Ramificação de Reafirmação Crítica: Reexpressa o passo da CoT em uma afirmação estritamente delimitada e explicitamente escopada para expor suposições ocultas antes de compilá-la em um segundo programa simbólico.
   • Objetivo: As codificações duplas reduzem o viés de tradução de caminho único e aumentam a robustez à variabilidade de paráfrase.

2. Auto-Auditor (Desentranhamento de Erros):
   Um componente crítico que distingue entre Erros de Tradução (artefatos da conversão neural-para-simbólica) e Erros de Raciocínio (defeitos lógicos genuínos).

   • Verificação de Consistência de Tradução: Compara fatos e restrições entre as duas ramificações. Grandes divergências sugerem ambiguidade de tradução.
   • Verificação de Crítica Lógica: Executa testes de sanidade leves (ex: contradições imediatas). Se uma falha desaparece sob reescritas mínimas e consistentes com o texto (ex: renomeação de variáveis), ela é atribuída à tradução, não ao raciocínio.
   • Saída: Uma atribuição binária ($ErroDeTradução$ vs. $ErroDeRaciocínio$) que filtra diagnósticos espúrios.

3. Verificação Simbólica ao Nível de Passo:
   Os estados simbólicos aprovados passam por verificações rigorosas:

   • Satisfatibilidade: Verifica se as premissas e restrições acumuladas são satisfatórias ($SAT(P_i \land C_i)$).
   • Implicação Local: Verifica se a afirmação do passo atual segue logicamente das premissas anteriores ($P_{i-1} \land C_{i-1} \models \phi_i$). Isso é operacionalizado pela verificação da não-satisfatibilidade da negação.
   • Geração de Evidência: Em caso de falha, o sistema gera evidências verificáveis, como contraexemplos, testemunhas de inconsistência (núcleos de insatisfatibilidade/unsat cores) e indicadores de premissa ausente.

Estágio II: Reparo Guiado pelo Diagnóstico

A saída do diagnóstico é convertida em feedback acionável para o LLM:

• Localização: Identifica índices falhos específicos na CoT.
• Atribuição: Atribui rótulos de erro (ex: erro aritmético, inferência inválida, premissa ausente).
• Estratégia de Reparo:
  • Patch Local: Se o defeito for isolado (ex: um erro de cálculo), o modelo é instruído a editar minimamente o passo específico.
  • Reescrita Global: Se a falha se propagar (ex: uma premissa ausente afetando passos posteriores), o modelo é instruído a reescrever o raciocínio a partir do ponto de falha mais precoce.

3. Principais Contribuições

1. Visão Centrada no Diagnóstico: Formaliza a verificação de raciocínio como um problema de diagnóstico de falha, visando localizar erros, atribuir causas e suportar o reparo direcionado, em vez de apenas pontuar resultados.
2. Desentranhamento Auto-Auditado: Introduz um mecanismo para separar explicitamente artefatos de tradução de falhas de raciocínio genuínas usando codificações simbólicas duplas e verificações de consistência entre ramificações, permitindo um diagnóstico confiável sob observabilidade parcial.
3. Pipeline Baseado em Evidências: Propõe um sistema de ciclo fechado que produz evidências diagnósticas verificáveis (contraexemplos, núcleos de insatisfatibilidade) para guiar o reparo iterativo, melhorando significativamente a correção de raciocínio de múltiplas rodadas.
4. Benchmark Diagnóstico Transversal de Domínios: Constrói um conjunto de dados unificado abrangendo matemática (AIME), raciocínio lógico (AR-LSAT), raciocínio científico (GPQA) e raciocínio geral (MMLU), demonstrando que diversos erros de raciocínio podem ser analisados dentro de uma estrutura simbólica compartilhada.

4. Resultados Experimentais

Os experimentos foram conduzidos em um conjunto de ouro auditado manualmente de 240 instâncias através de quatro domínios.

• Detecção de Fidelidade: O SymDiag alcançou o maior F1 score geral (70.7) na detecção de raciocínio não fiel, superando significativamente o Answer Matching, LLM-as-Judge, Modelos de Recompensa e LogicReward. A lacuna de desempenho foi particularmente pronunciada em benchmarks de raciocínio lógico e geral, onde respostas corretas frequentemente mascaram passos intermediários inválidos.
• Reparo de Raciocínio: Em tarefas de reparo de múltiplas rodadas, o SymDiag demonstrou ganhos de precisão mais rápidos e sustentados em comparação com as linhas de base. Enquanto o Answer Matching proporcionou uma melhoria mínima devido à falta de orientação localizada, e o feedback do LLM-as-Judge saturou rapidamente devido à sua imprecisão, os diagnósticos de nível de passo e baseados em evidências do SymDiag permitiram correções direcionadas.
• Estudos de Ablação: A remoção do Auto-Auditor ou da verificação simbólica de nível de passo causou quedas significativas de desempenho, confirmando que o sucesso do sistema depende da interação entre a robustez da tradução e a verificação lógica explícita.
• Análise de Atribuição de Erro: O SymDiag revelou modos de falha distintos entre escalas de modelos. Modelos menores (ex: 1B parâmetros) cometeram frequentemente erros aritméticos e omitiram premissas, enquanto modelos maiores (ex: 20B) mostraram menos erros de baixo nível, mas maior incidência de regras alucinadas e incompatibilidades de tipo.

5. Significância e Alegações

O artigo posiciona o SymDiag não meramente como um "melhor verificador" ou um "melhor sinal de recompensa", mas como um sistema de diagnóstico neuro-simbólico explicável. Sua principal significância reside em:

• Confiabilidade: Ao fornecer evidências verificáveis (contraexemplos, testemunhas de inconsistência) em vez de pontuações subjetivas, oferece uma base principiológica para diagnosticar o raciocínio de LLMs.
• Escalabilidade: A estrutura é projetada para lidar com diversos domínios de raciocínio (matemática, lógica, ciência, geral) dentro de um framework diagnóstico simbólico unificado.
• Capacidade de Ação: Diferente de métodos anteriores que retornam um escore ou um traço corrigido, o SymDiag localiza falhas e as atribui a causas específicas (tradução vs. raciocínio), permitindo reparos direcionados que são mais eficazes para a melhoria iterativa.

Os autores concluem que, embora modelos base mais fortes melhorem a qualidade da tradução, a estrutura neuro-simbólica estruturada do SymDiag permanece robusta através de diferentes escalas de modelos, oferecendo um caminho escalável para o diagnóstico de raciocínio confiável.