Resumo Técnico: Mesmas Fórmulas, Semânticas Diferentes

Declaração do Problema

O artigo aborda uma lacuna crítica na avaliação das capacidades de raciocínio de Grandes Modelos de Linguagem (LLMs) em relação à lógica modal. Enquanto os benchmarks existentes (ex: ProofWriter, FOLIO, LogicNLI) avaliam a dedução sob uma lógica de fundo fixa e implícita, eles falham em testar se os modelos podem adaptar seu raciocínio a especificações semânticas explicitamente declaradas. Na lógica modal, a validade de uma inferência frequentemente depende de propriedades específicas de quadros (ex: reflexividade, transitividade, simetria) ou condições de domínio (ex: domínio constante vs. variável). Um modelo pode ter um bom desempenho ao aprender um regime de inferência dominante (uma lógica "familiar" como S5) em vez de aderir às restrições específicas fornecidas no prompt. O problema central é determinar se os LLMs conseguem suprimir suas intuições lógicas padrão para seguir condições semânticas estipuladas, que podem ser não padronizadas.

Metodologia

Os autores constroem um benchmark de diagnóstico projetado para isolar o controle semântico do correspondência de padrões formulaicos.

1. Construção do Benchmark:

• Problemas Pareados: O conjunto de dados central consiste em pares de problemas onde as premissas ($P$) e a conjectura ($C$) são idênticas, mas a especificação semântica ($S$) difere por exatamente uma condição (ex: trocar um quadro reflexivo por um transitivo, ou um domínio cumulativo por um decrescente).
• Verificação por Oráculo: Um oráculo de raciocínio automatizado (usando Vampire e Leo-III via ferramenta de incorporação LET) verifica que as duas especificações geram valores de verdade opostos ($y_a \neq y_b$) para a mesma fórmula.
• Núcleo Balanceado: Para evitar que os modelos explorem um atalho de "apenas condição" (onde a resposta é determinada apenas pelo rótulo semântico sem ler a fórmula), os autores criaram um "núcleo não aninhado balanceado" de 160 pares. Neste subconjunto, cada condição semântica aparece com igual frequência com ambos os rótulos Verdadeiro e Falso. O sucesso aqui exige estritamente a leitura da fórmula para determinar qual condição a valida.
• Escopo: O conjunto de dados cobre cinco contrastes de propriedades de quadros (K–D, K–T, T–B, T–S4, B–S5) e três contrastes de domínio (variável–cumulativo, variável–decrescente, cumulativo–constante), totalizando 800 pares de sistemas aninhados e 160 pares de núcleo balanceado.
• Prompting: Os prompts utilizam inglês controlado para declarar regras explicitamente (ex: "A relação de acessibilidade é reflexiva e simétrica") sem usar nomes de sistemas convencionais (como "S4"), forçando o modelo a depender das regras fornecidas.

2. Protocolo Experimental:

• Modelos: O estudo avalia cinco modelos recentes: DeepSeek V4 (Flash e Pro), GPT-5.6 (Luna e Terra) e Claude Sonnet 5.
• Condições:
  • Prompt Direto: Inferência padrão sem modo de raciocínio.
  • Modo de Raciocínio: Ativado para modelos específicos (ex: DeepSeek Flash "alto esforço") para testar se o aumento da computação em tempo de inferência auxilia a adesão semântica.
  • Sensibilidade de Representação: Um subconjunto testa o desempenho através de condições em inglês nomeadas, definições relacionais e sintaxe TPTP formal.
  • Afinidade Semântica: Experimentos omitem as especificações de quadro para identificar qual lógica "padrão" os modelos favorecem quando não restringidos.

Principais Resultados

1. Falha de Controle Semântico sob Prompt Direto:
No núcleo balanceado, quatro dos cinco modelos apresentaram desempenho significamente abaixo da linha de base de 50% de "apenas condição" (que assume que o modelo ignora a fórmula e adivinha com base no rótulo da condição).

• DeepSeek V4 Flash: 4,4% de precisão de par estrito.
• DeepSeek V4 Pro: 2,5%.
• GPT-5.6 Luna: 21,2%.
• GPT-5.6 Terra: 25,0%.
• Claude Sonnet 5: 65,0% (o único modelo que excedeu a linha de base).
  Isso indica que a maioria dos modelos falha em rastrear a semântica declarada, aplicando, em vez disso, uma lógica fixa e familiar, independentemente das restrições do prompt.

2. Modo de Raciocínio como Mecanismo Restaurador:
Habilitar o modo de raciocínio melhorou dramaticamente o desempenho do DeepSeek V4 Flash, elevando sua precisão no núcleo balanceado de 4,4% para 88,1%. Ganhos semelhantes foram observados para o GPT-5.6 Luna em problemas de quadro. Isso sugere que a falha não é necessariamente uma falta de conhecimento lógico, mas uma falha em ativar o modo de inferência correto para processar as restrições específicas.

3. Afinidade Semântica e Padrões:
Quando as especificações foram omitidas, os modelos exibiram afinidades coerentes com lógicas familiares (ex: DeepSeek Flash favoreceu K, enquanto Sonnet favoreceu K, e outros favoreceram T). No entanto, esses padrões não predisseram de forma confiável os erros quando as restrições eram explícitas; os modelos frequentemente concordavam em problemas subespecificados, mas falhavam ao ajustar quando as restrições eram adicionadas.

4. Sensibilidade de Representação:
Alterar o formato de entrada (de condições nomeadas para definições relacionais ou TPTP) alterou o ranking de desempenho, mas não restaurou consistentemente o controle semântico. Por exemplo, a precisão do GPT-5.6 Terra caiu de 38% (nomeado) para 6% (definições relacionais), indicando que a formatação de superfície não é uma correção simples para o problema subjacente de adesão semântica.

Principais Contribuições

• Benchmark de Diagnóstico: Introdução de um framework de avaliação controlado que mantém o problema de nível de objeto fixo enquanto varia a especificação semântica, projetado especificamente para testar a "sensibilidade de especificação".
• Núcleo Balanceado: Um design de conjunto de dados inovador que elimina a possibilidade de resolver problemas mapeando condições semânticas para respostas sem ler a fórmula lógica.
• Evidência Empírica de Dependência de Modo: Demonstração de que a capacidade de seguir a semântica modal é altamente dependente do modo de inferência (direto vs. raciocínio), desafiando a noção de capacidades de raciocínio lógico estáticas em LLMs.
• Liberação de Recursos: Liberação pública das fórmulas, artefatos do oráculo, contraexemplos e respostas dos modelos.

Significância e Alegações

O artigo argumenta que benchmarks de semântica fixa podem superestimar a robustez do raciocínio de LLMs. O principal achado é que o conhecimento modal (conhecer a lógica) é distinto do controle semântico (aplicar a lógica específica fornecida). Um modelo pode possuir as regras lógicas necessárias, mas falhar em deixar uma especificação local governar sua resposta, recorrendo, em vez disso, a um regime de inferência familiar.

Os autores alegam modestamente que seu trabalho separa essas duas capacidades. Eles observam que, embora o modo de raciocínio possa restaurar a sensibilidade às intervenções semânticas, ele não garante a correção das etapas de derivação intermediárias (ex: um modelo pode alternar corretamente a lógica, mas ainda derivar uma conclusão falsa devido a um erro de raciocínio). O estudo conclui que avaliações futuras devem testar explicitamente se os modelos podem se adaptar às restrições declaradas em vez de depender de pressupostos de fundo fixos. O artigo não propõe novas aplicações ou mudanças arquiteturais futuras, focando estritamente na avaliação diagnóstica dos modelos atuais.