Resumen Técnico: U-Define: Diseño de Flujos de Trabajo de Usuario para Restricciones Duras y Blandas en la Planificación Basada en LLM

1. Declaración del Problema

Aunque los Modelos de Lenguaje Grande (LLM) han reducido la barrera para la planificación de tareas por parte de usuarios finales, su naturaleza de "caja negra" introduce problemas significativos de fiabilidad. Los LLM a menudo producen planes inconsistentes, fallan al imponer requisitos estrictos y generan salidas con razonamientos confiables pero erróneos. Los enfoques de verificación existentes, como críticos externos o verificación formal, suelen depender de plantillas pre-diseñadas rígidas o especificaciones específicas del dominio que limitan la flexibilidad. Por el contrario, los enfoques puramente de restricciones blandas (por ejemplo, pesos numéricos o preferencias flexibles) suelen ser difíciles de interpretar para los usuarios y no garantizan reglas críticas de seguridad o lógica.

El desafío central abordado por este trabajo es diseñar un flujo de trabajo de interacción que permita a los usuarios expresar y equilibrar de manera fiable las restricciones duras (reglas que nunca deben violarse) y las restricciones blandas (preferencias que reflejan flexibilidad) dentro de la planificación basada en LLM, sin requerir que los usuarios aprendan lenguajes de especificación formal ni dependan de plantillas rígidas.

2. Metodología y Diseño del Sistema

Los autores proponen U-Define, un sistema que operacionaliza un flujo de trabajo donde los usuarios definen restricciones en lenguaje natural, las categorizan por estrictitud y reciben resultados de verificación adaptados a cada tipo de restricción. El sistema extiende trabajos anteriores (VeriPlan) al eliminar las dependencias de plantillas e introducir una arquitectura de verificación híbrida.

Arquitectura del Sistema

U-Define estructura el proceso de planificación en tres etapas:

1. Etapa de Definición:

   • Entrada: Los usuarios introducen restricciones en lenguaje natural y las categorizan como Duras o Blandas.
   • Traductor de Reglas: Un agente LLM especializado (ajustado finamente en LLaMA 7B utilizando el conjunto de datos NL2LTL) traduce las restricciones duras definidas por el usuario a propiedades de Lógica Temporal Lineal (LTL).
   • Conversión a PRISM: Las propiedades LTL se traducen posteriormente al lenguaje de modelado PRISM, un formato requerido para la verificación de modelos probabilísticos.
   • Validación: El sistema convierte las reglas formales de nuevo a lenguaje natural para la verificación del usuario antes de proceder.

2. Etapa de Verificación:

   • Generación de Planes: Un Planificador LLM genera planes candidatos basados en el prompt de tarea del usuario y las restricciones.
   • Verificación de Restricciones Duras: El plan generado se convierte al formato PRISM. Un Verificador de Modelos formal (utilizando PRISM y Stormpy) explora exhaustivamente el espacio de estados del plan para verificar el cumplimiento de las reglas LTL. Devuelve un resultado binario de validez y una lista de reglas específicas violadas.
   • Verificación de Restricciones Blandas: Un agente LLM-como-Juez evalúa el plan frente a las restricciones blandas. Proporciona una calificación de 1 a 5 estrellas y una explicación en lenguaje natural sobre el grado de alineación con las preferencias del usuario.

3. Etapa de Retroalimentación:

   • Los usuarios revisan los planes clasificados (priorizados por violaciones de restricciones duras) y los resultados de verificación.
   • Los usuarios pueden refinar iterativamente las restricciones, ajustar la estrictitud de las reglas o modificar el prompt. El sistema regenera el plan y lo re-verifica, creando un bucle de retroalimentación cerrado.

Implementación Técnica

• Agentes LLM: La mayoría de los agentes utilizan GPT-4. El Traductor de Reglas utiliza un modelo LLaMA 7B ajustado finamente.
• Verificación Formal: Utiliza PRISM y Stormpy para la verificación de modelos.
• Evaluación: El sistema fue evaluado mediante una evaluación técnica a nivel de componente (midiendo la precisión de la traducción) y dos estudios con usuarios.

3. Contribuciones Clave

Contribuciones Técnicas

• Pipeline de Traducción Automatizada: Un pipeline automatizado que traduce restricciones duras en lenguaje natural a artefactos de verificación formal (LTL y PRISM) utilizando LLM, eliminando la necesidad de plantillas de dominio pre-diseñadas.
• Mecanismo de Verificación Híbrido: Un sistema que aplica métodos de verificación distintos según el tipo de restricción: verificación de modelos formal para restricciones duras (garantizando corrección) y evaluación LLM-como-juez para restricciones blandas (evaluando la alineación de preferencias).

Contribuciones del Sistema

• Interfaz U-Define: Una interfaz de usuario que permite la definición simultánea de restricciones duras y blandas, visualizándolas mediante un diseño de mapa mental, y presentando retroalimentación de verificación diferenciada (listas de violaciones frente a calificaciones por estrellas).

Contribuciones Empíricas

• Estudios con Usuarios: Se realizaron dos estudios:
  1. Estudio 1 (Usuarios Generales): Un estudio de ablación intra-sujeto con 12 participantes en tres escenarios (vacaciones, boda, planificación de recetas).
  2. Estudio 2 (Expertos de Dominio): Un estudio con 6 expertos de diversos campos (educación, construcción, finanzas) realizando tareas de planificación profesional.
• Hallazgos:
  • Valor Percibido: El sistema completo (C1) superó significativamente a las condiciones de ablación (Solo Blandas, Solo Duras, Ninguna) en utilidad percibida, satisfacción y rendimiento.
  • Roles Distintos: Los usuarios percibieron las restricciones duras y blandas como cumpliendo roles complementarios: las restricciones duras proporcionaron una base no negociable, mientras que las restricciones blandas permitieron la personalización.
  • Rigidez vs. Flexibilidad: Las condiciones de Solo Duras condujeron a menos iteraciones pero menor satisfacción debido a la rigidez y la latencia. Las condiciones de Solo Blandas fomentaron la exploración pero sufrieron de explicaciones poco fiables y brechas de verificación.
  • Desafíos de Expertos: Los expertos valoraron el sistema para gestionar reglas estrictas, pero enfrentaron una "sobrecarga de contexto" al recordar e introducir numerosas restricciones. También notaron que algunas restricciones profesionales (límites numéricos, lógica de calendario) excedían la expresividad del LTL.

4. Resultados y Significado

Rendimiento Técnico

• Traducción a LTL: El LLM ajustado finamente logró una similitud Levenshtein promedio del 83.12% frente a la verdad fundamental generada por humanos. Los errores fueron principalmente a nivel de predicado (por ejemplo, desajustes de tokens) en lugar de errores en operadores lógicos.
• Conversión a PRISM: La conversión de planes a PRISM logró una similitud del 97.4%, con errores que también ocurrieron a nivel de predicado.

Experiencia de Usuario e Implicaciones de Diseño

El artículo afirma que U-Define cierra con éxito la brecha entre la fiabilidad de la verificación determinista y la flexibilidad de la IA generativa. Las principales implicaciones de diseño derivadas de los resultados incluyen:

1. Soporte para Restricciones Mixtas: Los sistemas deben permitir a los usuarios distinguir explícitamente entre restricciones duras y blandas para equilibrar la fiabilidad y la personalización.
2. Explicaciones Accionables: Las explicaciones para restricciones duras deben listar explícitamente las reglas violadas en lugar de proporcionar calificaciones escalares genéricas, las cuales los usuarios encontraron confusas para las restricciones blandas.
3. Gestión del Contexto: Los sistemas futuros deben ayudar a los usuarios a reducir la carga cognitiva de la entrada de restricciones (por ejemplo, mediante plantillas, perfiles reutilizables o integración de herramientas externas), una necesidad crítica identificada por expertos de dominio.
4. Cobertura de Verificación: Los sistemas deben indicar transparentemente cuándo una restricción del usuario no puede ser verificada completamente por el motor formal (por ejemplo, restricciones numéricas) y tratar esas partes como comprobaciones heurísticas.

Significado

El artículo argumenta que el soporte efectivo para la planificación requiere dar a los usuarios control sobre cómo se expresan y aplican las restricciones. Al colocar la autoridad para definir la estrictitud de las restricciones en manos del usuario y combinarla con mecanismos de verificación apropiados, U-Define demuestra que es posible crear sistemas de planificación que sean tanto confiables (mediante verificación formal de reglas críticas) como adaptables (mediante el manejo flexible de preferencias). Este enfoque aborda las limitaciones de la verificación puramente basada en plantillas y la planificación puramente generativa, ofreciendo una vía para una colaboración humano-IA más fiable en escenarios complejos del mundo real.