用逻辑验证确保手机助手按指令正确操作，错误提前发现。
VeriSafe Agent: Safeguarding Mobile GUI Agent via Logic-based Action Verification
- 将自然语言指令转为可验证的逻辑规范，实现动作前校验。
- 在18款应用上验证，动作准确率达94.33%-98.33%，任务完成率提升90%-130%。
- 首个为手机界面智能体提供形式化保障的系统，适合高可靠场景。
大型基础模型（LFMs）为人机交互带来新可能，尤其体现在能够与移动图形用户界面（GUI）交互的手机助手方面。这类助手使用户可通过简单自然语言指令自动化复杂移动任务。然而，LFM固有的概率性以及移动任务的模糊性和上下文依赖性，导致基于LFM的自动化不可靠且易出错。为此，我们提出VeriSafe Agent（VSA）：一种基于形式化验证的手机助手安全防护系统。VSA通过确定性方式确保代理动作严格符合用户意图后再执行。其核心是创新的自动形式化技术，将自然语言用户指令转化为可形式化验证的规范，从而实现运行时规则验证，可在动作生效前检测错误行为。据我们所知，VSA是首次将形式化验证的严谨性引入GUI代理，弥合了基于LFM的动作与形式化软件验证之间的鸿沟。我们使用现成的LFM服务（GPT-4o）实现VSA，并在18个常用移动应用上对300条用户指令进行评估。结果表明，VSA在验证代理动作上达到94.33%-98.33%的准确率，优于现有基于LFM的验证方法30.00%-16.33%，并将代理的任务完成率提高90%-130%。
原文摘要 · Abstract (English)
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%.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。