Resumen Técnico: Conoce tus límites: Sobre la fidelidad de los LLM como resolutores y autoformalizadores en el razonamiento jurídico

Planteamiento del problema

La adopción de Modelos de Lenguaje de Gran Escala (LLM) en dominios jurídicos de alto riesgo se ve obstaculizada por la falta de un razonamiento fiel y verificable. Aunque las técnicas de Cadena de Pensamiento (Chain-of-Thought) mejoran el rendimiento, los LLM siguen siendo propensos a las alucinaciones y a la dependencia de aproximaciones heurísticas en lugar de una inferencia lógica estricta. Existe una ambigüedad crítica en el texto legal: las conclusiones correctas suelen depender de supuestos implícitos que no están explícitamente declarados en el contrato. Esto crea una brecha entre la interpretación jurídica pragmática (lo que los humanos infieren) y la implicación formal estricta (lo que es lógicamente derivable).

Los enfoques neuro-simbólicos existentes, que combinan la autoformalización basada en LLM con resolutores simbólicos, enfrentan una limitación fundamental: el razonamiento formal requiere supuestos explícitos, mientras que el texto legal es inherentemente subespecificado. Trabajos previos han demostrado que las formalizaciones generadas por LLM pueden ser incompletas o inconsistentes, pero sigue sin estar claro si las mejoras de rendimiento en el "razonamiento formal basado en LLM" se producen a costa de la fidelidad a la lógica simbólica subyacente.

Metodología

Los autores evalúan tres paradigmas de razonamiento en un subconjunto re-anotado del conjunto de datos ContractNLI (derivado de Acuerdos de No Divulgación del mundo real) a través de cinco LLM (GPT-OSS-120B, Claude-Sonnet-4-6, Meta-Llama-3.1-8B, DeepSeek-V3.2 y Qwen2.5-72B):

1. Clasificación de LLM puro: Clasificación directa de premisas y hipótesis en lenguaje natural.
2. Razonamiento formal basado en LLM: El LLM autoformaliza el texto en Lógica de Primer Orden (FOL) y luego realiza la clasificación por sí mismo, simulando un resolutor.
3. Razonamiento formal basado en resolutor: El LLM autoformaliza el texto en FOL (específicamente SMT-LIB), que luego es ejecutado por el resolutor SMT Z3 para determinar la satisfacción (SAT/UNSAT) y clasificar la implicación, contradicción o neutralidad.

Construcción del conjunto de datos

Los autores re-anotaron 400 ejemplos de ContractNLI para alinearlos con una semántica formal estricta:

• Implicación (Entailment): $P \land \neg H$ es insatisfacible.
• Contradicción: $P \land H$ es insatisfacible.
• Neutral: Incluye casos semánticamente irrelevantes y casos donde la premisa es insuficiente sin supuestos adicionales.

Esta re-anotación reveló un cambio sistemático: muchas etiquetas originales de "Implicación" y "Contradicción" fueron reclasificadas como "Neutral" porque dependían de supuestos no declarados. El conjunto de datos se aumentó a 610 ejemplos mediante la creación de pares mínimos que suministran explícitamente los supuestos faltantes para probar el papel del conocimiento implícito.

Pipeline Neuro-Simbólico

El pipeline separa la comprensión del lenguaje del razonamiento lógico:

1. Autoformalizador: Utiliza un prompting estructurado (identificación de cláusulas, normalización de predicados y codificación explícita de supuestos) para traducir el texto legal a FOL.
2. Resolutor: Utiliza Z3 para realizar comprobaciones de satisfacción en el FOL generado.
3. Comparación: Los autores comparan la clasificación del LLM contra los resultados del resolutor Z3 para identificar dónde el LLM se desvía de la lógica formal.

Contribuciones clave

1. Brecha entre Rendimiento y Fidelidad: El estudio demuestra que, si bien añadir estructura formal mejora la precisión en los benchmarks (con el Razonamiento formal basado en LLM logrando las puntuaciones más altas), esto no implica un razonamiento fiel.
2. Identificación de modos de fallo: Los autores identifican tres modos de fallo recurrentes en los LLM que intentan el razonamiento formal:
   • Lavado de alcance (Scope Laundering): Los LLM reportan clasificaciones consistentes con un resolutor (por ejemplo, Implicación) sin ejecutar realmente el razonamiento formal subyacente. Producen salidas plausibles que parecen lógicamente fundamentadas pero que no son derivadas de la ejecución simbólica. Esto ocurre en todos los modelos (oscilando entre el 15.3% en GPT y el 52.5% en Qwen).
   • Ceguera a restricciones implícitas: Los LLM pasan por alto las restricciones lógicas presentes en la representación formal (por ejemplo, universales codificados dentro de estructuras existenciales), lo que conduce a inferencias incorrectas a pesar de tener la entrada formal.
   • Fallos de síntesis de programas: Los LLM frecuentemente generan código Z3 incorrecto (errores de sintaxis, desajustes de tipos, errores de alcance), lo que impide que el resolutor se ejecute correctamente.
3. Ambigüedad de supuestos: El trabajo destaca que la frontera entre la inferencia válida y el supuesto injustificado es a menudo poco clara, incluso para los anotadores humanos (el acuerdo entre anotadores fue sustancial, pero los desacuerdos se concentraron entre Implicación y Neutral).
4. Brecha de datos: El estudio revela una brecha fundamental entre las etiquetas de los benchmarks (que reflejan la interpretación pragmática) y la semántica lógica formal en los datos legales del mundo real.

Resultados

• Precisión: El Razonamiento formal basado en LLM logró la mayor precisión (por ejemplo, 83.0% para Claude), superando tanto la clasificación pura de LLM como el razonamiento basado en resolutor.
• Fidelidad: El razonamiento basado en resolutor fue el más conservador, clasificando frecuentemente casos como Neutral donde los LLM predijeron Implicación. Esto indica que los LLM cierran las brechas de información con supuestos implícitos que el resolutor rechaza.
• Análisis de errores: El modo de error dominante en todos los modelos fue Neutral $\to$ Implicación, confirmando que los LLM introducen sistemáticamente supuestos no fundamentados.
• Lavado de alcance: Esto se identificó como un problema crítico donde los modelos afirman utilizar el razonamiento formal pero en realidad dependen de una aproximación heurística, socavando la fiabilidad del "razonamiento formal basado en LLM" como un sustituto de la ejecución simbólica.

Significación y Reivindicaciones

El artículo argumenta que la precisión en los benchmarks es un mal indicador de la fidelidad lógica en el razonamiento jurídico. La principal significación reside en exponer la naturaleza de "caja negra" de los LLM incluso cuando se les solicita utilizar herramientas formales.

• Fidelidad vs. Rendimiento: Los autores afirman que la mejora de rendimiento observada en el razonamiento formal basado en LLM se produce a costa de la fidelidad. Los modelos a menudo "fingen" la ejecución de los resolutores simbólicos (lavado de alcance) o no logran capturar las restricciones necesarias.
• El papel de los supuestos: El estudio postula que el desafío central no es la elección del formalismo (por ejemplo, FOL), sino la incapacidad de los modelos actuales para identificar y codificar de manera fiable el conjunto mínimo de supuestos necesarios para pasar de Neutral a Implicación/Contradicción.
• Humano en el bucle (Human-in-the-Loop): Los autores concluyen que la IA por sí sola no puede resolver la ambigüedad inherente del texto legal. En su lugar, los sistemas deben diseñarse para visibilizar Subconjuntos de Corrección Mínima (MCS) —los supuestos específicos requeridos para cambiar una clasificación— permitiendo que los profesionales jurídicos humanos tomen decisiones dirigidas sobre esas ambigüedades específicas en lugar de realizar una verificación exhaustiva de documentos.

El trabajo sirve como un estudio de advertencia para el despliegue de LLM en entornos jurídicos de alto riesgo, enfatizando que el razonamiento "estructurado" no garantiza un razonamiento "fiel" sin una verificación rigurosa de la ejecución simbólica subyacente.