Resumen Técnico: IA Neuro-Simbólica para el Derecho Penal Coreano

1. Planteamiento del Problema

El sistema de justicia penal coreano depende fuertemente de los procedimientos sumarios (guyaksik) para agilizar un alto volumen de infracciones menores, particularmente delitos de tráfico como la conducción bajo la influencia del alcohol (DUI) simple, la conducción sin licencia y accidentes de tráfico menores. Si bien este mecanismo mejora la capacidad de procesamiento judicial, impone una carga administrativa significativa a los fiscales, quienes deben procesar manualmente documentos legales no estructurados (por ejemplo, registros de alcoholimetría, informes policiales, actas de interrogatorio) en resultados estatutarios deterministas.

Los avances recientes en los Modelos de Lenguaje Extensos (LLM) han demostrado capacidades sólicas en la extracción semántica de textos legales densos. Sin embargo, el despliegue de LLM puros para la Predicción de Juicio Legal (LJP) presenta limitaciones fundamentales:

• Naturaleza Probabilística: Los LLM generan texto basado en la probabilidad, lo cual es inadecuado para el razonamiento aritmético estricto y basado en reglas requerido para el cálculo de multas estatutarias.
• Riesgo de Alucinación: En contextos legales, donde la rendición de cuentas exige un determinismo completo, los LLM producen con frecuencia "alucinaciones" cuando se enfrentan a restricciones matemáticas complejas o umbrales estatutarios específicos.
• Falta de Verificación Formal: Las arquitecturas puramente neuronales no pueden probar matemáticamente la validez de un resultado de sentencia, lo que las hace insuficientes para la aplicación judicial directa donde los errores estocásticos son intolerables.

2. Metodología

Los autores proponen un marco neuro-simbólico que tiende un puente entre los hechos legales no estructurados y la verificación formal. La arquitectura particiona estrictamente las tareas entre la comprensión semántica neural y el razonamiento lógico simbólico, organizadas en un flujo de cinco módulos:

Módulo 1: Ingesta de Datos Brutos

El sistema ingiere documentos probatorios heterogéneos y con estructuras de diseño complejas (declaraciones circunstanciales de DUI, resultados de alcoholimetría, actas de interrogatorio e informes de accidentes). Emplea un protocolo de ingesta híbrido sensible al diseño (layout-aware) utilizando un OCR basado en reglas personalizadas y segmentación de texto de codificador bidireccional para aislar las secciones narrativas de los índices tabulares y metadatos, convirtiéndolos en flujos de texto limpios.

Módulo 2: Extracción por LLM

Un LLM actúa como un analizador semántico para extraer elementos centrales del caso (tipos de delitos, variables continuas como la Concentración de Alcohol en Sangre (BAC), y variables categóricas discretas).

• Restricción: El LLM está estructuralmente constreñido para mapear cada factor extraído directamente a su fuente textual exacta ("Texto de Referencia") para imponer el silogismo legal y la fundamentación.
• Salida: Las entidades extraídas se pueblan en un esquema JSON intermedio, que sirve como puente entre la extracción probabilística y la lógica determinista.

Módulo 3: Verificación con Intervención Humana (HITL)

Para garantizar el cumplimiento legal y el debido proceso, se introduce una fase de verificación obligatoria antes de que ocurra cualquier cálculo.

• Interfaz: Una interfaz de pantalla dividida muestra la salida JSON estructurada junto con el documento original con el texto de referencia resaltado.
• Mecanismo: Todas las variables extraídas tienen por defecto el valor is_valid_by_human = false. Un profesional del derecho debe verificar explícitamente cada factor para cambiarlo a true.
• Procedencia de los Datos: Solo los parámetros validados explícitamente por un humano se transfieren al solver, asegurando que el sistema actúe como una herramienta de apoyo a la decisión en lugar de un decisor autónomo.

Módulo 4: Traducción Lógica y Solver SMT Z3

Este es el núcleo del puente neuro-simbólico. Los campos JSON validados se mapean a variables de estado formal (banderas booleanas y restricciones de enteros) dentro del solver de Satisfacibilidad Modulo Teorías (SMT) Z3.

• Modelado de Axiomas: Las Directrices de Sentencia de 2و26 para Delitos de Tráfico se formalizan como axiomas matemáticos. Por ejemplo, los umbrales de BAC se modelan como restricciones condicionales (ej., $0.08 \le BAC < 0.20 \implies Crime\_Category = 3$).
• Derivación de Zonas: El solver evalúa arreglos booleanos de factores atenuantes y agravantes, sumándolos para determinar la zona de sentencia (Básica, Atenuada o Agravada).
• Lógica de Prisión Obligatoria: El solver verifica restricciones lógicas compuestas (ej., si las condenas previas $\ge 3$ o si los factores agravantes son dominantes) para anular los cálculos de multas con recomendaciones de prisión obligatoria.
• Verificación de Satisfacibilidad: Antes de emitir un resultado, Z3 realiza una verificación SAT para asegurar que no existan contradicciones lógicas (ej., un caso no puede ser simultáneamente "Atenuado" y "Agravado"). Si se detecta un estado UNSAT, el flujo regresa a la interfaz HITL para la resolución de conflictos.

Módulo 5: Visualización y Generación de Documentos

Los resultados deterministas del solver Z3 se traducen en artefactos accionables:

• Visualización del Árbol de Sentencia: El sistema renderiza la ruta de decisión lógica (desde la categorización de BAC hasta la multa final) en un árbol visual, proporcionando una pista de auditoría interpretable.
• Redacción de Documentos: Utilizando prompts rígidamente estructurados, un LLM genera documentos legalmente conformes (Informes de Investigación Policial, Opiniones de Remisión y Solicitudes de Acusación Sumaria). Crucialmente, los montos de las multas se inyectan textualmente desde la salida del solver Z3, evitando que el LLM recalcule o alucine números.

3. Contribuciones Clave

El artículo describe tres contribuciones primarias:

1. Diseño de Pipeline Neuro-Simbólico: Un marco que transforma registros policiales y de fiscalía no estructurados en resultados legales deterministas, aislando específicamente al LLM para la extracción semántica con el fin de mitigar los riesgos de alucinación durante el cómputo de multas.
2. Verificación con Intervención Humana (HITL): Un esquema transparente que ancla las variables legales extraídas a los textos de referencia de origen, garantizando la supervisión humana e interpretabilidad mientras mantiene la autoridad legal final en manos del fiscal.
3. Marco de Lógica Legal Formal: La construcción de un marco lógico utilizando el solver SMT Z3 para computar rangos de sentencia precisos alineados con las Directrices de Sentencia de 2026, reemplazando la generación probabilística con prueba matemática.

4. Resultados y Reivindicaciones

El artículo no presenta métricas de rendimiento empíricas (ej., porcentajes de precisión en un conjunto de prueba), ya que el estudio se centra en la formulación teórica y el mapeo lógico de la arquitectura. En su lugar, los autores afirman lo siguiente basándose en el diseño:

• Determinismo: Al delegar los cálculos estatutarios a un demostrador de teoremas, el sistema garantiza que los resultados de las sentencias estén libres de los errores estocásticos inherentes a los LLM.
• Robustez: El mecanismo de verificación SAT asegura que las contradicciones lógicas sean detectadas y resueltas antes de generar un veredicto, evitando resultados legales inválidos.
• Responsabilidad: La integración de HITL asegura que el sistema siga siendo una herramienta de asistencia verificable, abordando las preocupaciones de transparencia inherentes a los modelos de IA de "caja negra".

5. Significado

Los autores posicionan este trabajo como una evolución necesaria en la Predicción de Juicio Legal para entornos de alto riesgo. Al reconocer que los LLM son insuficientes para la aritmética y el cumplimiento estricto de reglas, el artículo propone un enfoque híbrido que aprovecha las fortalezas semánticas de las redes neuronales mientras confía en la lógica simbólica para las restricciones "duras" de la ley.

La importancia radica en su potencial para aliviar el cuello de botella administrativo de las cargas de casos menores de la fiscalía en Corea sin comprometer la integridad judicial. El marco ofrece una vía para automatizar la redacción de acusaciones sumarias (yaksik-gongsojang) asegurando que cada resultado matemático esté fundamentado en hechos formalmente verificados y validados por humanos. Los autores señalan que, aunque el enfoque actual es en delitos de tráfico, la arquitectura está diseñada para ser escalable a otros delitos menores (ej., agresiones simples, difamación, robos menores) que concluyen mediante procedimientos sumarios.