VeriSafe Agent: Safeguarding Mobile GUI Agent via Logic-based Action Verification
作者: Jungjae Lee, Dongjae Lee, Chihun Choi, Youngmin Im, Jaeyoung Wi, Kihong Heo, Sangeun Oh, Sunjae Lee, Insik Shin
分类: cs.HC, cs.AI, cs.CL
发布日期: 2025-03-24 (更新: 2025-09-11)
💡 一句话要点
提出VeriSafe Agent，通过逻辑验证保障移动GUI Agent的可靠性
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 移动GUI Agent 形式验证 自然语言处理 大型语言模型 人机交互
📋 核心要点
- 基于大型语言模型的移动GUI Agent易受错误影响，缺乏可靠性保障。
- VeriSafe Agent (VSA) 提出了一种自动形式化验证方法，将自然语言指令转化为可验证的规范。
- 实验表明，VSA 显著提高了 Agent 动作验证的准确率和任务完成率。
📝 摘要（中文）
大型基础模型（LFMs）开启了人机交互的新可能性，特别是能够与移动图形用户界面（GUI）交互的移动GUI Agent的兴起。这些Agent允许用户通过简单的自然语言指令自动执行复杂的移动任务。然而，LFMs固有的概率性质，加上移动任务的模糊性和上下文依赖性，使得基于LFM的自动化不可靠且容易出错。为了解决这一关键挑战，我们引入了VeriSafe Agent（VSA）：一个形式验证系统，作为移动GUI Agent的逻辑基础保障。VSA确定性地确保Agent的动作在执行前严格符合用户意图。VSA的核心是一种新颖的自动形式化技术，该技术将自然语言用户指令转换为可形式验证的规范。这使得能够在运行时对Agent的动作进行基于规则的验证，甚至在错误动作生效之前检测到它们。据我们所知，VSA是首次尝试将形式验证的严谨性引入GUI Agent，弥合了LFM驱动的动作与形式软件验证之间的差距。我们使用现成的LFM服务（GPT-4o）实现了VSA，并在18个广泛使用的移动应用程序中的300条用户指令上评估了其性能。结果表明，VSA在验证Agent动作方面达到了94.33%-98.33%的准确率，优于现有的基于LFM的验证方法30.00%-16.33%，并将GUI Agent的任务完成率提高了90%-130%。
🔬 方法详解
问题定义：论文旨在解决基于大型语言模型（LLM）的移动GUI Agent在执行任务时容易出错的问题。现有的方法依赖于LLM的概率性输出，缺乏对Agent动作的严格验证，导致任务完成的可靠性较低。移动任务的模糊性和上下文依赖性进一步加剧了这一问题。
核心思路：论文的核心思路是将自然语言的用户指令转化为形式化的规范，然后使用基于规则的验证方法在运行时检查Agent的动作是否符合这些规范。通过形式验证，可以确定性地保证Agent的动作与用户意图一致，从而提高任务完成的可靠性。
技术框架：VSA 的整体框架包括以下几个主要模块：1) 自动形式化模块：将自然语言用户指令转换为形式化的规范。2) Agent动作执行模块：基于LLM生成Agent的动作。3) 运行时验证模块：使用形式化规范验证Agent的动作是否符合用户意图。如果验证失败，则阻止该动作的执行。
关键创新：VSA 最重要的技术创新点在于其自动形式化技术，该技术能够将自然语言指令转化为可形式验证的规范。这是首次尝试将形式验证的严谨性引入GUI Agent，弥合了LFM驱动的动作与形式软件验证之间的差距。
关键设计：自动形式化模块的设计细节未知，但可以推测其依赖于LLM的语义理解能力，并结合预定义的规则和模板，将自然语言指令映射到形式化的逻辑表达式。运行时验证模块则使用这些逻辑表达式作为规则，检查Agent的动作是否满足这些规则。具体的参数设置、损失函数和网络结构等细节未知。
🖼️ 关键图片
📊 实验亮点
实验结果表明，VeriSafe Agent 在验证 Agent 动作方面达到了 94.33%-98.33% 的准确率，显著优于现有的基于 LFM 的验证方法（提升 30.00%-16.33%）。同时，VSA 将 GUI Agent 的任务完成率提高了 90%-130%，表明其在实际应用中具有显著的性能提升。
🎯 应用场景
该研究成果可应用于各种需要高可靠性的移动自动化场景，例如金融交易、医疗健康和智能家居控制。通过确保Agent的动作严格符合用户意图，可以避免因Agent错误操作而造成的损失。未来，该技术还可以扩展到其他类型的Agent和交互界面，提升人机交互的可靠性和安全性。
📄 摘要（原文）
Large Foundation Models (LFMs) have unlocked new possibilities in human-computer interaction, particularly with the rise of mobile Graphical User Interface (GUI) Agents capable of interacting with mobile GUIs. These agents allow users to automate complex mobile tasks through simple natural language instructions. However, the inherent probabilistic nature of LFMs, coupled with the ambiguity and context-dependence of mobile tasks, makes LFM-based automation unreliable and prone to errors. To address this critical challenge, we introduce VeriSafe Agent (VSA): a formal verification system that serves as a logically grounded safeguard for Mobile GUI Agents. VSA deterministically ensures that an agent's actions strictly align with user intent before executing the action. At its core, VSA introduces a novel autoformalization technique that translates natural language user instructions into a formally verifiable specification. This enables runtime, rule-based verification of agent's actions, detecting erroneous actions even before they take effect. To the best of our knowledge, VSA is the first attempt to bring the rigor of formal verification to GUI agents, bridging the gap between LFM-driven actions and formal software verification. We implement VSA using off-the-shelf LFM services (GPT-4o) and evaluate its performance on 300 user instructions across 18 widely used mobile apps. The results demonstrate that VSA achieves 94.33%-98.33% accuracy in verifying agent actions, outperforming existing LFM-based verification methods by 30.00%-16.33%, and increases the GUI agent's task completion rate by 90%-130%.