VeriSafe Agent：基于逻辑的动作验证以保护移动 GUI 智能体
人机交互
2025-09-12 v2 人工智能
计算与语言
摘要
大型基础模型（LFMs）已为人机交互开辟了新的可能性，尤其是以移动图形用户界面（GUI）智能体的形式出现，这些智能体能够通过简单的自然语言指令与移动 GUI 进行交互。这些智能体允许用户通过自然语言指令自动化复杂的移动任务。然而，LFMs 固有的概率性质，以及移动任务的模糊性和情境依赖性，使得基于LFMs的自动化不可靠且容易出错。为此，我们引入VeriSafe Agent（VSA）：一个作为移动 GUI 智能体的形式化验证系统，作为逻辑上严谨的安全护栏。VSA 在执行动作前确保智能体的动作严格符合用户意图。其核心，VSA 引入一种新型的自动形式化技术，将自然语言用户指令翻译为可形式化验证的规范。这使得对智能体动作的运行时、基于规则的验证成为可能，即在动作发生前即可检测到错误动作。据我们所知，VSA 是首次将形式化验证的严谨性引入 GUI 智能体，弥合了LFM驱动动作与形式化软件验证之间的鸿沟。我们使用现成的LFM服务（GPT-4o）实现了VSA，并在18个广泛使用的移动应用上评估了300条用户指令的性能。结果表明，VSA 在验证智能体动作方面达到了94.33%至98.33%的准确率，优于现有LFM-based验证方法的30.00%至16.33%，并使GUI智能体的任务完成率提高了90%至130%。
关键词
引用
@article{arxiv.2503.18492,
title = {VeriSafe Agent: Safeguarding Mobile GUI Agent via Logic-based Action Verification},
author = {Jungjae Lee and Dongjae Lee and Chihun Choi and Youngmin Im and Jaeyoung Wi and Kihong Heo and Sangeun Oh and Sunjae Lee and Insik Shin},
journal= {arXiv preprint arXiv:2503.18492},
year = {2025}
}