半夜刷 arXiv，刷到一篇标题里躺着一个老词的论文：automata。这年头敢在具身 agent 论文里拿自动机当主角的，要么是来炒冷饭，要么是真发现了点什么。CEDAR 这篇属于后者——摘要里有一句话把我钉住了：语言模型负责提议，自动机负责把关。
先把判断说满：提示词管住的是词汇，管不住的是约束。这俩根本不是一个物种。
提示词在采样管子线上用力，作用是让某个 token 的概率升一点、降一点。约束不是概率的事。约束是轨迹上的断言，它管的是“这个动作序列在时间上、空间上合不合法”。你让 agent“只能在夜里睡觉”，意思不是让 sleep 这个 token 在合适的时候被采出来；是白天发起的 sleep 动作应该被结构性地拒绝，连试都不该试。凡是能靠一次采样侥幸绕过去的东西，都不配叫约束。
这话听着有点空。老规矩，我们先搓个最简版，让“约束”长出一个看得见的形状。
守一条规则：这个 agent 只能在夜晚睡觉。一个状态机，两个状态，白天和黑夜。事件就三个：入夜、日出、睡觉。入夜把状态拨到 NIGHT，日出拨回 DAY，其余事件不影响状态。唯一要拦的事发生在“状态是 DAY、事件是 sleep”这一格上。
def gate(state, event):
# 返回 (是否放行, 约束状态)
if event == "night":
return True, "NIGHT"
if event == "sunrise":
return True, "DAY"
if event == "sleep":
# 白天睡觉：这条转移在结构上就不存在
if state != "NIGHT":
return False, state
return True, state
# 其他事件：约束状态不动，放行
return True, state
十几行。看着丑，但它把“约束”这个词变成了可以执行的东西。看 sleep 那一支：状态不对，直接返回 False。这一步不跟概率商量，不给模型“这次想起来”的机会。
把它接到一串事件上，跑一下，看看出来啥：
def run_guarded(events):
state = "DAY"
for ev in events:
allowed, state = gate(state, ev)
print(f"{ev:<12} -> {'OK' if allowed else 'REFUSED'} [state: {state}]")
if not allowed:
return False
return True
run_guarded(["explore", "night", "sleep", "explore", "sunrise", "sleep"])
explore -> OK [state: DAY]
night -> OK [state: NIGHT]
sleep -> OK [state: NIGHT]
explore -> OK [state: NIGHT]
sunrise -> OK [state: DAY]
sleep -> REFUSED [state: DAY]
盯最后一行。状态是 DAY，事件是 sleep，结果 REFUSED，而状态机停在 DAY，没有陷入“违规了就破罐破摔”的泥潭。这不是模型这次“记得”白天不该睡，是它的转移表里压根没有这条边。约束的物理形态就是这样：一张表里少了一格。
顺嘴说个插曲。我第一版把事件顺序排错了，sunrise 放在 sleep 前面，等于让一个在白天醒过来的 agent 回笼觉睡了个爽，跑出来前几行全是 OK——我当时还以为 gate 写错了。后来才反应过来，状态机的语义本来就由事件顺序和当前状态共同决定，顺序换了，轨迹就换了一条。这种坑，只会调库的人一辈子碰不到。
现在拿它跟日常做法对照一下。
多数人会给 system prompt 写一句：“你是一个负责任的助手，请在夜晚睡觉，白天保持清醒。”这句话的作用是给概率吹风，把“白天生成 sleep 动作”的概率往下按一点。问题在于，概率被按得再低也不是零。第一轮它记住了，第十二轮它记住了，第五十二轮它照样在烈日下躺平。不是它叛逆，是“提醒”这玩意儿从来不是闸门，而它自己也没有那扇闸门。
你以为你在写约束，其实你只是在写请求。约束和请求的差别，就藏在那十几行的 False 里。
我带着这个糙版本回头重读 CEDAR，很容易就看懂它想干什么了——他们把上面这十几行放大了几百倍，并且放到了骨架的位置。
CEDAR 的做法是三段：把技能本身编码成一个 DFA，从观测事件到动作的转移结构；把用户约束也编码成另一个 DFA，“只在夜晚睡觉”“别离开这个生物群系”，都是轨迹上的状态约束；然后两个自动机取交集。交出来的那个新自动机，天然同时属于技能和约束——也就是说，它跑出来的每一条轨迹都满足约束，不需要谁在旁边监督。
值钱的不是自动机乘积。DFA 求交是几十年前形式语言课上的内容，本科作业水平，不值钱。值钱的是这件事带来的一连串后果：技能一旦被表示成 DFA，就不再是模型权重里一坨说不清道不明的行为倾向。它变成了一张有名字的转移表，可验证、可组合、可复用。过去两年大家说“技能库”，说的其实是“触发这一串词的概率分布”；CEDAR 说的技能库，是命名好的转移结构。新任务来了，把技能状态搬过去，和一条新约束一交，完事。
你也可以想想为什么不能靠堆 if 实现同样的事。给自己的小玩具写一条约束，if 完全够用；写两条，开始皱眉头；第三条加进去，你已经不敢改第一条了。约束之间会互相作用，手工枚举状态组合迟早爆炸。DFA 求交把“两条约束怎么共存”这个问题从手工劳动里拎了出来——这玩意儿天生就是干这个的。
那语言模型在这个框架里干嘛？干的恰恰是它最适合干的边缘活：把原始观测翻译成符号事件——这是语义判断；从成功轨迹里归纳出技能的 DFA 结构——这是模式归纳。归纳出来的结构要拿去模拟器里跑，跑出反例：“这一格不该有转移”“那个动作在某种观测下应该是非法分支”，拿反例回去修结构，修到控制器在验证轨迹上老实为止。
注意这里的角色分配。语言模型不再是那个在每个时刻都得负责“保证约束成立”的实体。约束被编译进控制器了，模型的工作只是沿着合法的转移边走，把原始观测喊成骨架能认的事件。该确定的东西用转移表锁死，该发散的东西让模型去发散——而不是反过来，让一个每次采样都可能飘的模型去守护边界。
他们在 Minecraft 里跑的实验，我读的时候一点不意外：跟一个同样吃模拟器和 API 观测的程序生成基线相比，CEDAR 保住了时间和空间约束，基线的轨迹跑着跑着就放飞了，该守的窗口没守住。
倒是另一个数字更戳我：可复用的已学技能，能把累积的 LLM 查询次数压下去。这个数字我信，而且原因不是“省”，是“分流”。约束一旦编译进 DFA，你就不需要每轮都对着模型重复一遍“记得你只能在夜里睡”。那句叮嘱从 prompt 里挪了出去，变成每个动作都要过一次的物理门禁。查询次数掉下来不是提示词写短了，是本来需要一遍遍重新说的话，被结构一次性承载了。
但糙版本和真实世界之间还有一道坎，得摆出来，不摆不诚实。
刚才那个 gate 能工作，前提是“入夜”“日出”这两个事件已经被正确标注好、喂进来了。真实环境里没这好事。原始观测是像素、传感器读数、连续不断的坐标流，谁告诉你这一刻算“入夜”？谁告诉你当前踩的地形是“草原”？CEDAR 把这步也交给了语言模型，让它从轨迹里翻译出符号事件。这解决了一半问题，剩下那一半它没藏起来：翻译本身依然是概率性的。翻译错了，后面的 DFA 再严格也白搭——自动机保证的是结构合法，不保证符号对齐。模型在原始观测和符号事件之间的那道翻译，是整个链路里最软的一环。
这篇论文没粉饰这个弱点。它只是把这个弱点压到了最小，然后让该硬的地方硬起来。我觉得这是它最值得借鉴的姿势：不去试图把语言模型磨严谨，那是一条注定失败的路；把严谨搬到模型外部，让模型做语义判断和归纳，让自动机做硬性拦截。模型依然可以不完美，但万一哪天它夜里该睡没睡，DFA 会当场大声拒绝——反例有了，修正的抓手也有了。这比在 system prompt 里写一百遍“请遵守约束”诚实得多。至少约束被违反的那一刻，有一个东西会喊出来，而不是让违规悄悄融进下一次采样的概率分布里，像从没发生过。
约束这种事，别放在提示词里求它成立。把它写成状态。一个许诺要想兑现，最后都得从祈使句变成转移表里那个没有合法路径的格子。
多说一句划边界的话：今天这十几行只是用来“懂”的，懂约束和请求的区别，懂为什么 DFA 这种老东西会在 agent 时代回来。真要上生产，请老老实实用现成的验证工具和框架，别拿这版去守真 agent。再往上还有一层没搓：两条 DFA 到底怎么求交、多约束怎么合成，那个留到下次。搓完那个，你手里的约束就能像积木一样拼了。