Resumo Técnico: Ponte entre Interpretação Jurídica e Lógica Formal

Declaração do Problema: A Divergência da Corretude

O artigo identifica um desalinhamento fundamental entre os objetivos dos profissionais jurídicos e dos pesquisadores de IA no contexto da adoção de Modelos de Linguagem de Grande Escala (LLMs). Enquanto a interpretação jurídica depende de conhecimento de fundo e inferência contextual para derivar conclusões, a lógica formal exige que todas as inferências estejam explicitamente fundamentadas no texto fonte.

O problema central não é meramente que os LLMs alucinem fatos, mas que eles sistematicamente extraem inferências além do que o texto fonte sustenta, apresentando conclusões carregadas de pressupostos como se fossem logicamente fundamentadas. Os sistemas atuais de IA jurídica geralmente ou imitam a interpretação jurídica (via treinamento de modelos de linguagem) ou impõem validade formal (via métodos simbólicos), falhando em reconhecer que esses dois modos de raciocínio divergem regularmente. Essa lacuna torna o raciocínio jurídico assistido por IA não confiável em ambientes de alto risco onde o rigor é primordial.

Metodologia e Desenho Experimental

1. Reanotação do ContractNLI

Os autores investigam essa lacuna utilizando o conjunto de dados ContractNLI, originalmente anotado por especialistas juridicamente treinados. Eles reanotam esses exemplos sob uma definição formal estrita de entailment (implicação):

• Entailment: Uma hipótese $H$ é entailed por uma premissa $P$ se e somente se $P \land \neg H$ for insatisfatível.
• Contradição: $H$ é contradita se $P \land H$ for insatisfatível.
• Neutro: Caso contrário.

Este processo transforma a "lacuna opaca" entre a interpretação pragmática e a lógica estrita em um objeto mensurável. Os autores constroem pares mínimos para casos divergentes — modificando hipóteses minimamente para fornecer explicitamente pressupostos ausentes, tornando-as assim formalmente entailed.

2. Avaliação de Três Paradigmas

O estudo avalia três paradigmas de raciocínio em cinco LLMs (GPT, Claude, LLaMA, DeepSeek, Qwen):

1. Classificação Pura por LLM: Prompting padrão sem restrições formais.
2. Raciocínio por LLM sobre Representações Formais: LLMs gerando estruturas lógicas.
3. Pipeline Neuro-Simbólico: Um sistema combinando formalização por LLM com um solver SMT (Z3) para verificação.

3. Abordagem "Solver-in-the-Loop"

Quando o pipeline SMT encontra uma falta de fundamentação explícita, ele não falha simplesmente; ele calcula o conjunto mínimo de axiomas adicionais necessário para mudar a classificação de Neutro para Entailment ou Contradição. Essas suposições mínimas são apresentadas a um revisor jurídico como perguntas direcionadas (por exemplo, "O direito contratual padrão estabelece implicitamente essa suposição?"), permitindo que a expertise humana valide ou rejeite as normas implícitas.

Principais Descobertas

Mudanças de Rótulo e Lacunas Sistemáticas

A reanotação revelou uma proporção substancial de mudanças de rótulo, principalmente de ENTAILMENT para NEUTRO. Isso indica que muitas conclusões consideradas válidas por especialistas jurídicos dependem de conhecimento de fundo ou pressupostos contextuais ausentes do texto.

Modos de Falha

O estudo identifica três modos de falha recorrentes nos modelos atuais:

1. Injeção de Suposições: Preencher lacunas silenciosamente com inferências não declaradas.
2. Lavagem de Escopo: Apresentar conclusões informais como formalmente fundamentadas.
3. Cegueira para Restrições Implícitas: Ignorar restrições presentes em representações formais.

Análise de Desempenho

• Precisão vs. Fielidade: Modelos de alto desempenho têm sucesso ao imitar a interpretação jurídica (incluindo suposições implícitas) em vez de raciocinar formalmente. Precisão não implica raciocínio fiel.
• A Vantagem do SMT: O pipeline neuro-simbólico é mais conservador, retornando "Neutro" quando a fundamentação explícita falta. Ele traz à tona a lacuna em vez de "tapá-la".
• Erro Dominante: O erro mais comum em todos os modelos é a má classificação NEUTRO $\to$ ENTAILMENT, refletindo injeção sistemática de suposições. Confusões entre Entailment e Contradição são raras, sugerindo que o problema é fundamentação insuficiente, e não inconsistência lógica.

Contribuições Propostas e Agenda de Pesquisa

1. Um Novo Conjunto de Dados de Referência

Os autores propõem um benchmark para má representação de posição em textos jurídicos e acadêmicos. Diferentemente de benchmarks existentes que focam em citações fabricadas, este conjunto de dados visa casos onde as fontes existem e são recuperadas corretamente, mas a alegação do modelo exagera, subestima ou caracteriza erroneamente a fonte. Utiliza o framework de três vias e a metodologia de pares mínimos estabelecidos em sua pesquisa.

2. Treinamento "Solver-in-the-Loop"

Em vez de depender de juízes LLM ou preferências humanas para feedback, os autores propõem usar uma ferramenta de verificação formal como sinal de recompensa.

• O sistema ensina os modelos a distinguir entre inferências formalmente suportáveis e aquelas carregadas de suposições.
• Quando uma alegação é sinalizada como insuficientemente fundamentada, o solver calcula os axiomas mínimos necessários para fundamentá-la.
• Isso alimenta diretamente a revisão humana direcionada nos pontos precisos onde a interpretação jurídica e a fundamentação formal divergem.

Significado e Visão

O artigo argumenta que entender onde e por que os sistemas atuais de IA jurídica falham não é uma limitação, mas a fundação para um futuro confiável. A visão proposta é um sistema de raciocínio jurídico por IA que opera transparentemente em ambos os frameworks:

• Capaz de interpretação jurídica quando apropriado.
• Capaz de fundamentação formal quando necessário.
• Capaz de trazer à tona as suposições mínimas que conectam os dois para revisão jurídica direcionada.

Ao caracterizar honestamente os modos de falha, os autores visam construir sistemas que proativamente exponham a incerteza interpretativa, reduzindo o ônus da verificação manual sem sacrificar a responsabilização exigida pela prática jurídica. Esta abordagem muda o paradigma de pedir aos advogados que verifiquem conclusões após o fato para integrar a expertise humana exatamente onde os métodos formais atingem seus limites.