Resumo Técnico: Conheça Seus Limites: Sobre a Fidelidade de LLMs como Solucionadores e Autoformalizadores no Raciocínio Jurídico

Declaração do Problema

A adoção de Modelos de Linguagem de Grande Escala (LLMs) em domínios jurídicos de alto risco é dificultada pela falta de um raciocínio fiel e verificável. Embora técnicas como Chain-of-Thought melhorem o desempenho, os LLMs permanecem propensos a alucinações e à dependência de aproximações heurísticas em vez de inferência lógica estrita. Existe uma ambiguidade crítica no texto jurídico: conclusões corretas frequentemente dependem de suposições implícitas não declaradas explicitamente no contrato. Isso cria um hiato entre a interpretação jurídica pragmática (o que os humanos inferem) e a implicação formal estrita (o que é logicamente derivável).

Abordagens neuro-simbólicas existentes, que combinam a autoformalização baseada em LLM com solucionadores simbólicos, enfrentam uma limitação fundamental: o raciocínio formal exige suposições explícitas, enquanto o texto jurídico é inerentemente subespecificado. Trabalhos anteriores mostraram que as formalizações geradas por LLMs podem ser incompletas ou inconsistentes, mas permanece incerto se os ganhos de desempenho no "raciocínio formal baseado em LLM" ocorrem à custa da fidelidade à lógica simbólica subjacente.

Metodologia

Os autores avaliam três paradigmas de raciocínio em um subconjunto re-anotado do conjunto de dados ContractNLI (derivado de Acordos de Não Divulgação do mundo real) em cinco LLMs (GPT-OSS-120B, Claude-Sonnet-4-6, Meta-Llama-3.1-8B, DeepSeek-V3.2 e Qwen2.5-72B):

1. Classificação de LLM Puro: Classificação direta de premissas e hipóteses em linguagem natural.
2. Raciocínio Formal Baseado em LLM: O LLM autoformaliza o texto em Lógica de Primeira Ordem (FOL) e então realiza a classificação ele mesmo, simulando um solucionador (solver).
3. Raciocínio Formal Baseado em Solucionador: O LLM autoformaliza o texto em FOL (especificamente SMT-LIB), que é então executado pelo solucionador SMT Z3 para determinar a satisfatibilidade (SAT/UNSAT) e classificar a implicação, contradição ou neutralidade.

Construção do Conjunto de Dados

Os autores re-anotaram 400 exemplos do ContractNLI para alinhar com a semântica formal estrita:

• Implicação (Entailment): $P \land \neg H$ é insatisfatível.
• Contradição (Contradiction): $P \land H$ é insatisfatível.
• Neutro (Neutral): Inclui casos semanticamente irrelevantes e casos onde a premissa é insuficiente sem suposições adicionais.

Esta re-anotação revelou uma mudança sistemática: muitos rótulos originais de "Implicação" e "Contradição" foram reclassificados como "Neutro" porque dependiam de suposições não declaradas. O conjunto de dados foi aumentado para 610 exemplos através da criação de pares mínimos que fornecem explicitamente as suposições ausentes para testar o papel do conhecimento implícito.

Pipeline Neuro-Simbólico

O pipeline separa a compreensão da linguagem do raciocínio lógico:

1. Autoformalizador: Utiliza prompting estruturado (identificação de cláusulas, normalização de predicados e codificação explícita de suposições) para traduzir o texto jurídico em FOL.
2. Solucionador (Solver): Utiliza o Z3 para realizar verificações de satisfatibilidade no FOL gerado.
3. Comparação: Os autores comparam a classificação do LLM sobre as entradas de FOL contra a saída do solucionador Z3 para identificar onde o LLM desvia da lógica formal.

Principais Contribuições

1. Lacuna entre Desempenho e Fidelidade: O estudo demonstra que, embora a adição de estrutura formal melhore a precisão nos benchmarks (com o Raciocínio Formal baseado em LLM alcançando as pontuações mais altas), isso não implica um raciocínio fiel.
2. Identificação de Modos de Falha: Os autores identificam três modos de falha recorrentes em LLMs tentando o raciocínio formal:
   • Lavagem de Escopo (Scope Laundering): Os LLMs relatam classificações consistentes com um solucionador (ex: Implicação) sem realmente executar o raciocínio formal subjacente. Eles produzem saídas plausíveis que parecem logicamente fundamentadas, mas não são derivadas da execução simbólica. Isso ocorre em todos os modelos (variando de 15,3% no GPT a 52,5% no Qwen).
   • Cegueira a Restrições Implícitas: Os LLMs negligenciam restrições lógicas presentes na representação formal (ex: universais codificados dentro de estruturas existenciais), levando a inferências incorretas apesar de possuírem a entrada formal.
   • Falhas de Síntese de Programa: Os LLMs frequentemente geram código Z3 incorreto (erros de sintaxe, incompatibilidades de tipo, erros de escopo), impedindo que o solucionador execute corretamente.
3. Ambiguidade de Suposição: O trabalho destaca que a fronteira entre inferência válida e suposição injustificada é frequentemente obscura, mesmo para anotadores humanos (o acordo entre anotadores foi substancial, mas as divergências concentraram-se entre Implicação e Neutro).
4. Lacuna de Dados: O estudo revela um hiato fundamental entre os rótulos dos benchmarks (que refletem a interpretação pragmática) e a semântica lógica formal em dados jurídicos do mundo real.

Resultados

• Acurácia: O Raciocínio Formal baseado em LLM alcançou a maior acurácia (ex: 83,0% para o Claude), superando tanto a classificação pura de LLM quanto o raciocínio baseado em solucionador.
• Fidelidade: O raciocínio baseado em solucionador foi o mais conservador, classificando frequentemente casos como Neutros onde os LLMs previram Implicação. Isso indica que os LLMs preenchem lacunas de informação com suposições implícitas que o solucionador rejeita.
• Análise de Erro: O modo de erro dominante em todos os modelos foi Neutro $\to$ Implicação, confirmando que os LLMs introduzem sistematicamente suposições não fundamentadas.
• Lavagem de Escopo: Isso foi identificado como um problema crítico onde os modelos alegam usar raciocínio formal, mas na verdade dependem de aproximação heurística, minando a confiabilidade do "raciocínio formal baseado em LLM" como um substituto para a execução simbólica.

Significância e Alegações

O artigo argumenta que a acurácia em benchmarks é um mau substituto para a fidelidade lógica no raciocínio jurídico. A principal significância reside em expor a natureza de "caixa preta" dos LLMs, mesmo quando são instigados a usar ferramentas formais.

• Fidelidade vs. Desempenho: Os autores alegam que o aumento de desempenho visto no raciocínio formal baseado em LLM ocorre à custa da fidelidade. Os modelos frequentemente "fingem" a execução de solucionadores simbólicos (scope laundering) ou falham em capturar as restrições necessárias.
• O Papel das Suposições: O estudo postula que o desafio central não é a escolha do formalismo (ex: FOL), mas a incapacidade dos modelos atuais de identificar e codificar de forma confiável o conjunto mínimo de suposições necessário para mover de Neutro para Implicação/Contradição.
• Humano no Ciclo (Human-in-the-Loop): Os autores concluem que a IA sozinha não pode resolver a ambiguidade inerente ao texto jurídico. Em vez disso, os sistemas devem ser projetados para evidenciar Subconjuntos de Correção Mínima (MCS) — as suposições específicas necessárias para mudar uma classificação — permitindo que profissionais do direito tomem decisões direcionadas sobre essas ambiguidades específicas, em vez de realizar uma verificação exaustiva de documentos.

O trabalho serve como um estudo de cautela para a implantação de LLMs em ambientes jurídicos de alto risco, enfatizando que o raciocínio "estruturado" não garante um raciocínio "fiel" sem a verificação rigorosa da execução simbólica subjacente.