When Can Agents Safely Checkpoint, Fork, Restore, and Merge? Exact Checking for Execution Edits
本文提出了一种精确算法，通过计算所有既能保留必要结果又能避免策略违规的有效延续，来确定智能体执行编辑（如检查点、分叉、恢复和合并）的安全性，并通过 Lean 形式化验证提供形式化证明，并进行经验验证。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
在现代数字景观中，软件智能体作为自主助手，能够通过调用外部工具来执行复杂的任务。它们可以检查航班时刻表、处理付款或批准购买，逐步推进工作流。然而，这些智能体并非无懈可击；它们可能会犯错、遇到意外的障碍，或者仅仅是需要在任务执行过程中改变方向。为了应对这种情况，开发人员构建了这样的系统，允许智能体暂停其工作，保存当前状态，并在稍后从该点恢复，甚至可以分叉其路径以同时探索多种选择。这些能力——保存进度快照、分支进入新路径，或将不同的结果合并在一起——被称为“执行编辑”（execution edits）。它们对于灵活性至关重要，使得任务能够在不从头开始的情况下，实现错误恢复或探索替代方案。然而，这种灵活性也引入了深刻的风险。如果允许智能体自由地回溯或分叉，它可能会意外地重复执行关键操作，例如两次授权付款，或者丢弃一个任务仍然迫切需要的执行结果。挑战在于，如何确保当智能体请求更改其路径时，系统能够验证新的路径是否仍然安全并符合所有规则，而不依赖于智能体自身可能存在缺陷的意图描述。
研究人员开发了一种严谨的方法来解决这个问题，创建了一个能够明确判定智能体工作流变更是否安全的系统。其核心是一个“精确检查器”（exact checker），这是一个数学引擎，它不仅检查智能体的当前状态，还会审查其整个行动历史。当智能体请求保存检查点、分叉进入新分支、恢复先前状态或合并两条路径时，该检查器并不会简单地询问智能体下一步打算做什么。相反，它会查看已经发生过的不可篡改记录：调用了哪些工具、授予了哪些权限以及完成任务仍需哪些结果。随后，系统会计算从该点开始任务可能继续进行的每一种方式。它会系统性地排除任何会导致违反政策（例如重复授权付款）或任何会导致必要结果无法完成的路径。如果至少存在一条安全的路径，系统就会允许该编辑继续进行，并为智能体提供其必须遵循的特定规则以保持在该安全路径上。如果没有安全路径存在，系统则会拒绝该请求，并提供关于为何无法安全继续执行的清晰证明，从而防止智能体进入危险状态。
研究人员证明，这种方法比以往的方法更为可靠，因为以往的方法往往依赖于智能体对其工作流的描述，或者未能考虑到不同任务分支之间的复杂交互。在他们的研究中，他们表明仅仅知道过去的操作列表是不够的；系统还必须理解这些操作之间的特定关系，例如哪些调用指向同一个底层权限。他们证明，如果缺失了这段详细历史中的任何部分，系统就无法保证安全性。例如，如果系统知道已授权了一笔付款，但不知道该付款属于哪一笔特定的交易，那么它就无法防止恢复的分支再次意外授权同一笔付款。通过维护每一项调用、每一项权限和每一个所需结果的完整且精确的记录，这个新颖的检查器能够以绝对的确定性来区分安全与不安全的编辑。
为了验证他们的发现，团队构建了这个检查器的运行版本，并针对各种场景进行了测试，包括具有多达 128 种不同可能结果的复杂任务。该系统能够以极短的时间做出这些安全决策，从简单情况下的 0.11 毫秒到最复杂情况下的约 53 毫秒不等。在编辑不安全的情况下，系统能迅速识别冲突并予以拒绝，通常耗时不到 6 毫秒。研究人员还使用了经计算机程序验证的形式化数学证明，来证明其方法对于他们研究的六种工作流编辑类型均能正确运作。这些证明确认了即使在智能体进行多次变更、在崩溃后重启或不同部分系统并行运行时，该系统也能保持任务的安全性。其结果是一个稳健的框架，使智能体可以在探索和恢复工作流时充满信心，而不必担心会意外违反规则或丢失关键结果。
这项工作从根本上改变了我们对管理自主智能体的方式。它将安全性的责任从可能产生混乱或具有恶意倾向的智能体，转移到了作为一个“守护者”的受信任运行时系统。这个守护者并不靠猜测或期望，而是计算出可能的精确边界。它确保每当智能体暂停以保存进度或分散注意力尝试不同方法时，系统都已经验证了未来依然是开放且安全的。研究人员发现，这种精确度不仅是一个理论上的理想，更是一个现实，能够处理现实世界任务中非线性的复杂性质。通过直接从已发生的历史中推导出安全规则，而非从智能体当前的意图中推导，该系统为下一代自主软件创建了一个可靠的基础。能够无需担忧灾难地进行分叉、恢复和合并工作流，意味着这些智能体可以变得更加雄心勃勃，去处理那些需要探索与恢复的任务，并深知有一套精确、不屈的逻辑正在时刻监督着它们。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。