Resumen: La racionalidad del derecho se manifiesta en dos formas: la racionalidad sustantiva, que se refiere a la justicia o la deseabilidad moral de los resultados, y la racionalidad formal, que requiere que las decisiones jurídicas sigan reglas explícitamente establecidas, generales y lógicamente coherentes. Los sistemas existentes basados en LLM destacan en el análisis de textos a nivel superficial, pero carecen de las garantías necesarias para una jurisprudencia basada en principios. Presentamos L4M, un marco novedoso que combina agentes LLM adversarios con pruebas respaldadas por solucionador SMT para unir la flexibilidad interpretativa del lenguaje natural con el rigor de la verificación simbólica. El proceso consta de tres fases: (1) Formalización de estatutos, donde las indicaciones específicas del dominio convierten las disposiciones legales en fórmulas lógicas; (2) Extracción dual de hechos y estatutos, en la que los LLM alineados con el fiscal y la defensa asignan de forma independiente narrativas de casos a tuplas de hechos y estatutos, asegurando el aislamiento de funciones; y (3) Adjudicación centrada en Solver, donde un autoformalizador compila los argumentos de ambas partes en restricciones lógicas, y los núcleos no satisfechos desencadenan una autocrítica iterativa hasta que se logra una fórmula satisfactoria, que luego es verbalizada por un juez-LLM en un veredicto transparente y una oración optimizada. Los resultados experimentales en puntos de referencia públicos muestran que nuestro sistema supera los LLM avanzados, incluidos GPT-o4-mini, DeepSeek-V3 y Claude 4, así como las líneas base de IA legal de última generación, al tiempo que proporciona justificaciones simbólicas rigurosas y explicables.
Publicado originalmente en export.arxiv.org el 26 de noviembre de 2025.
Ver fuente original
