Resumo Técnico: Pelos Seus Frutos os Conhecereis

Declaração do Problema

A formalização de disposições legais em estruturas legíveis por máquina promete raciocínio jurídico automatizado e leis acessíveis por máquinas. Com o advento dos Modelos de Linguagem de Grande Escala (LLMs), tornou-se viável gerar essas formalizações diretamente a partir de textos legais. No entanto, qualquer formalização envolve inerentemente escolhas interpretativas implícitas. Quando um LLM atua como autor, essas escolhas são opacas, e as consequências de interpretações divergentes são difíceis de antecipar. Uma formalização que parece estruturalmente sólida pode produzir vereditos injustos ou incorretos em casos extremos não previstos por seu redator.

O desafio central abordado é como comparar sistematicamente múltiplas formalizações da mesma disposição legal para identificar onde elas divergem em seus resultados lógicos, em vez de meramente comparar sua similaridade estrutural. Métodos existentes frequentemente dependem de correspondência estrutural ou comparação contra um "padrão-ouro", mas os autores argumentam que comparar formalizações entre si sem assumir uma verdade fundamental é necessário para revelar ambiguidades e erros interpretativos genuínos.

Metodologia

Os autores propõem um pipeline de quatro etapas para comparar formalizações de disposições legais geradas por LLMs:

1. Formalização:
   Nove LLMs de ponta recebem instruções para gerar formalizações para dez disposições legais distintas da UE (abrangendo GDPR, Lei de IA, DMA, etc.). Cada formalização é representada como uma árvore rotulada e enraizada, onde os nós folha são variáveis de entrada (fatos) e os nós internos são operadores lógicos (E, OU, NAND, NOR). A raiz representa a consequência legal binária (por exemplo, "proibido" ou "permitido").

2. Correspondência (Construção de Gráfico de Classes de Equivalência):
   Para comparar árvores com estruturas potencialmente diferentes, o método identifica nós em diferentes formalizações que representam o mesmo conceito legal. Um LLM (especificamente o Claude Opus 4.6, selecionado por consistência) agrupa nós de todas as formalizações em Classes de Equivalência (CEs). Isso cria um vocabulário compartilhado (interface) para comparação. O processo de correspondência garante que cada formalização contribua com no máximo um nó para qualquer CEs dada, formando um grafo acíclico direcionado (DAG) de conceitos.

3. Análise de Casos Extremos (Enumeração Baseada em SAT):
   Para cada par de formalizações, o método define uma interface compartilhada com base nas CEs mais profundas comuns a ambas. Ele traduz as sub-árvores acima dessa interface em funções booleanas ($f_A$ e $f_B$).

   • O sistema computa a função de discordância $f_A \oplus f_B$.
   • Usando um solucionador SAT (Z3), ele enumera os implicantes primos dessa função de discordância. Um implicante primo representa um conjunto mínimo de condições de entrada (uma atribuição parcial) que força as duas formalizações a discordarem, independentemente dos valores de outras variáveis não atribuídas.
   • Esses implicantes primos são tratados como "casos extremos".

4. Verbalização:
   Implicantes primos brutos não são interpretáveis por humanos. Os autores aplicam um pipeline de seleção para reduzir o conjunto de casos extremos a um subconjunto representativo (agrupando por "causas raiz" de discordância). Esses casos selecionados são então verbalizados por um LLM em cenários factuais concretos e realistas. A verbalização inclui o cenário, a questão legal específica e uma análise da divergência interpretativa, permitindo que especialistas jurídicos revisem o ponto específico de controvérsia.

Contribuições Principais

O artigo apresenta três contribuições primárias:

1. Uma Estrutura para Formalização Comparativa: Um método para comparar sistematicamente diferentes formalizações da mesma disposição legal enumerando os casos de entrada específicos sobre os quais elas discordam, em vez de depender de similaridade estrutural agregada.
2. Verbalização de Casos Extremos: Uma técnica para transformar casos extremos lógicos derivados de SAT (implicantes primos) em cenários factuais concretos que especialistas jurídicos podem avaliar, fechando a lacuna entre artefatos de verificação formal e raciocínio jurídico humano.
3. Estudo Empírico de Formalizações por LLMs: Uma aplicação deste método a nove LLMs de ponta formalizando dez disposições da UE. O estudo revela que a divergência comportamental é amplamente não correlacionada com o acordo estrutural e que casos verbalizados expõem tipos qualitativamente distintos de discordância, incluindo aqueles que espelham controvérsias genuínas em comentários jurídicos.

Resultados

O estudo gerou 90 formalizações (9 modelos × 10 disposições) e analisou 360 pares.

• Divergência Estrutural vs. Comportamental: Os autores constataram que alto acordo estrutural (medido pela cobertura da interface compartilhada) não garante equivalência lógica. Mesmo quando as formalizações coincidiam bem em conceitos (alta cobertura), elas frequentemente discordavam quanto aos resultados. Por outro lado, pares de baixa cobertura eram frequentemente trivialmente equivalentes simplesmente porque não compartilhavam estrutura sobre a qual discordar.
• Variância entre Modelos: As taxas de discordância variaram significativamente entre os modelos (oscilando de ~32% a ~71% dos pares sendo não equivalentes), mas nenhum modelo único foi uniformemente "extremo". O comportamento foi altamente dependente da disposição, com alguns modelos oscilando de 0% a 100% de discordância entre diferentes disposições.
• Achados Qualitativos:
  • Ambiguidade Interpretativa: No caso do Artigo 5 da Lei de IA (sobre categorização biométrica para aplicação da lei), os modelos dividiram-se igualmente (4 contra 4) sobre se uma exceção específica se aplicava. Essa divergência espelhou uma controvérsia real e em curso em comentários jurídicos sobre o escopo da exceção.
  • Erros de Formalização: No caso do Artigo 3 da Diretiva sobre Cláusulas Abusivas em Contratos (DCAC), um modelo (Kimi K2.5) codificou incorretamente uma regra processual de ônus da prova como um requisito substantivo adicional (conjunção em vez de disjunção), levando a uma definição superconstrita.
  • Limitações: O pipeline apenas revela discordâncias; não consegue detectar erros compartilhados por todos os modelos (por exemplo, se todos os modelos omitirem uma referência cruzada na lei).

Significado e Alegações

O artigo alega que "conhecer a lei é conhecer seus vereditos". Seu significado reside em deslocar a avaliação de formalizações legais de uma análise estrutural estática para uma comparação dinâmica baseada em resultados.

• Auxílio de Auditoria, Não Automação: Os autores afirmam explicitamente que seu pipeline destina-se a ser um "auxílio de auditoria com humano no loop", e não um componente de um sistema automatizado de decisão jurídica. As formalizações não são validadas para uso autônomo.
• Revelação de Divergência Oculta: O método demonstra que a comparação puramente estrutural é insuficiente. Duas formalizações podem parecer semelhantes, mas produzir resultados jurídicos radicalmente diferentes em casos extremos específicos.
• Espelhamento do Discurso Jurídico: Os casos extremos verbalizados revelaram com sucesso discordâncias que correspondem a debates genuínos e não resolvidos na doutrina jurídica, sugerindo que os LLMs não estão apenas alucinando aleatoriamente, mas lidando com as mesmas ambiguidades que os especialistas humanos enfrentam.

Os autores concluem que, embora seu método tenha limitações (dependência de correspondência por LLM, falta de contexto jurídico externo e a incapacidade de verificar a correção sem um padrão-ouro), ele fornece um mecanismo necessário para "conhecer" a lei através das decisões que suas formalizações codificam.