发表机构
University of Colorado Boulder（科罗拉多大学博尔德分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出 CEDAR 框架，将具身智能体的自然语言指令转化为正则语言并表示为确定有限自动机，在 Minecraft 中可维持基线无法保留的时空约束并减少 LLM 查询，提供了实用的验证层。
AI 中文摘要
自然语言对具身智能体的任务指派很少仅为目标指定：用户还会施加随环境变化必须持续遵守的约束。生成代码的大语言模型（LLM）智能体可为这类指令生成看似合理的行为，但其自由形式的程序无法提供可验证、可与新约束组合或从失败轨迹中修复的稳定对象。我们提出 CEDAR，这是一种反例引导的框架，它将指令基于环境事件轨迹上的正则语言。CEDAR 使用语言模型进行语义判断、执行轨迹进行修正，随后将技能和规范均表示为确定有限自动机。这将约束转化为可执行的有限状态对象：学习到的技能可与学习到的“夜间睡眠”或“待在该生物群系”等规范相交，从而生成控制器，该控制器通过构造而非重复提示来强制执行学习到的约束。在 Minecraft 中，使用与生成代码的基线相同的模拟器/API 观测值，CEDAR 维持了基线未能保留的时间和空间约束，并摊销了学习技能的复用，减少了累积的 LLM 查询。这些结果表明，正则语言在自然语言指令与具身智能体策略之间提供了实用的验证层。
英文摘要
Natural-language tasking of embodied agents is rarely just goal specification: users also impose constraints that must persist while the world changes. Code-generating LLM agents can produce plausible behaviors for such instructions, but their free-form programs provide no stable object to verify, compose with new constraints, or repair from a failing trace. We present CEDAR, a counterexample-guided framework that grounds instructions as regular languages over environment event traces. CEDAR uses a language model for semantic judgments and execution traces for correction, then represents both skills and specifications as deterministic finite automata. This turns constraints into executable finite-state objects: a learned skill can be intersected with a learned sleep at night or stay in this biome specification, yielding a controller that enforces the learned constraint by construction rather than by repeated prompting. In Minecraft, with the same simulator/API observations available to a program-generating baseline, CEDAR maintains temporal and spatial constraints that the baseline fails to preserve and amortizes reuse of learned skills, reducing cumulative LLM queries. These results suggest that regular languages offer a practical verification layer between natural-language instructions and embodied-agent policies.
