Human Emotion Verification by Action Languages via Answer Set Programming

Resumen Técnico: Verificación de la Emoción Humana mediante Lenguajes de Acción vía Programación de Conjuntos de Respuestas

Planteamiento del Problema
El artículo aborda la necesidad crítica de sistemas interactivos e inteligentes para gestionar los estados mentales humanos, particularmente las emociones, sin inducir efectos secundarios no deseados o influencias inseguras. A medida que los sistemas de IA se despliegan cada vez más en dominios sensibles como la terapia y el cambio de comportamiento, existe una falta de métodos formales para verificar que los comportamientos de los agentes se adhieran a los principios psicológicos que rigen la evolución de los estados mentales. Los enfoques existentes suelen depender de modelos estadísticos de usuario basados en instantáneas del comportamiento, los cuales no logran capturar la naturaleza dinámica, causal y no determinista de los estados mentales humanos. Además, aunque las teorías psicológicas (por ejemplo, la Teoría de la Evaluación o Appraisal Theory) describen patrones de cambio emocional, los modelos computacionales formales rara vez integran estos principios como restricciones de transición o invariantes para verificar rigurosamente el comportamiento del sistema a largo plazo.

Metodología
Los autores introducen CMT (Lenguaje de Transición Mental), un lenguaje de acción construido sobre la Programación de Conjuntos de Respuestas (ASP) y sistemas de transición. El CMT está diseñado para representar cómo evolucionan los estados mentales humanos en respuesta a secuencias de acciones observables.

• Formalismo: El CMT extiende el lenguaje de acción $CTAID$ distinguiendo entre fluentes/acciones ambientales observables y fluentes/acciones mentales no observables. Introduce constructos especializados como influences (influye), facilitates (facilita) y contravenes (contraviene) para modelar cómo los estados mentales regulan el comportamiento humano.
• Restricción Novedosa: Una innovación clave es la regla forbids to cause (prohibir causar). Esta regla causal especifica que si ciertos fluentes mentales se mantienen en el tiempo $t$, otros fluentes mentales específicos tienen prohibido mantenerse en el tiempo $t+1$. Esto permite la restricción directa de las transiciones de estado independientemente de acciones específicas, permitiendo el modelado de principios que prohíben ciertos cambios mentales.
• Gráfico de Creencia (BG): El marco utiliza un Gráfico de Creencia, un grafo dirigido donde los nodos representan estados mentales (configuraciones de fluentes mentales) y las aristas representan transiciones válidas. El BG se codifica en ASP como un conjunto de restricciones de integridad derivadas de teorías psicológicas. Estas restricciones filtran las trayectorias de acción, asegurando que solo las secuencias que se adhieren a principios psicológicos específicos sean consideradas válidas.
• Implementación: El marco traduce las especificaciones de CMT en programas ASP. La semántica operativa se define de tal manera que cada conjunto de respuestas corresponde a un modelo de trayectoria válido del sistema. Esto permite la generación, verificación y comparación de trayectorias de acción.

Estudio de Caso: Razonamiento Emocional
Para demostrar el marco, los autores aplican CMT a la Teoría de la Evaluación de la Emoción (AE) de Roseman, modelando las emociones como configuraciones multidimensionales basadas en cuatro fluentes: Consistencia de Necesidad, Consistencia de Meta, Responsabilidad y Potencial de Control. Esto produce un espacio de estados de 108 configuraciones que representan 16 emociones básicas.

Los autores formalizan dos teorías distintas de regulación emocional como conjuntos de restricciones de transición dentro del BG:

1. Regulación Emocional Hedónica (HER): Busca aumentar las emociones positivas y disminuir las negativas. Las restricciones imponen que la consistencia de la necesidad no debe exceder la consistencia de la meta de una manera que genere estados negativos.
2. Regulación Emocional Utilitaria (UER): Busca lograr la utilidad a largo plazo, aceptando potencialmente emociones negativas a corto plazo. Las restricciones priorizan la Consistencia de Necesidad y el Potencial de Control sobre el equilibrio emocional inmediato, permitiendo transiciones que la HER prohibiría.

Contribuciones Clave

1. Lenguaje de Acción CMT: Introducción de una plataforma fundacional para el razonamiento del estado mental, que cuenta con la novedosa regla forbids to cause para restringir las transiciones de estado mental basadas en principios psicológicos.
2. Marco Formal: Un sintaxis y semántica completos para CMT, mapeados a ASP, que permiten la verificación formal de la dinámica del estado mental y la detección de propiedades invariantes.
3. Caracterización Psicológica: La formalización de la Teoría de la Evaluación, la Regulación Emocional Hedónica y la Regulación Emocional Utilitaria en modelos computacionales, permitiendo la representación de estados mentales multidimensionales.
4. Método de Análisis Comparativo: Una metodología para representar, verificar y comparar diferentes teorías psicológicas mediante el análisis de las trayectorias que estas permiten o prohíben.

Resultados Experimentales
Los autores realizaron una evaluación experimental utilizando un conjunto de datos sintéticos de 512 ejecuciones (256 para HER, 256 para UER) con una longitud de plan de 6.

• Alcanzabilidad: Bajo las restricciones de HER, los estados positivos (ej. Alegría, Esperanza) eran alcanzables desde todas las configuraciones iniciales, mientras que los estados negativos (ej. Ira, Frustración) eran mayormente inalcanzables. Por el contrario, las restricciones de UER permitieron la alcanzabilidad de estados como Frustración y Culpa (que sirven a propósitos utilitarios), pero bloquearon muchos estados positivos.
• Análisis de Prioridad: El estudio analizó la "Prioridad Emocional" de los fluentes en cada paso de una trayectoria. Las trayectorias de HER priorizaron el Potencial de Control y la Consistencia de Meta para mantener un equilibrio positivo. Las trayectorías de UER priorizaron la Responsabilidad (específicamente propia o del entorno) y la Consistencia de Necesidad, reflejando un enfoque en la responsabilidad y metas a largo plazo en lugar del valencia emocional inmediata.
• Ejemplo de Verificación: El marco se aplicó a un escenario de diálogo con un chatbot que fomentaba intenciones violentas. El análisis mostró que las acciones del chatbot satisfacían las restricciones de HER (manteniendo una postura de apoyo y hedónica) pero violaban las restricciones de UER, ilustrando cómo el sistema puede detectar patrones de influencia inseguros.

Significancia y Reivindicaciones
El artículo afirma que el CMT proporciona una base rigurosa y basada en la lógica para el comportamiento controlado de los agentes. Al imponer principios psicológicos como restricciones de transición, el marco permite a los sistemas anticipar y prevenir efectos secundarios mentales no deseados. Los autores enfatizan que su enfoque ofrece una forma estructurada de comparar teorías psicológicas en conflicto computacionalmente, yendo más allá de los modelos de usuario estáticos hacia un razonamiento dinámico basado en trayectorias.

El trabajo es modesto en su alcance, reconociendo que el modelo actual aún no maneja la incertidumbre en las transiciones de estado mental (aunque soporta el no determinismo mediante múltiples conjuntos de respuestas) y depende de interpretaciones específicas de teorías psicológicas. Los autores posicionan esto como un paso fundacional hacia el puente entre la teoría psicológica y la implementación computacional, con trabajos futuros planeados para incorporar la incertidumbre, fluentes ponderados y evaluaciones del mundo real con humanos en el bucle (human-in-the-loop).