CEDAR：以自动机作为语言引导具身动作的可验证接口

实体代理的自然语言任务很少只是目标规范：用户还施加了在世界发生变化时必须持续存在的约束。代码生成 LLM 代理可以为此类指令生成看似合理的行为，但它们的自由格式程序不提供稳定的对象来验证、组合新约束或修复失败的跟踪。我们提出了 CEDAR，一个反例引导的框架，它将指令作为环境事件跟踪的常规语言。 CEDAR使用语言模型进行语义判断和执行跟踪进行校正，然后将技能和规范表示为确定性有限自动机。这将约束转化为可执行的有限状态对象：学习的技能可以与学习的夜间睡眠相交或停留在该生物群落规范中，产生一个控制器，该控制器通过构造而不是通过重复提示来强制学习的约束。在 Minecraft 中，通过可用于程序生成基线的相同模拟器/API 观察，CEDAR 维护了基线无法保留的时间和空间约束，并摊销了所学技能的重用，从而减少了累积的 LLM 查询。这些结果表明，常规语言在自然语言指令和具体代理策略之间提供了一个实用的验证层。