DeepSeek 北大这篇新论文,把「撤销」做成了数学

作者:龍德明宇

系统能抹除自己边界内的历史,但抹除不了对世界造成的状态——这不是一句哲学格言,是一篇 88 页论文用定理写出来的结论。

装了个 VSCode 插件,想卸掉,弹窗:需要重启。为什么「装了再卸」这么简单的操作,现代软件都做不干净?

论文抓取了 VSCode 下载量前 100 的扩展:87 个含可执行代码,卸载都得重启宿主;官方给过扩展间依赖声明机制,可前 100 个扩展里只有 7 个声明了对其他扩展的依赖——不是不需要,是机制太弱,撑不起来。

但这篇论文值得说的点不在「卸载麻烦」这个工程痛点。它把「卸干净」做到了定理级别——而且在证明的过程中,它对自己下手非常狠。

一、先说它在做什么

论文《A Programming Paradigm for Spatiotemporal Composability》,DeepSeek-AI 与北大联合,三人署名(Yifan Shi、Wei Zhang、Tianyi Cui),88 页,8 月 13 日挂在官方 GitHub 的预印本,标注还在活跃修订中。

它处理的是动态组合:函数调用、模块导入这些静态组合,程序编译打包时就固定死了,理论很成熟;而运行时的装、卸、改,业界长期只有「重启进程」「上容器」这类粗办法。

论文提出「上下文范式」,按两个正交维度展开:时间可组合性——组件移除时,它对共享环境的全部修改被完全、安全地逆转;空间可组合性——组件只声明自己需要什么,运行时自动解析依赖、依赖变化时自动重连激活。

落到机制上就两个:

可逆效应:每个上下文操作自带一个显式逆操作,运行时用「逆累积器」自动跟踪。直觉是系统自动记账——每个动作发生时,它的撤销步骤被自动记下;组件一卸载,账自动冲销,不需要谁记得去清理。

反应式共效应:组件只声明「我需要什么」,上下文变化被自动归类为激活、停用或中性,驱动组件起停。像插座声明「我要 220V」,电路一变自动断电,不用自己盯着。

案例是 Koishi 聊天框架:4000 多个社区插件、4 年生产运行。论文形式化的是其底层 Cordis v4,Koishi 当前生产用的是同源框架 v3——不是纸上谈兵。

二、三个反直觉的定理

机制说完,真正让这篇论文区别于「又一个插件框架」的,是三条定理。

第一击,恢复精确性(Theorem 61)。 前提:各步骤两两独立——粗说就是,各组件的效应之间可交换、互不打架。结论:对任何一个组件运行它的逆累积器,得到的终态,与「这个组件从未启动过」不可区分。

直觉翻译:一个组件跑过又走了,系统里不留它的任何贡献——不是「清理得干净」,是「从未发生过」。而且是结构性保证,不靠开发者写清理代码的自觉。

第二击,汇合定理(Theorem 73),全文最重的一条。 前提三条:最终停下来时,没有一个组件实例处于失败状态;各步骤两两独立;每个组件承诺提供的功能,激活完成时确实都装好了。结论,论文原文:

“whatever sequence of activations and deactivations a running system has been through, the state it quiesces at is the one the same insertions and retirements would have produced had each component that ends up active been loaded once, in dependency order, and none ever unloaded.”

翻译过来:一个被装装拆拆、折腾了无数次的系统,最终停下来的状态,和「一开始就配好、从未动态操作过」的那套系统不可区分。论文自己的总结只有一句:dynamic history leaves no trace——动态历史不留下任何痕迹。

论文还给了个类比:这是动态组合版的「增量计算与从零重算一致」。

第三击,总能稳定(Theorem 66)。 前提:依赖关系无环、单组件步数有界、组件集合有限。结论:无死锁、步数有界——任何动态折腾最终都会停在一个稳定点上,系统不会僵死在半装配状态。「动态系统最终会稳下来」从运气变成了定理。

读到这里你可能还没直观感受,我们做个思想实验:想象一台修了又拆、拆了又装的机器。最后一次拆装结束后,它每个零件的状态、每处配合的间隙,都和「出厂即此配置、从未动过」的那台完全一样。那它「经历」了什么?

这台机器自己无法回答——因为承载经历的痕迹,已经不存在了。

三条定理都带前提,前提有多苛刻,第五节回来算账。但先说清楚一件事:这不是时间倒流。

三、这不是时间倒流,是「观察等价」

论文在这一点上出人意料地诚实。它自己承认:恢复不是把状态变回字面上的原来,而是「观察等价」——两个状态等价,当且仅当没有任何观察者能区分它们。

论文举的例子很具体:free 释放内存块,不会恢复 malloc 之前的堆布局;生成名被逆操作丢弃后,下次创建拿到的是全新的名字。物理历史没有恢复——内存堆的布局变了,名字的编号也变了。

那抹除掉的到底是什么?是任何观察者通过这套系统能够区分出来的因果痕迹。

所以「回到过去」不存在,「无法区分于从未发生」存在。论文要的是后者,也只承诺后者。

这个自我设限,比任何外部泼冷水都有信息量:它没声称恢复物理状态,它只声称恢复可观察的状态——承诺到哪里,理论就诚实到哪里。

四、最微妙的部分:撤销发生时,没有谁在负责

回到传统做法作对照。今天的插件系统(OSGi、Eclipse、IntelliJ、VSCode),卸载清理靠开发者手写 unload 回调。论文点出病根:逆操作和操作是脱钩的,原文叫「the inverse is an unenforced duty」——逆是一份不被强制执行的义务,忘了写,资源就静默泄漏。

论文的做法是把每个逆操作和它对应的正向操作结构性配对。原话:「a component’s teardown is derived from its loading rather than written alongside it」——组件的拆卸由它的加载派生出来,不是在旁边另写一份。效果,还是论文原话:「原本依赖开发者自觉的正确性,变成了范式的结构性质。」

那么卸载发生的那一刻,谁在「负责清理」?

【本文推演】不是开发者——他没写清理代码;不是用户——他什么都没做;不是组件——它只是被停用。是结构在清理。没有谁为「抹除」负责。

顺带一句:论文 Introduction 明确点名了 self-evolving agent harnesses——未来的 Agent 运行时,可能一边持续服务,一边生成并部署对自己组件的修改。如果这套机制用到自进化 Agent 上,一个绕不开的问题会立刻浮出来。这件事的真正分量,放在最后说。

五、边界:抹得掉内部历史,抹不掉对外状态

这套机制能抹掉一切吗?不能。论文 6.1 节专门划了系统边界。

边界之内的位置——系统能独占修改、且能恢复的地方——可跟踪、可撤销、可抹除。边界之外——做不到这两点的地方——不可逆,只能补偿。

关键在一个两阶段结构:获取阶段在边界内,open(打开文件句柄)、malloc(申请内存)、fork(创建子进程),都可逆;发出阶段跨出边界,write(写磁盘文件)、send(发网络数据包)——数据一旦出去、他人可能已经读到,就收不回来了。

对收不回的操作,论文给两条路:扣住不发,直到确定状态会持久;或者补偿——删除已创建的文件、退还已扣的钱。但补偿是「粗一点的撤销」,论文承认得很干脆:补偿动作按同样的后进先出顺序复合(类似叠盘子:最后放上去的最先拿下来),但前面那套定理保证,对这种更粗的等价不再自动成立,要重新证明。

现在来还第二节欠的账。这三条定理的前提,工程上大多好满足——依赖无环、组件数量有限、没有组件实例异常失败、承诺的功能装好,都是常规约束。真正重的一条是「两两独立」:无痕抹除只在效应可交换的前提下成立,纠缠的因果只能按后进先出顺序、或靠声明的排序处理。【本文推演】完美的因果抹除,是对「无纠缠世界」的承诺——它同时暴露了自己的理想化边界。

一句话收束:系统能抹除自己边界内的历史,但抹除不了对世界造成的状态。

六、对 Agent 发展意味着什么

技术上一句话,不展开:动态组合是 Agent 自进化的地基——Agent 要能安全地装、卸、改自己,过去只能靠重启和容器隔离这类粗办法;这篇论文给出的是带证明的形式化地基(预印本,尚待同行评审)。

具体三个「意味着」:

  1. 从「重启才能改」到「运行中可改且不留痕迹」——自进化不再是停机事件;
  2. 从「开发者手写清理」到「结构保证清理」——组件生态可以放开让陌生人写,正确性不依赖人品;
  3. 【本文推演】从「系统有过历史」到「系统与历史无关」——这对「Agent 要为自己的行为负责」的讨论提出了一个绕不开的新前提:如果痕迹可以被结构性抹除,「做过什么」的证据还剩下什么。

延伸阅读:


Logo

欢迎加入DeepSeek 技术社区。在这里,你可以找到志同道合的朋友,共同探索AI技术的奥秘。

更多推荐