Resumo Técnico: LLMEval-Logic

Declaração do Problema

A avaliação de modelos de linguagem de grande escala (LLMs) em raciocínio lógico em linguagem natural é crítica para aplicações de alto risco, como revisão de contratos, conformidade regulatória e verificação de diretrizes clínicas, onde as conclusões devem seguir estritamente as premissas declaradas. No entanto, os benchmarks existentes de raciocínio lógico sofrem de três deficiências primárias:

1. Falta de Fundamentação Semântica: Muitos benchmarks são gerados via construção reversa (amostragem de fórmulas formais e renderização em texto), resultando em formulações de tipo modelo que permitem aos modelos prever respostas por meio de pistas superficiais em vez de inferência genuína.
2. Auditoria Insuficiente da Formalização: Os benchmarks existentes frequentemente fornecem apenas anotações formais grosseiras ou não auditadas. Eles falham em avaliar se a tradução de um modelo de linguagem natural para lógica formal (NL-para-LF) codifica fielmente unidades semânticas locais, relações lógicas e restrições.
3. Saturação Rápida: Os benchmarks atuais saturam rapidamente sob modelos de raciocínio de ponta, oferecendo pouco espaço para discriminar entre modelos ou localizar modos de falha específicos em tarefas de raciocínio complexo.

Metodologia

Os autores apresentam o LLMEval-Logic, um benchmark de raciocínio lógico chinês construído através de um pipeline auditado de três estágios, projetado para abordar os desafios acima.

1. Construção do Conjunto de Dados (Subconjunto Base)

O subconjunto Base (246 itens) é construído via autoria direta, onde colaboradores com formação em lógica escrevem itens baseados em cenários situacionais realistas (por exemplo, regras de elegibilidade, agendamento) em vez de reengenharia reversa de fórmulas.

• Revisão por Especialistas e Normalização: Os itens passam por revisão especializada para estabilidade conceitual e validade do raciocínio, seguidos por um pipeline de normalização de quatro camadas (alinhamento lexical, sintático, semântico e padronização de tipo/parâmetro) para garantir consistência.
• Verificação Z3: Cada item é verificado usando o solucionador SMT Z3. O solucionador verifica se as premissas formalizadas e as consultas suportam logicamente a resposta anotada sob três tipos de tarefa: possible (satisfatibilidade), necessary (implicação) e enumerate_models (enumeração de modelos).
• Rubricas de Especialistas: Cada item é emparelhado com rubricas desenvolvidas por especialistas que decompõem a fidelidade NL-para-LF em três grupos atômicos: logical_relation (por exemplo, implicação, quantificação), stated_constraint (fatos, limites) e query_alignment. Essas rubricas existem tanto em linguagem natural quanto em formas verificáveis pelo Z3.

2. Endurecimento Adversarial (Subconjunto Hard)

Para prevenir saturação, itens que performam muito bem na sondagem inicial de modelos entram em um fluxo de trabalho de endurecimento adversarial em loop fechado envolvendo cinco papéis de agente: Decisor, Proposta, Revisão, Resposta e Verificação.

• Estratégias de Endurecimento: O fluxo de trabalho reescreve itens usando seis estratégias: ramificação, distratores válidos, incerteza explícita, saídas de valor de conjunto, variantes contrafactuais e variação de alias/coreferência. Essas estratégias alteram o espaço de candidatos fechado ou o caminho de raciocínio em vez de meramente reescrever a superfície.
• Subconjunto Hard: O Hard resultante contém 190 itens compostos por 938 subquestões de múltiplos passos. Um item é considerado correto apenas se todas as subquestões estiverem corretas, forçando os modelos a manter todo o espaço de candidatos através de consultas relacionadas.

3. Protocolo de Avaliação

O benchmark avalia 14 LLMs de ponta em dois eixos:

• Precisão da Resposta: Medida via Precisão do Item (todas as subquestões corretas) e Precisão da Subquestão.
• Precisão da Formalização: Avaliada sob configurações Livre (o modelo escolhe símbolos) e Fixa (símbolos de referência fornecidos). O desempenho é pontuado usando dois sinais complementares:
  • Execução Z3: Verifica se a resposta derivada pelo solucionador corresponde à referência.
  • Correspondência de Rubrica: Verifica se a formalização do modelo passa na lista de verificação atômica desenvolvida por especialistas.
  • Pontuação Conjunta: Requer concordância entre os sinais Z3 e Rubrica.

Resultados Principais

As avaliações de 14 LLMs de ponta (incluindo GPT-5.4 Pro, Claude Opus 4.6, Gemini 3.1 Pro e vários modelos chineses) revelam lacunas significativas nas capacidades atuais:

• Queda de Desempenho: Enquanto o melhor modelo alcança 75,5% de precisão no subconjunto Base, o desempenho cai abruptamente para 37,5% no subconjunto Hard.
• Lacunas de Formalização: Mesmo com símbolos de referência fornecidos, a maior pontuação conjunta de formalização Z3+Rubrica é de apenas 60,16%, indicando que os modelos lutam para codificar premissas com a força semântica necessária, mesmo quando o inventário de símbolos é fixo.
• Divergência de Classificação: Há uma forte correlação negativa ($\rho = -0,61$) entre as classificações Base e Hard. Modelos que se destacam no raciocínio de questão única (por exemplo, Seed 2.0 Pro) frequentemente colapsam em tarefas adversárias de múltiplas questões, enquanto outros (por exemplo, Claude Opus 4.6) mostram estabilidade relativa.
• Modos de Falha: A análise identifica padrões de falha específicos, incluindo:
  • Rastreamento de Quantificador Modal: Confundir consultas existenciais e universais.
  • Enumeração Incompleta: Falhar em percorrer todo o espaço de restrições.
  • Recomputação Contrafactual: Corrigir edições locais sem recomputar globalmente ramificações dependentes.
  • Manutenção do Espaço de Candidatos: Perder o rastreamento do conjunto completo de atribuições viáveis ao lidar com ramificação ou distratores.

Significado e Alegações

O artigo alega que o LLMEval-Logic fornece uma avaliação mais rigorosa e discriminativa do raciocínio lógico ao:

1. Eliminar Artefatos de Modelo: Através da autoria direta a partir de cenários realistas, o benchmark resiste a atalhos de padrões superficiais.
2. Auditar Fidelidade: Ao combinar execução Z3 com rubricas de especialistas, avalia o processo de formalização (fidelidade às semânticas de origem) em vez de apenas a resposta final.
3. Sustentar Dificuldade: O fluxo de trabalho de endurecimento adversarial garante que o benchmark permaneça desafiador para modelos de ponta, expondo limitações específicas na manutenção de espaços de candidatos fechados e na realização de recomputação global.

Os autores concluem que os modelos de ponta atuais, embora capazes de raciocínio de tiro único, ainda carecem da robustez necessária para tarefas lógicas de múltiplos passos e endurecidas adversarialmente, e que a tradução fiel de natural para formal permanece um desafio aberto crítico. O benchmark, o fluxo de trabalho e os rastros de auditoria são lançados publicamente para facilitar pesquisas futuras.