💻 computer science

Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows

本文介绍了因果过去逻辑（CPL），这是一种集成于 ZipperGen 框架中的源码级时序逻辑，它利用向量时钟监视器确保语义正确性，使分布式大语言模型智能体能够基于因果可见事件而非顺序日志，对控制流执行在线运行时验证。

原作者： Benedikt Bollig

发布于 2026-05-21

📖 1 分钟阅读☕ 轻松阅读

原作者： Benedikt Bollig

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一个由专门的人工智能代理组成的团队，共同协作完成一个大项目，例如在代码合并到软件系统之前对其进行审查。在旧有的思维方式中，我们可能会设想这些代理在一条完美、单一的对话线中相互交谈，就像电话录音一样，每个人都以完全相同的顺序听到所有内容。

但在现实中，这些代理就像身处不同时区的人们一样异步工作。他们发送消息、开展各自的工作，并以不同的速度做出决策。有时，代理 A 会根据收到的一条消息做出决策，却未意识到代理 B 已经发现了一个关键错误，并发送了一条新消息，而这条消息尚未到达代理 A 的桌面。

本文提出了一种处理这些决策的新方法，以确保团队不会基于不完整或过时的信息做出错误决定。以下是使用简单类比进行的分解说明：

问题：“乱序”邮箱

想象你是一位经理（即“提交者”），正在等待两位检查员的报告：一位是“测试运行器”，另一位是“安全守卫”。

陷阱：你收到一份报告称“测试通过”。你正准备批准该项目。
现实：安全守卫实际上在测试通过后发现了一个重大漏洞，但其新报告仍卡在邮件系统中。
错误：如果你仅仅按照消息到达的顺序查看简单列表，可能会认为一切正常。但如果你查看“因果”现实（即此时此刻你实际所知的情况），你尚未知晓该漏洞。

本文主张，我们不应基于“完美、全局的日志”（记录所有发生之事）来评判团队的决策。相反，我们必须基于决策者此时此刻因果可见的内容来评判他们的决策。

解决方案：“因果过去逻辑”（CPL）

作者为代理在做出决策时创建了一种新的“语言”。你可以将其视为代理在点击“批准”之前可以阅读的智能清单。

代理不再仅仅询问：“我收到过‘通过’消息吗？”而是会问：

“测试运行器是否因果地看到了测试通过，而我是否因果地看到过此后任何表示测试失败的消息？”

这种逻辑允许代理说：“我看到了‘通过’消息，且尚未看到‘失败’消息，因此我可以继续。”它还允许代理检查具体细节，例如：“这个‘通过’消息是否与我此刻正在查看的同一版本代码相关？”

工作原理：“向量时钟”背包

为了实现这一目标而无需中央主管监控所有人，每个代理都携带一个背包（称为“向量时钟”）。

每当代理执行操作或接收消息时，他们都会更新自己的背包。
当他们向朋友发送消息时，会将背包装入信封内。
当朋友收到信封时，会取出背包，并将其与自己的背包合并。

这个背包确切地告诉代理：“我知道测试运行器做了 3 件事，安全守卫做了 2 件事。”无论消息是否延迟到达，背包都能确保代理确切知道在此特定时刻他们拥有哪些信息。

“守卫”机制

在此系统中，“守卫”并非站在外部事后检查日志簿的安全人员。守卫是直接写入工作流中的规则。

旧方式：工作流运行并结束，然后监控器检查：“嘿，你因为漏掉了一条消息而犯了错！”（为时已晚，无法补救）。
新方式（CPL）：工作流在决策点暂停。代理检查其“因果过去逻辑”规则。如果规则显示“我尚未看到最新的失败”，工作流将自动停止并要求重新检查。它在错误发生之前便予以预防。

现实世界示例：代码审查

本文使用代码审查场景来证明该方法的有效性：

设置：“提交者”等待“测试运行器”和“安全代理”。
场景：测试运行器表示“通过”。提交者准备合并。
转折：测试运行器随后发现了一个失败，但该消息尚未到达提交者处。
结果：由于提交者使用 CPL，他们查看自己的“因果过去”。他们看到了“通过”，且未看到“失败”（因为尚未到达）。因此，他们继续执行。
- 等等，这难道不危险吗？ 本文指出：不。策略是“若未看到失败则合并”。如果失败已经到达，守卫本会阻止合并。如果失败稍后到达，系统设计为能够处理这种情况（例如稍后重新检查），但不应因提交者无法预知未来而责备他们。

总结

本文赋予分布式人工智能代理一种能力，使其能够基于此时此刻实际所知的内容做出明智、安全的决策，而非基于完美观察者在稍后才会知晓的内容。它利用“背包”系统来追踪信息流，并使用特殊的“逻辑语言”来确保代理仅在因果证据支持其前进时才继续行动。这将运行时监控从“尸检”（犯罪后查看尸体）转变为“交通信号灯”（在撞车前让车辆停下）。

技术摘要：用于分布式 LLM 代理工作流运行时验证的因果过去逻辑

问题陈述
在分布式大语言模型（LLM）代理工作流中，多个代理在没有共享内存的情况下异步交互，无法像产生单一顺序日志那样被有效监控。在异步执行中，代理做出的决策（即“生命线”）仅依赖于对其因果可见的事件。在全局顺序日志中较早出现的事件，在本地可能尚未被知晓；而本地最近发生的事件，可能并未反映远程代理的最新状态。

现有的运行时验证方法通常依赖顺序轨迹或事后日志分析。然而，对于代理工作流而言，这是不够的，因为监控应当在决策点影响执行。如果决策者（例如提交者）尚未因果地看到干净的测试结果，系统就不应合并并在稍后报告违规；而应立即阻止合并或请求重新运行。此外，LLM 应用中的标准防护机制通常将执行视为顺序日志，忽略了正确分布式决策所需的因果结构。

方法论
作者通过引入因果过去逻辑（CPL），扩展了ZipperGen框架（一种用于分布式 LLM 代理的编排编程系统）。

形式化模型（消息序列图 MSCs）：执行被建模为消息序列图（MSCs），其中事件分布在各个生命线上。因果顺序由局部继起和消息传递的自反传递闭包定义。每个事件都携带局部变量的估值。
因果过去逻辑（CPL）：CPL 是一种小型的过去时态逻辑，设计为源代码级的防护语言。
- 语法：公式包括沿单条生命线解释的标准过去时态模态（Previous $Y$ ，Since $S$ ），以及因果模态 $@A(\phi)$ ，该模态在当前事件因果可见的代理 $A$ 的最新事件处评估 $\phi$ 。
- 变量访问：该逻辑支持如 $@A.x$ 的项，用于读取代理 $A$ 的最新因果可见事件处变量 $x$ 的值。
- 语义：防护条件 $\phi@A$ 由拥有该生命线的代理 $A$ 在决策点（分支或循环）本地评估。真值决定控制流。该逻辑是非严格的：如果没有代理 $A$ 的事件可见，则公式评估为假。
在线监控算法：
- 作者提出了一种分布式监控算法，其中每个生命线维护一个向量时钟和最新值视图。
- 状态：每个代理维护一个向量时钟，以跟踪从其他每个生命线看到的事件数量。它还维护一个部分映射，用于存储来自其他生命线的布尔公式和变量值的“最新值视图”。
- 传播：当代理发送消息时，它会附加其当前的向量时钟和最新值视图。收到消息后，代理将这些视图与其本地状态合并，更新其向量时钟，并自底向上重新评估所有防护条件。
- 正确性：该算法确保本地计算的监控值与消息序列图（MSC）上防护条件的指称语义相一致。

主要贡献

因果过去逻辑（CPL）：一种专为分布式代理工作流设计的新型逻辑，它将标准的过去时态算子与对其他代理最新可见状态的因果访问相结合。它允许防护条件表达诸如“所需测试已通过，且在因果过去中未看到任何失败”的条件。
源代码级防护：与事后检查日志的外部监控器不同，CPL 公式集成在工作流的源代码中。它们由决策者在线评估，以直接影响控制流。
基于向量时钟的分布式监控：一种高效的在线监控算法，利用向量时钟和最新值视图来跟踪因果可见性，无需中央观察器或全局顺序日志。
形式化验证：消息序列图（MSCs）、CPL 满足性、本地评估器以及监控正确性定理的定义已在 Lean 4 中机械化并得到验证。论文证明了防护条件的本地运行时评估与其在当前事件处的指称语义相匹配。
原型实现：在 ZipperGen 框架（Python）中的原型实现展示了该方法的可行性，表明防护条件可以跨生命线比较变量（例如，确保测试结果对应于当前的合并候选项）。

结果

理论方面：论文证明了引理 1（本地评估正确性）和引理 2（监控状态不变量），最终得出定理 1（监控正确性）。这些证明确立了分布式算法能够基于拥有该生命线的代理所见的因果过去，正确计算任何 CPL 公式的真值。
实践方面：ZipperGen 中的原型实现成功处理了分布式代码审查的示例，其中提交者仅在因果地看到特定候选项的测试通过和安全扫描后，才决定合并补丁；如果在因果过去中可见失败，则阻止合并。

意义
论文认为，分布式 LLM 代理工作流的运行时验证必须超越顺序日志分析。通过将监控视为协调语言（通过源代码级防护）的组成部分，系统可以基于决策点可用的因果可见信息做出正确决策，而无需等待全局日志或中央观察器。这种方法解决了分布式编程中的根本难题，即局部决策依赖于部分的因果视图。这项工作弥合了编排编程（投影到本地代理的全局规范）与运行时强制之间的差距，确保安全性和协调属性能够动态且因果正确地得到执行。