智能体何时能安全地进行检查点、分叉、恢复与合并？执行编辑的精确检查
When Can Agents Safely Checkpoint, Fork, Restore, and Merge? Exact Checking for Execution Edits
浏览论文内容
中文总结 AI 辅助
该研究针对智能体的检查点、分叉等执行编辑操作，提出一种精确判定编辑安全性的算法，通过形式化方法验证，相关成果已在 Lean 中实现并开源。
中文摘要 AI 辅助
智能体运行时可以对执行过程进行检查点（Checkpoint，记录当前执行状态供后续使用）、分叉（Fork）、恢复（Restore）或合并（Merge）操作，无需重启任务，我们将这些操作称为执行编辑。检查点用于记录当前执行状态，而分叉、恢复与合并操作会改变智能体后续的行为。执行编辑无法撤销先前已授权的操作或已发送的工具请求，因此不安全的编辑可能导致同一工具动作被授权两次、丢弃任务仍需的结果，或与编辑开始前已发起的调用产生冲突。由于智能体是不可信的，运行时需利用其执行记录来确定编辑必须考虑的过去操作，以及必须保留的所需结果，以确保后续执行的安全性。然而，现有的智能体系统在支持此类操作时，并未从运行的执行过程中推导出每个编辑必须保留的内容，而此前计算安全行为的方法将该要求作为输入。我们提出了一种算法，可精确判定某一编辑是否安全，该算法会返回所有安全的后续执行方式，或证明不存在任何安全方式。为做出该判定，算法会列出任务在不违反策略的情况下完成的所有可能方式，剔除任何可能导致后续无法完成仍需结果的方式。若剩余方式为空，则返回可验证的证明，表明不存在安全实现；否则，剩余方式将精确描述运行时可允许的操作。我们的形式化结果涵盖检查点以及分叉、恢复、合并的六种形式，同时包含扩展、原子执行，以及每个精确检查器所需的信息。Lean 工具实现了有限检查器和运行时不变量，测试验证了全部六种编辑形式，源代码、Lean 证明和可执行测试可在该公开 GitHub 仓库获取。
英文摘要
Agent runtimes can Checkpoint an execution, Fork it, Restore a checkpoint, or Merge branches without restarting a task. We call these operations execution edits, with Checkpoint recording the current execution for later use and Fork, Restore, and Merge changing what the Agent will do next. An execution edit cannot undo an earlier authorization or a tool request already sent. An unsafe edit can therefore authorize the same tool action twice, discard a result the task still requires, or conflict with a call that began before the edit. The Agent is untrusted, so the runtime uses its execution record to determine which past actions an edit must account for and which required results it must preserve to keep the subsequent execution safe. Yet existing Agent systems support such operations without deriving what each edit must preserve from the running execution, whereas prior methods for computing safe behavior take that requirement as input. We give an algorithm that decides exactly whether an edit is safe. It returns all safe ways to continue, or proves that none exists. To make this decision, the algorithm lists every way the task can finish without violating policy. It removes any way that could make a still-required result impossible to finish later. If none remain, it returns a checkable proof that no safe implementation exists. Otherwise, the remaining ways describe exactly what the runtime may allow. Our formal results cover Checkpoint and the six forms of Fork, Restore, and Merge, together with extensions, atomic enforcement, and the information every exact checker needs. Lean mechanizes the finite checker and runtime invariant, and tests validate all six edit forms. The source code, Lean proofs, and executable tests are available in the public GitHub repository at https://github.com/eunomia-bpf/agent-check-restore-safety.
