Resumo Técnico: Os LLMs são Tradutores de Lógica Formal Estáveis em Raciocínio Lógico Através de Textos Linguisticamente Diversificados?

1. Definição do Problema

Sistemas de raciocínio lógico que utilizam Grandes Modelos de Linguagem (LLMs) frequentemente empregam um paradigma neuro-simbólico onde o LLM traduz a linguagem natural (NL) para a lógica formal, que é então processada por um resolvedor simbólico. Embora eficaz, essa abordagem depende fortemente de a etapa de tradução ser fiel e consistente. Uma vulnerabilidade crítica, porém subexplorada, é o desvio de símbolo (symbol drift): a falha dos LLMs em mapear expressões semanticamente equivalentes para o mesmo símbolo lógico quando essas expressões aparecem em diferentes formas linguísticas (ex: sinônimos, paráfrases ou variações sintáticas).

Benchmarks existentes para raciocínio lógico costumam utilizar uma linguagem altamente uniforme, repetindo frequentemente as mesmas formas superficiais para os mesmos conceitos. Consequentemente, eles falham em avaliar se os LLMs conseguem manter a consistência de símbolos através de variações linguísticas realistas. Essa lacuna leva a uma superestimação da robustez dos LLMs, visto que textos do mundo real frequentemente expressam o mesmo conceito através de diversas formulações, o que pode quebrar a cadeia de raciocínio e causar erros no resolvedor.

2. Metodologia

2.1 SoLT: Um Benchmark para Diversidade Linguística

Para abordar a falta de avaliação da estabilidade de tradução, os autores introduzem o SoLT (Stability of Logical Translation). O SoLT não é um novo conjunto de dados criado do zero, mas uma transformação sistemática de conjuntos de dados de raciocínio existentes (LogicDeduction, ProntoQA, FOLIO, ProofWriter, ProverQA) utilizando um método de Diversificação Linguística Invariante à Lógica.

O pipeline de diversificação opera em três estágios:

1. Identificação de Conceitos Repetidos: O sistema identifica expressões superficiais que aparecem múltiplamente dentro de um problema ($freq_q(e) \ge 2$).
2. Construção da Estratégia de Diversificação: Para cada conceito repetido, o sistema gera variantes em três níveis:
   • Nível de palavra: Substituição por sinônimos (usando WordNet).
   • Nível de frase: Parafraseamento (usando PPDB).
   • Nível de sentença: Reescritas sintáticas (ex: alternância ativa-passiva, reformulação de terceira pessoa) usando LLMs.
3. Geração de Candidatos sob Filtragem Semântica: Os candidatos gerados são filtrados usando modelos fortes de embedding de sentenças (ex: BGE-large-en-v1.5) para garantir que a similaridade semântica exceda um limiar ($\theta = 0.90$). Um LLM então monta o problema diversificado final, selecionando candidatos que maximizam a diversidade superficial enquanto minimizam formas repetidas para conceitos idênticos.

A validação via escores de similaridade de embedding e pontuação de invariância lógica humana/LLM (escala de 1–5) confirma que o SoLT preserva o significado semântico e a estrutura lógica, enquanto aumenta significativamente a variação linguística.

2.2 MenTaL: Um Framework Guiado pela Representação Mental

Para mitigar o desvio de símbolo, os autores propõem o MenTaL (Mental Representation Table-guided Translation). Inspirado em teorias cognitivas de representação mental, o MenTaL guia explicitamente o LLM para construir e manter uma Tabela de Representação Mental (MRT) durante o processo de tradução.

A MRT mapeia expressões semanticamente equivalentes a um símbolo lógico unificado ($\sigma$). O framework define três operações de atualização para a tabela:

• Extensão (Extending): Atribuição de um novo símbolo a um conceito previamente não visto.
• Reuso (Reusing): Mapeamento de uma nova expressão para um símbolo existente se ela for semanticamente equivalente ($e^{(i)} \equiv e^{(j)}$).
• Verificação e Refinamento (Checking & Refining): Ajuste de mapeamentos para sobreposições parciais ou subsumções (ex: mapear "programa popular" para um símbolo atômico refinado).

O MenTaL pode ser implementado via:

• Aprendizado em Contexto (In-Context Learning): Fornecimento de exemplos de construção de MRT no prompt para modelos de código fechado.
• Ajuste Fino Supervisionado (SFT): Treinamento de modelos menores de código aberto (ex: LLaMA-3-8B) em traços de raciocínio gerados por modelos de alto desempenho utilizando o MenTaL.

3. Principais Contribuições

1. Benchmark SoLT: Um método geral e o benchmark resultante que reescreve conjuntos de dados de raciocínio em formas linguisticamente diversas e logicamente equivalentes para avaliar sistematicamente a estabilidade de tradução sob variação linguística.
2. Framework MenTaL: Uma abordagem leve e generalizável que impõe um mapeamento de símbolos consistente ao organizar explicitamente as relações conceito-símbolo em uma tabela de representação mental.
3. Análise Empírica: Experimentos extensos demonstrando que os LLMs atuais sofrem de um desvio de símbolo generalizado sob diversidade linguística e que o MenTaL mitiga esse problema efetivamente.

4. Resultados Experimentais

4.1 Instabilidade dos LLMs Atuais

Experimentos no SoLT utilizando quatro LLMs (GPT-3.5, GPT-4, DeepSeek-V3, DeepSeek-R1) e três resolvedores simbólicos revelam uma degradação significativa de desempenho:

• Queda de Acurácia: Sob prompting direto, a acurácia cai substancialmente em entradas diversificadas (ex: de 0.51 para 0.24 em média entre as tarefas).
• Escore de Dispersão de Símbolos (SDS): Um novo métrica que quantifica o desvio de símbolo. O SDS aumenta bruscamente nos inputs do SoLT (indicando mapeamento inconsistente), enquanto permanece próximo de zero nos datasets originais.
• Análise de Erro: O principal modo de falha são erros de lógica causados pelo mapeamento inconsistente de símbolos, e não erros de parsing ou execução. Mesmo variações linguísticas leves (ex: substituição de sinônimos) causam uma clara degradação da acurácia.
• Limitações de Ajuste de Prompt: Simples ajustes de prompt ou exemplos de few-shot incentivando a consistência falharam em melhorar significativamente o desempenho ou reduzir o SDS em tarefas diversificadas.

4.2 Eficácia do MenTaL

A aplicação do MenTaL produz ganhos de desempenho consistentes e estáveis:

• Aprendizado em Contexto: Para modelos de alto desempenho, o MenTaL reduziu o SDS para próximo de zero nas tarefas do SoLT e melhorou a acurácia em até 40.74% (ex: no ProntoQA).
• Ajuste Fino Supervisionado (SFT): Para o modelo menor LLaMA-3-8B, o SFT padrão melhorou a acurácia, mas falhou em reduzir o desvio de símbolo em dados diversificados. Em contraste, o SFT baseado em MenTaL alcançou SDS próximo de zero e acurácia significativamente maior tanto nos datasets originais quanto nos diversificados, demonstrando forte generalização entre solvers e tarefas.
• Atribuição de Erro: Análises manuais confirmaram que aproximadamente 50% dos erros corrigidos pelo MenTaL foram especificamente devido à melhoria na consistência de símbolos, validando a eficácia direcionada do mecanismo.

4.3 Intensidade da Diversificação

Experimentos variando a "intensidade da diversificação" (o número de sentenças modificadas por problema) mostraram um declínio suave e contínuo na acurácia dos LLMs conforme a intensidade aumentava. Isso indica um efeito cumulativo onde o processamento de mais variantes semânticas erode progressivamente a capacidade do modelo de manter o alinhamento consistente de símbolos.

5. Significância e Alegações

O artigo alega que negligenciar a diversidade linguística nos benchmarks atuais obscurece uma fraqueza crítica nos tradutores lógicos baseados em LLM: a incapacidade de manter um mapeamento de símbolos consistente através de expressões variadas. Este "desvio de símbolo" quebra a coerência lógica em cenários do mundo real onde sinônimos e paráfrases são comuns.

A significância deste trabalho reside em:

1. Diagnóstico: Fornecer uma ferramenta sistemática (SoLT) para identificar e medir a instabilidade de tradução que os benchmarks padrão não detectam.
2. Solução: Oferecer um método prático e generalizável (MenTaL) para aumentar a robustez de sistemas de raciocínio neuro-simbólicos sem exigir mudanças arquiteturais nos solvers.
3. Confiabilidade: Mover o campo em direção a um raciocínio lógico mais confiável em aplicações do mundo real, garantindo que a estabilidade de tradução seja mantida apesar da variação linguística.

Os autores concluem que, embora o MenTaL melhore significativamente a estabilidade, o desafio do mapeamento consistente de símbolos permanece como uma área chave para pesquisas futuras, particularmente à medida que os LLMs são implantados em ambientes complexos e linguisticamente diversos.