Human Emotion Verification by Action Languages via Answer Set Programming

Resumo Técnico: Verificação de Emoção Humana por Linguagens de Ação via Programação de Conjuntos de Respostas

Definição do Problema
O artigo aborda a necessidade crítica de sistemas interativos e inteligentes para gerenciar estados mentais humanos, particularmente emoções, sem induzir efeitos colares indesejados ou influências inseguras. À medida que os sistemas de IA são cada vez mais implantados em domínios sensíveis, como terapia e mudança de comportamento, há uma carência de métodos formais para verificar se os comportamentos dos agentes aderem aos princípios psicológicos que regem a evolução dos estados mentais. As abordagens existentes frequentemente dependem de modelagem estatística do usuário baseada em instantâneos (snapshots) de comportamento, o que falha em capturar a natureza dinâmica, causal e não determinística dos estados mentais humanos. Além disso, embora as teorias psicológicas (ex: Teoria da Avaliação) descrevam padrões de mudança emocional, modelos computacionais formais raramente integram esses princípios como restrições de transição ou invariantes para verificar rigorosamente o comportamento de longo prazo do sistema.

Metodologia
Os autores introduzem a CMT (Linguagem de Transição de Mente), uma linguagem de ação construída sobre a Programação de Conjuntos de Respostas (ASP) e sistemas de transição. A CMT é projetada para representar como os estados mentais humanos evoluem em resposta a sequências de ações observáveis.

• Formalismo: A CMT estende a linguagem de ação $CTAID$ ao distinguir entre fluentes/ações ambientais observáveis e fluentes/ações mentais não observáveis. Ela introduz construtos especializados como influences (influencia), facilitates (facilita) e contravenes (contravém) para modelar como os estados mentais regulam o comportamento humano.
• Restrição Inovadora: Uma inovação fundamental é a regra forbids to cause (proíbe causar). Esta regra causal especifica que, se certos fluentes mentais ocorrem no tempo $t$, outros fluentes mentais específicos são proibidos de ocorrer no tempo $t+1$. Isso permite a restrição direta de transições de estado independentemente de ações específicas, possibilitando a modelagem de princípios que proíbem certas mudanças mentais.
• Grafo de Crença (BG): O framework utiliza um Grafo de Crença, um grafo direcionado onde os nós representam estados mentais (configurações de fluentes mentais) e as arestas representam transições válidas. O BG é codificado em ASP como um conjunto de restrições de integridade derivadas de teorias psicológicas. Essas restrições filtram trajetórias de ação, garantindo que apenas sequências que aderem a princípios psicológicos específicos sejam consideradas válidas.
• Implementação: O framework traduz as especificações da CMT em programas ASP. A semântica operacional é definida de tal forma que cada conjunto de respostas corresponde a um modelo de trajetória válido do sistema. Isso permite a geração, verificação e comparação de trajetórias de ação.

Estudo de Caso: Raciocínio Emocional
Para demonstrar o framework, os autores aplicam a CMT à Teoria da Avaliação (AE) de Roseman para Emoção, modelando emoções como configurações multidimensionais baseadas em quatro fluentes: Consistência de Necessidade, Consência de Objetivo, Responsabilidade e Potencial de Controle. Isso resulta em um espaço de estados de 108 configurações representando 16 emoções básicas.

Os autores formalizam duas teorias distintas de regulação emocional como conjuntos de restrições de transição dentro do BG:

1. Regulação Emocional Hedônica (HER): Visa aumentar as emoções positivas e diminuir as negativas. As restrições impõem que a consistência de necessidade não deve exceder a consistência de objetivo de uma forma que gere estados negativos.
2. Regulação Emocional Utilitária (UER): Visa alcançar a utilidade a longo prazo, potencialmente aceitando emoções negativas de curto prazo. As restrições priorizam a Consistência de Necessidade e o Potencial de Controle sobre o equilíbrio emocional imediato, permitindo transições que a HER proibiria.

Principais Contribuições

1. Linguagem de Ação CMT: Introdução de uma plataforma fundamental para o raciocínio de estado mental, apresentando a nova regra forbids to cause para restringir transições de estado mental baseadas em princípios psicológicos.
2. Framework Formal: Um conjunto completo de sintaxe e semântica para a CMT, mapeado para ASP, permitindo a verificação formal da dinâmica do estado mental e a detecção de propriedades invariantes.
3. Caracterização Psicológica: A formalização da Teoria da Avaliação, Regulação Emocional Hedônica e Regulação Emocional Utilitária em modelos computacionais, permitindo a representação de estados mentais multidimensionais.
4. Método de Análise Comparativa: Uma metodologia para representar, verificar e comparar diferentes teorias psicológicas através da análise das trajetórias que elas permitem ou proíbem.

Resultados Experimentais
Os autores conduziram uma avaliação experimental usando um conjunto de dados sintéticos de 512 execuções (256 para HER, 256 para UER) com um comprimento de plano de 6.

• Alcançabilidade: Sob restrições HER, estados positivos (ex: Alegria, Esperança) foram alcançáveis a partir de todas as configurações iniciais, enquanto estados negativos (ex: Raiva, Frustração) foram amplamente inalcançáveis. Por outro lado, as restrições UER permitiram a alcançabilidade de estados como Frustração e Culpa (que servem a propósitos utilitários), mas bloquearam muitos estados positivos.
• Análise de Prioridade: O estudo analisou a "Prioridade Emocional" dos fluentes em cada etapa de uma trajetória. As trajetórias HER priorizaram o Potencial de Controle e a Consistência de Objetivo para manter um equilíbrio positivo. As trajetórias UER priorizaram a Responsabilidade (especificamente eu ou o ambiente) e a Consistência de Necessidade, refletindo um foco na responsabilidade e objetivos de longo prazo, em vez do valência emocional imediata.
• Exemplo de Verificação: O framework foi aplicado a um cenário de diálogo envolvendo um chatbot incentivando intenções violentas. A análise mostrou que as ações do chatbot satisfaziam as restrições HER (mantendo uma postura de apoio, hedônica), mas violavam as restrições UER, ilustrando como o sistema pode detectar padrões de influência inseguros.

Significância e Alegações
O artigo afirma que a CMT fornece uma base rigorosa e lógica para o comportamento controlado de agentes. Ao impor princípios psicológicos como restrições de transição, o framework permite que os sistemas antecipem e previnam efeitos colaterais mentais indesejados. Os autores enfatizam que sua abordagem oferece uma maneira estruturada de comparar teorias psicológicas conflitantes computacionalmente, indo além de modelos de usuário estáticos para um raciocínio dinâmico baseado em trajetórias.

O trabalho é modesto em seu escopo, reconhecendo que o modelo atual ainda não lida com a incerteza nas transições de estado mental (embora suporte não determinismo via múltiplos conjuntos de respostas) e depende de interpretações específicas de teorias psicológicas. Os autores posicionam isso como um passo fundamental para unir a teoria psicológica e a implementação computacional, com trabalhos futuros planejados para incorporar incerteza, fluentes ponderados e avaliações do mundo real com humanos no ciclo (human-in-the-loop).