VASO：形式化可验证的物理AI智能体自进化技能
VASO是一个框架，通过形式化验证引导大语言模型生成的机器人技能合约的自我进化。在Clearpath Jackal和PX4四旋翼任务上，VASO在不到100个优化样本下达到了97.2%的规范符合度，优于执行反馈、提示优化和微调基线。这是首个将形式化验证与自进化技能闭环的框架。
随着基础模型（如大语言模型）的快速发展，机器人技能的创建成本大幅降低，但信任成本并未随之下降。传统的技能进化循环依赖执行反馈、单元测试、环境奖励或LLM自我批判，但这些信号仅能提供轨迹级别的证据，证明技能在采样的执行中有效，而无法保证在未测试条件下技能所引发的计划能够满足时序安全合约。为了解决这一问题，来自学界的研究团队提出了VASO（Verifiably Autonomous Self-Operating）框架，旨在通过形式化验证引导LLM生成的机器人技能合约实现自我进化。
VASO的核心思想是将每个可重用的机器人技能表示为一个语义合约，该合约包含两个关键的接口：形式化接口和规划器接口。形式化接口将机器人的状态、观测和控制命令与逻辑命题对齐，以便进行模型检查；规划器接口则指导可执行行为的生成。在运行过程中，模型检查器首先过滤掉逻辑不一致的技能合约，然后验证由该技能引发的计划是否满足全局和局部的时序规范。如果验证失败，VASO将反例轨迹转换为文本梯度，用于更新可重用的技能合约，同时保持基础模型的权重不变。
在实验部分，研究团队在Clearpath Jackal地面机器人和PX4四旋翼无人机上对VASO进行了测试。结果显示，VASO在不到100个优化样本的情况下达到了97.2%的形式规范符合度，显著优于执行反馈、提示优化和微调等基线方法。据我们所知，VASO是首个将形式化验证与LLM生成技能自进化闭环的框架，其中形式反例不仅用于验证一次性计划，还成为可重用技能合约的优化反馈，从而避免了仅调整规划器提示或微调模型权重的局限性。
这项研究为机器人技能的可信进化提供了新的范式，有望在安全关键的物理AI应用中发挥重要作用。通过将形式化验证融入技能进化循环，VASO能够提供更强的安全保障，确保机器人行为在复杂环境中始终符合预期。