形式化定理的工程翻译
论文 §4.4 给出 6 条核心元理论定理。这里不列证明,只把每条定理翻译成"对真实 Agent Runtime 意味着什么"。理解 Confluence 是理解整个论文价值的关键。
六条定理工程翻译表
【论文原文结论 §4.4】
| 定理 | 章节号 | 工程翻译 |
|---|---|---|
| Preservation(Thm 59) | §4.4.1 | 任何规则应用后 registry 仍然 well-formed:parent 指针落在 registry 内、不同 fiber 的 provision 不相交、committed view 只指向 installed fiber。工程意义:运行时永远不会出现"悬空 fiber 引用"或"两个插件同时声称自己提供 'database'"的状态。 |
| Recovery Exactness(Thm 61) | §4.4.2 | 在 pairwise independence 假设下,对一个 fiber n 的 episode [b, u],应用其 accumulator 等于"从未加载过 n"时的状态(up to control fields)。工程意义:卸载一个插件后,环境状态等价于它从未存在过——这对 HMR、插件热替换至关重要。 |
| Ordering(Thm 63) | §4.4.3 | Provider 必须先于 Consumer 激活、晚于 Consumer 卸载;Consumer 在整个 episode 中读到的依赖解析(committed view)不变。工程意义:连接池关闭前所有 connection 已归还;数据库关闭前所有事务已提交;没有"race condition 导致 consumer 读到半个关闭的 provider"。 |
| Resolution Coherence(Thm 64) | §4.4.3 | 一个 transition 的所有 iteration 都跑在同一份 committed view 下;若中途 target 变化,要么完成转入 Active,要么经 L-Divert/L-Raise 进入 Unloading 并完全回滚。工程意义:async 加载组件时不会"半旧半新"——不会一部分 effect 用旧依赖、另一部分用新依赖。 |
| Progress(Thm 66) | §4.4.4 | 在 ≺ acyclic、len(e_n) ≤ K、fiber 名有限的前提下,non-quiescent 状态必有规则可施,且每个 fiber 的 step 数有界。工程意义:系统不会死锁(guard 一定会释放);每次配置变更最终会达到稳定状态。 |
| Confluence(Thm 73) | §4.4.5 | 在 pairwise independence、component total on provision、no failure 假设下,无论经过多少次加载/卸载/替换,只要最终配置相同,稳定状态等价于按最终配置从零启动一次。工程意义:动态历史不留痕迹——一个 Agent 经过反复替换自己组件后,等价于一次性启动最终配置。这是"自演化 Agent"的理论基石。 |
Confluence:动态历史不留痕迹
Confluence 是这套理论的高潮,值得单独展开。
直观表述:系统经过任意次数的动态加载、卸载和替换后,只要最终配置相同,其稳定状态应等价于按照最终配置从零启动一次得到的状态。
对一个自演化 Agent 来说,这意味着:假设 Agent 在运行过程中先后替换了工具 A 三次、卸载并重装了 Skill B 两次、调整了子 Agent C 的隔离 realm,只要它最终的组件配置与"某次干净启动"相同,那么运行时的稳定状态(哪些组件激活、各自的 committed view、累积的环境状态)就等价于那一次干净启动。动态历史不留下任何痕迹。
这是其他 DI/HMR 框架都没有的保证:
- 传统 DI 不支持运行时替换,无 Confluence 可言;
- HMR 需要开发者手写状态迁移函数,迁移是否正确没有形式化保证;
- 容器编排"重启即干净"是粗粒度丢弃全部状态,不是同粒度的等价。
【论文原文结论 §4.4.5】注意 Confluence 的前提:
- pairwise independence:effect 彼此独立或可交换(Def 19);
- component total on provision:每个 component 实际安装它声明的所有 key(Def 69);
- no failure:排除 failure 场景。
【论文原文结论 §4.4.5】Confluence 排除了 failure 场景(§4.3.4 的 L-Raise)——因为 failure 是真实分歧源:一个 schedule 可能 fail 另一个可能 succeed,但 Cor 62 保证 failed fiber 对 state 的贡献为 0(失败组件的副作用被完全回滚,不影响其他 fiber)。所以"失败"不破坏状态一致性,但确实让两条动态路径产生分歧(一条有失败、一条没有)。
这套证明不能保证什么
【论文原文结论 §6.1, §6.3】形式化证明只覆盖通过 Context 管理的副作用。它不保证:
- 开发者写的 inverse 一定正确(witness 条件
g(δ)=γ是义务不验证); - Context 之外的副作用(直接改全局变量、文件、数据库、外部系统)能被撤销;
- 外部 emission(网络请求、消息、邮件、支付)能自动回滚——这些一旦发出就跨出系统边界;
- 不可信插件的安全性——Context 级权限控制不能替代进程/容器/WASM sandbox;
- failure 场景下的 Confluence(明确排除);
- 依赖 key 的版本兼容与结构兼容(§6.6 open problem)。
详细前提与局限见 局限与综合评价。这套理论如何落到 DeepSeek Harness 上见 与 DeepSeek Harness 的关系。