Conversational agents are increasingly used as support tools along mental therapeutic pathways with significant societal impacts. In particular, empathy is a key non-functional requirement in therapeutic contexts, yet current chatbot development practices provide no systematic means to specify or verify it. This paper envisions a framework integrating natural language processing and formal verification to deliver empathetic therapy chatbots. A Transformer-based model extracts dialogue features, which are then translated into a Stochastic Hybrid Automaton model of dyadic therapy sessions. Empathy-related properties can then be verified through Statistical Model Checking, while strategy synthesis provides guidance for shaping agent behavior. Preliminary results show that the formal model captures therapy dynamics with good fidelity and that ad-hoc strategies improve the probability of satisfying empathy requirements.

翻译：对话智能体正日益被用作心理健康治疗路径中的辅助工具，并产生显著的社会影响。特别是在治疗情境中，共情是一项关键的非功能性需求，然而当前的聊天机器人开发实践缺乏系统化的方法来规范或验证其共情能力。本文设想了一个整合自然语言处理与形式化验证的框架，以提供具有共情能力的治疗聊天机器人。基于Transformer的模型提取对话特征，这些特征随后被转化为描述二元治疗会话的随机混合自动机模型。通过统计模型检验可验证与共情相关的属性，而策略综合则为塑造智能体行为提供指导。初步结果表明，该形式化模型能以较高保真度捕捉治疗动态，且定制策略能提升满足共情需求的概率。