Resumo Técnico: Rumo a uma IA Jurídica Confiável via Avaliação Sensível à Relevância e Raciocínio Fundamentado em Solvers

1. Declaração do Problema

O raciocínio jurídico exige fundamentalmente distinguir entre mudanças que são juridicamente materiais e aquelas que são irrelevantes. Em sistemas baseados no Estado de Direito, os resultados judiciais devem satisfazer a racionalidade formal: conclusões devem ser justificadas por regras explícitas, gerais e logicamente coerentes, rastreáveis até os estatutos governantes. No entanto, os atuais Modelos de Linguagem de Grande Escala (LLMs) aplicados a tarefas jurídicas (por exemplo, resposta a perguntas, sumarização de opiniões, raciocínio em exames da ordem) exibem falhas críticas nessa distinção. Eles frequentemente são:

• Instáveis sob perturbações irrelevantes: Suas decisões mudam com base em atributos juridicamente irrelevantes (por exemplo, dados demográficos, reformulações estilísticas, antecedentes processuais) ou enquadramento adversarial.
• Insensíveis a mudanças materiais: Falham em atualizar previsões quando elementos estatutários, estados mentais ou exceções aplicáveis são alterados.
• Vulneráveis à confusão: Têm dificuldade em distinguir entre estatutos semelhantes com fatos superficiais sobrepostos, mas condições de aplicabilidade diferentes.

Avaliações existentes frequentemente estudam esses fenômenos de forma isolada (por exemplo, equidade ou robustez separadamente). Há uma falta de um quadro unificado que avalie se um modelo permanece invariante sob perturbações "que não deveriam mudar", ao mesmo tempo que atualiza corretamente sob perturbações "que deveriam mudar".

2. Metodologia

O artigo propõe uma abordagem de duas frentes: um novo quadro de avaliação e uma arquitetura de raciocínio inovadora.

2.1 Avaliação Sensível à Relevância Jurídica

Os autores formulam o raciocínio jurídico confiável como um problema de avaliação sensível à relevância jurídica. Este quadro unifica a avaliação de equidade judicial, robustez, enquadramento adversarial e confusão de estatutos em um único conjunto.

• Taxonomia de Perturbações: A avaliação categoriza perturbações em dois tipos:
  1. Preservação de Rótulo (Não Deve Mudar): Perturbações que alteram informações juridicamente irrelevantes (por exemplo, atributos demográficos, paráfrases, opiniões de especialistas irrelevantes, autoridades jurídicas fabricadas) enquanto preservam fatos materiais. Um modelo confiável deve satisfazer $f(x) = f(\tau(x))$.
  2. Mudança de Rótulo (Deve Mudar): Perturbações que modificam condições juridicamente materiais (por exemplo, conduta, estado mental, gravidade do dano, exceções estatutárias). Um modelo confiável deve satisfazer $f(\tau(x)) = y_{\tau}$, onde $y_{\tau}$ é o novo rótulo juridicamente correto.
• Métricas: O quadro mede Invariância (estabilidade sob mudanças irrelevantes), Alinhamento de Mudança (atualizações corretas sob mudanças materiais), Magnitude de Viés e Correção Estatutária.

2.2 LexGuard: Quadro Adversarial Multiagente Fundamentado em Solver

Para abordar as falhas dos LLMs padrão, os autores introduzem o LexGuard, um quadro que separa a proposta jurídica da verificação jurídica usando raciocínio formal.

• Formalização da Lei: Estatutos e interpretações judiciais são auto-formalizados em uma base de conhecimento jurídica formal ($K$) consistindo em restrições executáveis. Cada regra é representada como uma restrição condicional: $ARTICLEGUARD \land CLAUSEGUARD \Rightarrow PENALTY$. Esses guardas verificam sujeito, objeto, conduta, intenção, dano, causalidade e exceções.
• Agentes Adversariais: Dois agentes LLM com papéis diferenciados (Promotor e Defesa) extraem independentemente tuplas estruturadas de fato-estatuto-argumento da mesma narrativa do caso.
  • O Promotor foca em fatos que suportam a responsabilidade.
  • A Defesa foca em elementos ausentes, exceções e interpretações alternativas.
  • Os agentes debatem disposições confusas dentro de clusters de similaridade para refinar estatutos candidatos.
• Adjudicação Centrada no Solver:
  1. O sistema busca em $K$ restrições correspondentes aos estatutos propostos.
  2. Os fatos extraídos são refinados e comparados com os elementos jurídicos necessários.
  3. Os fatos refinados e as restrições são codificados em uma fórmula SMT (Satisfiability Modulo Theories) ($\Phi$).
  4. Um solver SMT (Z3) verifica a satisfiabilidade dos guardas de artigo, guardas de cláusula e guardas de exceção.
  5. Resolução de Conflitos: Se o solver encontrar uma contradição (por exemplo, fatos conflitantes ou guardas incompatíveis), ele retorna um "núcleo insatisfatível" identificando o conflito, desencadeando o re-ancoramento de fatos ou reparo de restrições.
  6. O julgamento final é produzido apenas pela aplicabilidade jurídica verificada pelo solver, filtrando fatos irrelevantes e estatutos alucinados.

3. Contribuições Principais

1. Quadro de Avaliação: A formulação do raciocínio jurídico confiável como um problema sensível à relevância jurídica, instanciado com um conjunto unificado de perturbações "que deveriam mudar" e "que não deveriam mudar", cobrindo equidade, robustez, ataques adversariais e confusão de estatutos.
2. Arquitetura LexGuard: Um quadro adversarial multiagente fundamentado em solver que formaliza estatutos em restrições executáveis, utiliza agentes adversariais para extrair argumentos concorrentes e emprega um solver SMT para verificar consistência lógica e satisfação estatutária.
3. Validação Empírica: Experimentos abrangentes demonstrando que os LLMs jurídicos existentes são sistematicamente sensíveis a variações irrelevantes e falham em distinguir elementos jurídicos relacionados, enquanto o LexGuard melhora significativamente a confiabilidade, equidade e robustez.

4. Resultados Experimentais

Os autores avaliaram o LexGuard em conjuntos de dados jurídicos públicos (LeCaRDv2, LEEC) e em seu conjunto de perturbações personalizado.

• Desempenho de Previsão Padrão: O LexGuard alcançou as melhores pontuações F1 tanto para previsão de disposições gerais quanto específicas no LeCaRDv2 e LEEC. Os ganhos foram impulsionados principalmente por maior precisão, indicando que o solver suprime efetivamente previsões de estatutos irrelevantes.
• Precisão na Sentença: O LexGuard alcançou o menor Erro Quadrático Médio (RMSE) em previsões de sentença, tanto com quanto sem estatutos "dourados" (verdade fundamental), mantendo alta validade jurídica (verificada pelo solver).
• Sensibilidade à Relevância (RQ3 & RQ4):
  • Deve Mudar: O LexGuard mostrou capacidade superior de atualizar previsões quando elementos estatutários foram modificados, superando as linhas de base no "Alinhamento de Mudança".
  • Não Deve Mudar: O LexGuard demonstrou forte robustez contra enquadramento adversarial (por exemplo, autoridades fabricadas, sequestro de papel) e reformulações benignas, mantendo alta invariância e pontuações F1 conscientes de ataques onde as linhas de base falharam.
• Confusão de Estatutos (RQ5): Em tarefas envolvendo clusters de estatutos confusos (por exemplo, roubo vs. fraude), o LexGuard alcançou "Precisão Positiva" significativamente maior (88,71% vs. 58,57% para linhas de base) e taxas menores de omissão e seleção errada de estatutos semelhantes.
• Estudo de Ablação: A remoção do reasoner Z3 causou a maior degradação no desempenho, destacando a necessidade de verificação de consistência simbólica. A remoção do módulo de debate adversarial também reduziu significativamente a precisão, confirmando o valor da competição granular entre disposições confundíveis.

5. Significado e Alegações

O artigo alega que a confiabilidade jurídica requer não apenas precisão, mas também sensibilidade calibrada a mudanças juridicamente materiais.

• Além da Precisão: Alta precisão sozinha é insuficiente para IA jurídica se o modelo for instável sob perturbações irrelevantes ou insensível a mudanças materiais. A confiabilidade é definida pela capacidade de distinguir mudanças relevantes de irrelevantes.
• Raciocínio Auditável: Ao fundamentar decisões em restrições formais e verificação SMT, o LexGuard produz justificações simbólicas que são auditáveis contra regras estatutárias explícitas, abordando a natureza de "caixa preta" dos LLMs padrão.
• Mecanismo de Robustez: Os resultados sugerem que a robustez contra ataques adversariais e perturbações irrelevantes não pode ser alcançada apenas por engenharia de prompt (por exemplo, Cadeia de Pensamento ou few-shot prompting), mas requer uma separação estrutural de proposta e verificação via solvers formais.

Limitações Reconhecidas:
Os autores observam que a qualidade da formalização do quadro depende da precisão dos LLMs usados para gerar fatos e regras iniciais. O sistema atual é limitado a regras estatutárias e ainda não captura plenamente a jurisprudência, normas de textura aberta ou jurisprudência em evolução. Além disso, o processo multiestágio introduz sobrecarga computacional moderada, embora o custo por caso permaneça praticamente acessível.