Resumen Técnico: Por Sus Frutos Los Conoceréis

Enunciado del Problema

La formalización de disposiciones legales en estructuras legibles por máquina promete un razonamiento jurídico automatizado y un derecho accesible por máquinas. Con la llegada de los Modelos de Lenguaje Grandes (LLM), se ha hecho factible generar estas formalizaciones directamente a partir del texto normativo. Sin embargo, cualquier formalización implica inherentemente elecciones interpretativas implícitas. Cuando un LLM actúa como autor, estas elecciones son opacas y las consecuencias de interpretaciones divergentes son difíciles de anticipar. Una formalización que parece estructuralmente sólida puede producir veredictos injustos o incorrectos en casos extremos no previstos por su redactor.

El desafío central abordado es cómo comparar sistemáticamente múltiples formalizaciones de una misma disposición legal para identificar dónde divergen en sus resultados lógicos, en lugar de simplemente comparar su similitud estructural. Los métodos existentes suelen basarse en la coincidencia estructural o en la comparación contra un "estándar de oro", pero los autores argumentan que comparar formalizaciones entre sí sin asumir una verdad fundamental es necesario para descubrir ambigüedades e interpretativas genuinas y errores.

Metodología

Los autores proponen un pipeline de cuatro etapas para comparar formalizaciones de disposiciones legales generadas por LLM:

1. Formalización:
   Nueve LLM de vanguardia reciben instrucciones para generar formalizaciones de diez disposiciones legales distintas de la UE (abarcando el RGPD, la Ley de IA, el DMA, etc.). Cada formalización se representa como un árbol etiquetado y enraizado donde los nodos hoja son variables de entrada (hechos) y los nodos internos son operadores lógicos (Y, O, NAND, NOR). La raíz representa la consecuencia legal binaria (por ejemplo, "prohibido" o "permitido").

2. Emparejamiento (Construcción de Gráfico de Clases de Equivalencia):
   Para comparar árboles con estructuras potencialmente diferentes, el método identifica nodos entre distintas formalizaciones que representan el mismo concepto legal. Un LLM (específicamente Claude Opus 4.6, seleccionado por su consistencia) agrupa nodos de todas las formalizaciones en Clases de Equivalencia (CE). Esto crea un vocabulario compartido (interfaz) para la comparación. El proceso de emparejamiento asegura que cada formalización contribuya con como máximo un nodo a cualquier CE dada, formando un grafo acíclico dirigido (DAG) de conceptos.

3. Análisis de Casos Extremos (Enumeración Basada en SAT):
   Para cada par de formalizaciones, el método define una interfaz compartida basada en las CE más profundas comunes a ambas. Traduce los subárboles por encima de esta interfaz en funciones booleanas ($f_A$ y $f_B$).

   • El sistema calcula la función de desacuerdo $f_A \oplus f_B$.
   • Utilizando un solver SAT (Z3), enumera los implicantes primos de esta función de desacuerdo. Un implicante primo representa un conjunto mínimo de condiciones de entrada (una asignación parcial) que fuerza a las dos formalizaciones a discrepar, independientemente de los valores de otras variables no asignadas.
   • Estos implicantes primos se tratan como "casos extremos".

4. Verbalización:
   Los implicantes primos brutos no son interpretables por humanos. Los autores aplican un pipeline de selección para reducir el conjunto de casos extremos a un subconjunto representativo (agrupando por "causas raíz" del desacuerdo). Estos casos seleccionados son luego verbalizados por un LLM en escenarios fácticos concretos y realistas. La verbalización incluye el escenario, la pregunta legal específica y un análisis de la divergencia interpretativa, permitiendo a expertos legales revisar el punto específico de controversia.

Contribuciones Clave

El artículo hace tres contribuciones principales:

1. Un Marco para la Formalización Comparativa: Un método para comparar sistemáticamente diferentes formalizaciones de una misma disposición legal enumerando los casos de entrada específicos en los que discrepan, en lugar de depender de la similitud estructural agregada.
2. Verbalización de Casos Extremos: Una técnica para transformar casos extremos lógicos derivados de SAT (implicantes primos) en escenarios fácticos concretos que los expertos legales pueden evaluar, cerrando la brecha entre los artefactos de verificación formal y el razonamiento jurídico humano.
3. Estudio Empírico de Formalizaciones por LLM: Una aplicación de este método a nueve LLM de vanguardia formalizando diez disposiciones de la UE. El estudio revela que la divergencia de comportamiento está en gran medida descorrelacionada con el acuerdo estructural y que los casos verbalizados exponen tipos cualitativamente distintos de desacuerdo, incluidos aquellos que reflejan controversias genuinas en la doctrina jurídica.

Resultados

El estudio generó 90 formalizaciones (9 modelos $\times$ 10 disposiciones) y analizó 360 pares.

• Divergencia Estructural vs. Conductual: Los autores encontraron que un alto acuerdo estructural (medido por la cobertura de la interfaz compartida) no garantiza la equivalencia lógica. Incluso cuando las formalizaciones coincidían bien en conceptos (alta cobertura), a menudo discrepaban en los resultados. Por el contrario, los pares de baja cobertura a menudo eran trivialmente equivalentes simplemente porque no compartían estructura sobre la cual discrepar.
• Varianza del Modelo: Las tasas de desacuerdo variaron significativamente entre modelos (oscilando entre ~32% y ~71% de los pares no equivalentes), pero ningún modelo fue uniformemente "extremo". El comportamiento dependía en gran medida de la disposición, con algunos modelos oscilando de 0% a 100% de desacuerdo entre diferentes disposiciones.
• Hallazgos Cualitativos:
  • Ambigüedad Interpretativa: En el caso del Artículo 5 de la Ley de IA (sobre la categorización biométrica para aplicación de la ley), los modelos se dividieron equitativamente (4 contra 4) sobre si una excepción específica aplicaba. Esta divergencia reflejó una controversia real y en curso en la doctrina jurídica sobre el alcance de la excepción.
  • Errores de Formalización: En el caso del Artículo 3 de la Directiva sobre Cláusulas Abusivas (DCCA), un modelo (Kimi K2.5) codificó incorrectamente una regla procesal de carga de la prueba como un requisito sustantivo adicional (conjunción en lugar de disyunción), lo que llevó a una definición sobre-restringida.
  • Limitaciones: El pipeline solo pone de manifiesto desacuerdos; no puede detectar errores compartidos por todos los modelos (por ejemplo, si todos los modelos omiten una referencia cruzada en la ley).

Significado y Afirmaciones

El artículo afirma que "conocer la ley es conocer sus veredictos". Su importancia radica en desplazar la evaluación de las formalizaciones legales del análisis estructural estático a la comparación dinámica basada en resultados.

• Ayuda de Auditoría, No Automatización: Los autores declaran explícitamente que su pipeline está destinado a ser una "ayuda de auditoría con intervención humana", no un componente de un sistema automatizado de decisión legal. Las formalizaciones no están validadas para su uso autónomo.
• Descubrimiento de Divergencias Ocultas: El método demuestra que la comparación puramente estructural es insuficiente. Dos formalizaciones pueden parecer similares pero producir resultados legales radicalmente diferentes en casos extremos específicos.
• Reflejo del Discurso Jurídico: Los casos extremos verbalizados pusieron de manifiesto con éxito desacuerdos que corresponden a debates genuinos y sin resolver en la doctrina jurídica, lo que sugiere que los LLM no están alucinando aleatoriamente, sino que están lidiando con las mismas ambigüedades que enfrentan los expertos humanos.

Los autores concluyen que, aunque su método tiene limitaciones (dependencia del emparejamiento por LLM, falta de contexto legal externo e incapacidad para verificar la corrección sin un estándar de oro), proporciona un mecanismo necesario para "conocer" la ley a través de las decisiones que codifican sus formalizaciones.