可复用机器人技能正成为具身智能体将开放式指令转化为长时程物理行为的基本单元。尽管基础模型大幅降低了创建这些技能的成本，但信任这些技能的成本并未同步下降。现有技能演化循环通常依赖执行反馈、单元测试、环境奖励或 LLM 自我批评来改进技能，但这些信号只提供轨迹级证据：它们表明技能在采样执行中有效，却不能保证技能诱导的计划在未测试条件下满足时序安全合约。
为此，研究者提出 VASO，一个面向 LLM 生成机器人技能合约的验证引导自演化框架。VASO 的核心思想是将形式化验证与技能演化闭环连接起来：形式化反例不再仅用于验证一次性计划，而是成为优化可复用技能合约的反馈信号。
在 VASO 中，每个技能被表示为一个语义合约，包含两个耦合接口。其一是形式化接口，负责将机器人状态、观测和控制命令与逻辑命题对齐，以便进行模型检查；其二是面向规划器的接口，用于指导可执行行为的生成。这种双接口设计使技能既能被形式化工具分析，又能被规划器实际使用。
VASO 的工作流程分为两步。首先，模型检查器过滤逻辑上不一致的技能合约，避免无效合约进入后续流程。然后，模型检查器针对全局和局部时序规范，验证由技能诱导的计划。当验证失败时，VASO 将反例轨迹翻译成文本梯度，并利用该梯度更新可复用技能合约，同时保持基础模型权重冻结。这意味着技能演化发生在合约层面，而非模型参数层面。
在 Clearpath Jackal 和 PX4 四旋翼任务上的实验表明，VASO 使用少于 100 个优化样本即可达到 97.2% 的形式化规范合规率，优于执行反馈、提示优化和微调基线。据作者所知，VASO 是首个在物理 AI 智能体中闭合形式化验证与 LLM 生成技能自演化循环的框架：形式化反例成为可复用机器人技能合约的优化反馈，而不仅仅是验证一次性计划、调整规划器提示或微调模型权重。
该工作由 Yunhao Yang 等六位作者完成，提交于 2026 年 6 月 3 日，属于机器人学（cs.RO）与人工智能（cs.AI）交叉领域，论文编号 arXiv:2606.05395。项目网页已提供，供进一步了解。