arXiv:2503.18492v1 类型: cross 摘要: 大规模基础模型（LFMs）为人机交互开辟了新的可能性，特别是在移动图形用户界面（GUI）代理崛起之际，这些代理能够解释GUI。这些代理承诺通过简单的自然语言指令自动化复杂的移动任务，从而彻底改变移动计算。然而，LFMs固有的概率性质，加上移动任务的模糊性和上下文依赖性，使得基于LFMs的自动化不可靠且容易出错。为了解决这一关键挑战，我们提出了VeriSafe Agent（VSA）：一种作为移动GUI代理逻辑基础的安全措施的正式验证系统。VSA 是一种设计来确定性地确保代理的动作严格符合用户意图然后再执行动作。其核心是引入了一种新颖的自形式化技术，将自然语言用户指令转化为可以在我们领域特定语言（DSL）中表达的形式可验证规范。这使得可以在运行时，基于规则的验证成为可能，VSA 可以检测并防止执行动作时的错误行为，通过提供纠正反馈或停止不安全行为。据我们所知，VSA 是第一次将形式验证的严谨性引入GUI代理，有效地弥合了由LFM驱动的自动化与形式软件验证之间的差距。我们使用现成的LLM服务（GPT-4o）实现VSA，并在18个广泛使用的移动应用上对300条用户指令进行了评估。结果表明，VSA 在验证代理动作方面的准确率为94.3%-98.33%，比现有的基于LLM的验证方法提高了20.4%-25.6%，从而提高了GUI代理任务完成率90%-130%。