从 Minimax 到 MRI：双轨验证是怎样长出来的

它不是一开始就存在的

现在回看 MRI 项目，我很容易把它讲成一个完整故事：先从范畴论得到跨域迁移的想法，再建立知识地图，让 AI 生成研究候选，最后用形式证明和工程复现让成果“双轨立住”。

这个故事大体符合后来形成的方法，却不符合方法出现的顺序。

我没有先设计好一套 Auto Research 范式，再拿 MRI 去执行。双轨是在项目推进中逐渐变成规则的。更早的 Minimax 可能影响了它，但当时我没有把两个项目主动关联起来，Minimax 的记录里也没有“双轨”这个名称。

更重要的是，双轨并不是“同一个研究结论需要两份不同证据”。

它来自我对问题的一种分类：逻辑问题、工程问题，以及不可知的问题——也可以暂时称为玄学问题。逻辑问题最终由形式化判定，工程问题最终由可复现的工程结果判定；第三类不在这套方法的讨论范围内。

这篇文章要追问的，是这套分类怎样从两次并不相同的研究经历里长出来。

Minimax：一个不断缩小的结果

Minimax 最初研究的是一个很简单的问题：把某种结构先验放进很小的模型里，能不能让它在参数很少时仍然具有更强的泛化能力？

我和 AI 先后尝试了六版小模型。它们在某些训练集或同分布任务上会出现好看的数字，到了真正陌生的数据上，优势却不稳定。有一版带结构的模型，分布内准确率超过了普通基线，但在未见分布上的表现只有约 3%。

继续换模型没有带来稳定结果，项目于是从机器学习转向《易经》的可计算结构：把 64 卦、384 爻和传统概念整理成数据，问这些结构到底能够解释多少文本差异。

最初出现过一个令人兴奋的相关系数：r≈0.28。

这个数字很容易被写成“结构解释了 28%”。但相关系数不是解释率，同一批材料上的拟合也不等于对未见材料的解释能力。加入按卦留出的交叉验证以后，能够稳定保留的解释率收紧到约 14%。

后来又用最小描述长度问了另一个问题：这套位置结构究竟让描述变短了多少？结论再次缩小：在当时的数据、特征与模型下，压缩收益约为每爻 0.06–0.11 bit。

它不是零，也远没有最初听起来那么宏大。

项目最后没有继续堆更复杂的模型去追逐正结果。六类模型和多种测量方式大致收敛到相近范围，剩余问题需要另一种角度，于是这条路径停了下来。

Minimax 没有证明《易经》的结构上限。它只说明：在这套材料和检验协议下，我最初看到的信号，经不起更严格的外推以后，只剩下一点有限、真实但很小的东西。

Minimax 只有一条轨道

在事后的叙述中，很容易把 Minimax 说成双轨的前身：一边生成结果，另一边寻找结果为什么可能不成立。这个说法并不准确。

Minimax 面对的是工程问题。模型有没有泛化能力、某种结构能不能稳定解释未见材料，都不是靠语言论证就能结束的问题。它们需要被实现、运行，并且在预先说清楚的条件下留下可重复的结果。

交叉验证、随机基线和最小描述长度，是这个项目中不同的工程检验方式。它们改变了测量条件，也不断收紧结论，但并没有构成另一条“形式轨”。

Minimax 真正留下的经验是：一个工程问题只有在结果可复现时才算结束。AI 可以提出假设、选择特征、编写模型、运行实验，再解释为什么结果有意义；整条链条很流畅，仍然不能代替复现。

后来回看，它可以被理解为我先经历的工程轨；但在当时，我还没有理由给它起一个由“两条轨道”组成的名字。

MRI：当另一类问题出现

2026 年 5 月，我开始 MRI 项目。

它的思想起点，是我对范畴论的一种朴素理解：对象不只由内部成分定义，也由它与其他对象的关系定义；不同领域如果具有相似的关系结构，某个领域已经存在的解法，也许可以迁移到另一个领域。

这未必是数学家对范畴论最严格的表述。它首先是一种产生问题的直觉。

我完全不懂 MRI，也不懂完成这个项目需要的数学。第一步不是让 AI 直接写论文，而是根据权威教材和文献建立本地知识地图，标记什么已经知道、什么仍有争议、什么只是候选接缝。教材也可能被推翻，但在没有能力重建整个领域时，它是我必须先接受的当前底座。

然后，AI 才开始把一个领域的结构搬到另一个领域，寻找可能的对应。

MRI 与 Minimax 不同的地方，是其中出现了大量逻辑命题：一个结论能不能从这些定义和假设推出，两个数学对象是否等价，一个定理在什么条件下成立。

这类问题即使数值上试过很多次，也没有得到最终判定。有限次实验只能说明它还没有在这些样本上失败，不能说明逻辑上必然成立。

于是，另一类问题以及它对应的终局出现了。这不是给原有的工程主张追加一次形式验证，而是把不同问题送进不同轨道。

三类问题，两条轨道

MRI 仓库在 5 月 5 日建立。到 5 月 8 日，项目协作规则里已经写下了“双轨立得住”原则。它当时最核心的一句话是：

逻辑的问题用形式化证明，工程的问题用现实来证明，构建它，得到我们预期的结果。

现在，我会把这个原则完整地表达成三类问题：

逻辑问题         → 形式化 → 在声明的定义与假设内判定成立或不成立
工程问题         → 可复现 → 在声明的条件下构建、运行并接受实际结果
不可知／玄学问题 → 出界   → 不在这套方法中讨论

前两类才构成双轨。

这不是要求每个结论都同时通过 Lean 和实验，也不是用两种工具给同一句话盖两枚印章。纯粹的逻辑问题走到形式化就可以结束；纯粹的工程问题走到可复现就可以结束。

一个研究项目当然可能同时包含两类问题，但这时需要做的是拆分命题，而不是混合证据。

例如，“某个相位耦合族在给定假设下酉等价”是逻辑问题，可以交给 Lean；“实现这个耦合以后，模拟器是否产生预期的数值行为”是工程问题，需要构建和复现。它们彼此相关，却不是同一个命题的双重证明。

至于“这个类比是否指向一个重要发现”“它最终是否具有临床价值”，如果还没有被转化为明确的逻辑命题或可复现的工程问题，就不能假装已经被双轨判定。它可以继续作为直觉、方向或价值判断存在，但暂时不进入“已经立住”的结果。

这里所谓“玄学”不是对问题价值的贬低，也不等于断言它永远不可知。它只是一个工作边界：目前无法给出形式化或可复现终局的问题，不由这套方法裁决。

双轨不是 Lean 加 Python

Lean 和 Python 只是当前使用的工具，不是双轨的定义。

形式化的对象，是逻辑问题。它要求把定义、假设和结论明确写入一个形式系统，再由机械检查器判断结论是否真的能够推出。非形式化证明可以是中间草图，却不是这一轨的终点。

可复现的对象，是工程问题。它要求说明构建了什么、在什么条件下运行、预期结果是什么，以及其他人如何重新得到它。若预期没有出现，工程命题就应当被推翻或收缩，而不是用解释挽救。

复现所需要的现实层级取决于主张本身。关于数值模拟器的主张，可以在公开代码、数据与声明模型中复现；关于 MRI 真机的主张，需要真机或体模；关于临床效果的主张，则必须进入临床数据与相应实验。用模拟结果不能替代一个自己并未提出和完成的临床验证。

MRI 目前主要完成的是形式证明，以及公开模型和软件层面的工程复现。它没有 MRI 真机、标准体模或临床验证，所以成果的边界也停在这里。

双轨仍然可能解决错问题

形式化不是把教材变成宇宙真理，可复现也不是把一次运行变成无条件的事实。

MRI 中的定义和假设来自当时能够取得的权威教材、文献与领域知识图谱。Lean 能够判定的是：在这些已经写明的定义和假设中，结论是否成立。它不能替我保证这些前提永远不会被未来的领域知识修正。

工程复现同样只在声明的模型、数据、设备和条件中有效。条件改变，结论可能随之改变。

更根本的风险发生在进入双轨之前：如果我或 AI 把领域问题翻译错了，形式系统可能严密地证明了错误问题，工程系统也可能稳定地复现了错误目标。

这不是第三条验证轨道，而是分类和建模的边界。双轨解决的是“怎样判定一个已经说清楚的问题”，不是“怎样保证最初理解的就是世界真正的问题”。

正确也可能没有意义

双轨还留下另一个没有解决的问题。

一项逻辑命题可以被正确证明，一项工程命题也可以被准确复现，却仍然平凡、已知，或者对目标领域没有新的作用。MRI 中有些跨域迁移最终只重新得到熟悉的条件数关系；有些严格成立的接口，在欠定情形下仍然看不见零空间。

它们不是假结果。

但“是真的”和“值得继续研究”不是同一个问题。

Minimax 最后停止继续增加复杂度，已经隐约触到了这道边界：微小信号存在，不代表投入更多资源一定有意义。MRI 把逻辑和工程问题各自做得更严格以后，这个问题反而更明显了。

原创性、重要性和资源优先级属于研究的准入判断。它们决定什么问题值得被送入双轨，却不是第三条真理判据，也不能取代双轨的终局。

那需要另一道门禁，而不是另一种“证明”。

方法是两段经历会合后的形状

我仍然为双轨感到自豪，但自豪的理由不是其中任何一个组件属于我。知识图谱、交叉验证、随机基线、Lean 和数值复现都早已存在。

后来回看，Minimax 可以被放在工程这一轨：构建它，让结果在声明的条件下重现。到了 MRI，逻辑命题大量出现，形式化才作为另一种终局被明确写下。

我无法证明 Minimax 直接导致了 MRI 中的双轨；当时我的意识也没有把两者串联起来。只能说，在事后的结构里，两段经历恰好可以会合：双轨不是两种证据的组合，而是一条分类规则。先判断问题属于哪一类，再把裁决权交给与它相匹配的机制；如果问题目前既不能形式化，也不能复现，就诚实地把它留在边界之外。

提出问题
→ 将复杂问题拆成可以分别判定的子问题
→ 判断每个子问题是逻辑问题、工程问题，还是暂时不可判定的问题
→ 逻辑问题进入形式化，工程问题进入复现
→ 把子问题之间的组合关系当作新的问题，再次分类和判定
→ 只在上层命题本身、必要子问题及其组合关系都走到各自终局后，声明上层问题在自己的边界内立住
→ 再用原创性与意义门决定是否值得继续投入

同一个治理单元可以作用于一个最小命题，也可以递归作用于模块、系统和完整研究。局部成立不会自动推出整体成立，因为“这些局部怎样组成整体”本身还要重新进入双轨。这里的分形不是几何学意义上的严格断言，而是结构上的自相似：问题无论缩小还是放大，都重复同一套分类、判定与组合规则。

这是否构成一种新的 Auto Research 方法，目前还不能由我自己宣布。它需要在更多领域中重复，也需要与其他自动研究流程比较。

但至少在我自己的研究里，它解决了一个非常具体的问题：当我进入一个完全陌生的领域，又无法亲自审查 AI 的全部产出时，我不再要求某个人替我相信结果。大问题可以持续拆解，多个局部可以并行推进，而每一层是否有资格重新组合，都由同一个基本单元治理。

我先问它究竟是哪一种问题，再要求它走到属于自己的终点。