Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers
本文引入了一种机器可检查的“恢复契约”（Resume Contract）来形式化定义并验证工作流持久化语义，揭示了诸如 LangGraph 和 CrewAI 等主流框架违反了诸如效应仅一次（effect exactly-once）和检查点有效性（checkpoint validity）等关键属性，同时提出了一个经过验证的参考实现（REMIT），该实现通过一种新颖的跨进程消费门控（cross-process consumption gate）来保证一致性，并对其进行了验证。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
AI 智能体的数字失忆症
想象一下，你正在制造一个能够完成复杂任务的机器人，比如规划一次旅行或写一个故事。有时，这个机器人需要停下来问你一个问题，比如“我应该预订机票吗？”或者“你喜欢这个剧情转折吗？”这被称为“中断”（interrupt）。如果机器人崩溃了、断电了或者被中断了，它需要一种能够记住自己精确停在何处的方法，以便能从停止的地方继续执行。这被称为“持久化”（persistence）。
在计算机科学领域，特别是在 人工智能（AI）工作流 领域，存在着一个日益严重的问题。我们已经构建了许多不同的“机器人大脑”（框架），它们可以暂停并恢复。然而，这些机器人非常不擅长记住它们已经做了什么。如果一个机器人完成了任务，保存了进度，然后重新启动，一个表现良好的机器人应该说：“我已经做过那个了，让我们继续下一步。”但一个困惑的机器人可能会说：“我不记得做过那个了！”然后又把任务重新做了一遍。如果那个任务是发送电子邮件或扣除信用卡费用，重复执行两次将是一场灾难。本论文研究的是：我们目前的 AI 机器人是真的感到困惑，还是仅仅在假装聪明。
伟大的“恢复”混乱
这篇论文就像是一个侦探故事，但作者 Sajjad Khan 解决的不是谋杀案，而是一个关于数字失忆症的谜团。这个谜团是：当一个 AI 智能体暂停并随后恢复时，它是否记得自己已经做了什么，还是会不小心又做了一遍？
作者发现，目前市面上最流行的五个 AI 框架都在遵循不同且相互冲突的规则手册。这就像你有五种不同的电子游戏，在其中一个游戏中，按下“继续”会跳过你刚刚打过的关卡，而在另一个游戏中，它会强迫你再次挑战 Boss。更糟的是，其中一些游戏甚至不会告诉你它们正在使用哪条规则。
优秀恢复的六大规则
为了弄清楚谁在公平竞争，作者发明了一个“恢复契约”（Resume Contract）。你可以把它想象成一本关于机器人醒来后应该如何表现的规则手册。该契约包含六个主要规则：
- 前缀延续（Prefix Continuation）： 当你醒来时，你应该从中断的地方开始，而不是从电影开头开始。
- 效果仅执行一次（Effect Exactly-Once）： 如果你已经发送了电子邮件或扣除了费用，你绝不能再做第二次。只能做一次。
- 分支确定性（Fork Determinism）： 如果你决定分叉路径（比如选择“向左走”对比“向右走”），机器人必须记住你选择了哪条路径。如果你两次都说“向左”，它不应该在第二次时表现得好像你说了“向右”。
- 检查点有效性（Checkpoint Validity）： 机器人的记忆日志必须是干净的。它不应该保存“垃圾”或损坏的数据，导致稍后发生崩溃。
- 单次消费（Consume-Once）： 如果人类给出了一个答案（比如“是的，预订机票”），机器人应该只使用这个答案一次。它不应该意外地使用同一个“是”来预订两张机票。
- 恢复确定性（Recovery Determinism）： 如果两个机器人拥有完全相同的记忆日志，它们必须做出完全相同的决策。
调查结果：谁失败了？
作者构建了一个超级精确、无需机器人的测试机（harness）来测试五个流行的 AI 框架。测试过程中没有涉及人类大脑或 AI 模型，只有纯代码。结果令人震惊：没有任何两个框架的行为是一致的。
- LangGraph： 这个框架就像一个会忘记自己作业的机器人。当它崩溃并重启时，它会重做已经完成的工作（违反了“效果仅执行一次”）。它还有一个故障：如果你试图改变主意（即“分叉”），它会忽略你的新选择并重复旧的选择。
- CrewAI： 这个框架更加混乱。它声称会跳过已完成的工作，但重启时却会重做一切。这就像一个厨师说：“我已经切好洋葱了，”但接着又切了一遍，浪费了时间和食材。
- LlamaIndex Workflows： 这个框架对自己的困惑很诚实。它承认：“嘿，如果你暂停，我可能会重做暂停前的部分工作。”这不是一个 Bug，而是他们记录在案的一个特性，但对于处理支付等事务来说仍然存在风险。
- pydantic-graph： 这个机器人非常脆弱，如果它在任务中途崩溃，它根本无法醒来。这就像一辆你在行驶档位时关闭引擎，它就无法启动的车。
- AutoGen： 这是唯一一个会大声说“嘿，你尝试加载一个损坏的存档文件！”并拒绝运行的框架。它是那个不让你绕过验证检查的严厉老师。
“双重预订”灾难
最危险的发现之一是关于 单次消费（Consume-Once） 的问题。想象你有一个“停车位”，人类可以在这里给出答案。如果两个人同时尝试给出答案（并发执行），目前的系统会让两人都停进去。机器人随后认为它收到了两个答案，从而执行了两次任务。
作者用 16 个“赛车手”同时尝试回答进行了测试。在 40 次测试中，有 36 次系统完全失败，让所有 16 个赛车手都触发了动作。这就像一个售票亭，16 个人购买了同一张票，而系统竟然让所有人都能进场。
证明与修复
作者并非凭空猜测；他们使用了名为 TLA+ 的数学工具来模拟数百万种场景，以证明这些失败是真实存在的，而非运气不好。他们还使用了形式化验证工具 Verus 来构建一个名为 REMIT 的“完美”机器人引擎。
REMIT 是一个遵循规则的参考引擎。它通过记住你确切选择了哪条路径解决了“分叉”问题，并通过锁定答案确保只有一个人的回答能生效，从而解决了“双重预订”问题。作者展示了当使用 REMIT 时，即使有 64 个不同的线程同时与其通信，机器人也能表现得正确无误。
总结
这里的大教训是：仅仅因为一个 AI 框架宣称它具有“检查点功能”（即保存并恢复的能力），并不意味着它是安全的，不能用于处理金钱或发送消息等重要事务。目前，许多 AI 工具上的“恢复”按钮在某些方面是损坏的，可能会导致重复扣款或数据丢失。
本论文证明了我们需要一个标准化的规则手册（恢复契约），以便开发者明确知道他们的 AI 在醒来时会做什么。在此之前，如果你正在构建一个执行现实世界任务的 AI，你不能仅仅信任框架会记住它所做的事情——你必须建立自己的安全网。作者甚至发布了一个免费工具（REMIT），开发者可以用它来修补自己的系统并使其变得安全，这证明了实现一个完美的、遵守规则的恢复机制是可能的，即便目前的流行工具尚未做到这一点。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。