Cheng Tan

无窗之箱中的正确

存在性等价：给 AI 的一个正确性定义

· verificationcorrectnessai

自从有软件验证这门手艺起，「规约」（specification）一直是个可以核对的东西。给你一个输出，你能判定它对不对。给列表排序：结果有序吗？是输入的一个排列吗？两个问题，都可判定。我做过的工作，大半站在这块基石上：我的系统 Cobra 验证一个数据库是否以可串行化的方式执行了事务；我们的 Orochi 项目验证一台不受信任的服务器返回的，是否就是真实计算本会返回的东西。系统各异，基石只有一块：正确性，是一个可以核对的性质。

现代 AI 把这块基石抽走了。让模型总结四百页的文档，起草一份法律文书，或者跑一个替你订行程的 agent。你盯着输出，试图判定——对，还是不对？无物应答。不是规约变得更难核对了，而是它干脆不再是一个可核对的对象。

所谓「标准解法」，是找一个参照（reference）：选定一个可信的实现，输出与之相符便算正确——把计算重跑一遍，与「金版」逐位比对。GPU kernel 的开发者就是这么做的，深度学习编译器也是这么测的。但「相等」多半是个错误的关系。一百万个浮点数换个顺序求和，末尾几位就会变动；答案依然正确，参照比对却会把它拒之门外。而若参照本身有错，你等于把它的 bug 认证成了真理。我们要的不是与某个参照相等，而是等价——并且必须说清楚，哪些差异是被允许的。

物理学早想明白了这件事

坐进一只没有窗的密闭箱子，松手放下一只球，球落了地。你是在地球上，还是在一枚以一个重力加速度飞驰的火箭里？箱内的任何测量都分辨不出。爱因斯坦拒绝追问哪一个才「真实」：若没有任何观测能区分二者，二者便是同一回事。「相同」不是绝对的，它永远相对于你能观测什么。

一只静止在地球上的密闭箱子，和一只在深空中以一个重力加速度飞驰的密闭箱子：从箱内看，任何实验都无法把它们区分开。

这种「观测等价」，我们在别的领域其实早已见过，物理学只是把它讲得格外生动：定死你观测什么，你就定死了什么算正确。

给「AI 正确性」下个定义

那就换个问法。不问「机器给出的答案对不对」，而问：我眼前这个结果，能否由机器的某一次合法运行产生？

正确 ⇔ 存在一次合法运行 e，使得 observe(e) = 所见的结果。

一个输出是正确的，当有某次合法执行能解释它。说它错，反而是更重的断言：任何一次合法运行都产生不了它。这个定义系于三个抉择。什么样的运行算合法——这就是规约的真身。什么样的两个结果算相等。以及，我们观测什么。合法运行的集合，恰好圈出了那些无关紧要的差异：浮点求和换个顺序，行；所有合法运行都得 3、你却给我 7，不行。

如果你觉得眼熟，那就对了。它与计算机科学里好几个既有概念遥相呼应。就拿可串行化来说：一段数据库历史是正确的，恰恰当存在一个与所观测到的读写相容的事务串行顺序；而 Cobra 这样的数据库校验器，全部力气都花在寻找那一个合法顺序上。可串行化从头到尾就是存在性等价，只是从没有人给这个模式起过名字。

这个定义好在哪

让我兴奋的是这个模式本身：系统再野，它也不散架。从一块芯片爬到一个 agent，你只需拧两个旋钮——放宽什么算合法，调粗观测什么——这句话依然成立。在 GPU kernel 上，合法运行是各种有效的求和顺序，你观测数值，容差为 ε。在 LLM 推理里，合法运行是解码策略允许的各种采样，你观测文本（例子见我们的 Jailbreak Oracle 问题）。到了 agent，合法运行是工具调用与外部世界的各种允许交错，你观测副作用——机票订没订上，日历改没改对。

存在性等价的三个海拔——张量、词元、轨迹。同一个问题；越往上爬，合法性越宽，观测越粗。

同一个定义，三个海拔。给它起名字，好处有二。其一，规约收拢成一个对象——合法性谓词；此后每一场「这个 AI 到底对不对」的争执，都变成一个具体得多的争执：哪些运行，我们愿意承认合法。其二，难处在哪，数一数便知：要接受，举出一次合法运行即可；要拒绝，得排除全部。

这个定义只说机器运行得合法，不说它的输出高明。结果是否有益、是否无害，是另一个问题，留待日后的文章。

结语

存在性等价是一个走到哪里都用得上的定义：一个输出是正确的，当某次合法运行能解释我们之所见——无论那次运行是一个求和顺序、一条采样路径，还是一个 agent 的轨迹。它没有让「给 AI 写规约」变容易，它只是指明了难处的住址：在合法性谓词里，在我们选择观测什么里。比起「这个 AI 对不对」，这是一个更小、也更锋利的问题——一个更好的起点。

每一个正确性问题，都是一只无窗的箱子。唯一要紧的决定，是你允许自己观测什么。诚实地做这个决定，「正确」就不再是你宣判的一纸裁决，而成为世界能够——或不能——递给你的一份解释。

参考文献