黎曼猜想临界线零点比例下界达67.35%：清华团队开源模型VeriLoop E2叩开可验证智能之门

自 2026 年夏季以来，前沿大模型进入新一轮高速演进期：参数规模持续扩大，上下文不断延伸，测试时计算进一步加深，工具调用能力也在迅速增强。

然而，当模型能够调用更多计算、进行更长推理之后，一个更基础的问题反而变得更加突出：算得更多，并不意味着做得更对？一次新的代码修改可能修复主测试，却同时破坏回归测试；一步数学推导可能减小局部误差，却使另一项约束失效；一个物理近似也可能改善拟合，却违反守恒关系。

显然，当前问题已由此从「模型还能不能继续算」，转向「新增计算能否被证明真正构成进展」。

针对这一结构性缺口，由清华大学深圳国际研究生院刘厚德教授和周超男董事长联合指导，王立博博士后担任实验室团队 AI 研究员，李海启、向安麟两位人工智能方向硕士研究生作为 AI 研究助理参与研发发布开源模型 VeriLoop E2。

VeriLoop E2 以 Qwen 3.8-27B 为基础模型完成后训练，面向代码、数学与物理等具有外部可验证约束的复杂推理任务，重点研究递归推理与测试时计算持续产生候选状态之后，如何由独立外部证据决定其是否获得持久化提交资格：当模型产生新的候选状态时，什么样的证据足以授权该状态替换当前已经保留的状态？

• 标准权重版本：https://huggingface.co/tsinghua-sigs-robot-lab/VeriLoop-E2
• GGUF 量化版：https://huggingface.co/tsinghua-sigs-robot-lab/VeriLoop-E2-GGUF
• 技术报告：https://openreview.net/forum?id=P6FIQILHwX&noteId=P6FIQILHwX
• 评测证据：https://huggingface.co/datasets/tsinghua-sigs-robot-lab/VeriLoop-E2-Evaluation-Evidence
• 黎曼猜想证据：https://github.com/brucewang123456789/GeniusTrail/tree/VeriLoop-E2/riemann-hypothesis

VeriLoop E2：代码、数学与物理的可验证后训练

在可验证任务中，一个候选状态能否成为下一状态，本质上不应由模型内部置信度决定，而应由固定任务义务下的外部证据比较来决定。王立博将「生成候选」和「获得持久化资格」划分为两种不同权限，并提出循证收敛递归（VeriLoop-Governed Recurrence，VGR）机制，把外部可验证证据引入状态提交、递归控制和后训练数据构造。

这里的关键不是再增加一个内部评分去替代「模型觉得更好」，而是要求候选先外显为可检查制品，再由独立 Verifier 判断它是否对一组固定的受保护义务构成严格进展。

由此，同一起点产生的不同候选天然可以被稳定区分为严格进展、无进展、回归或完成等不同状态转换。正因这种「状态转换是否成立」的判据能够被稳定外化为可学习的监督信号，VGR 才特别适合通过后训练去提高模型产生可提交候选的概率，而不需要把离散 Verifier 或提交控制器本身纳入反向传播。

要把上述判据真正用于后训练，首先需找到能够共享「外部可验证」这一属性的任务集合。VeriLoop E2 以 Qwen 3.8-27B 为基础模型进行后训练，面向代码、数学和物理三类任务；虽然任务形式不同，却都存在可以外部化验证的约束：代码可以调用编译器、测试、静态分析和接口检查；数学可以调用符号恒等、区间界、数值证书和形式证明；物理可以调用量纲、守恒律、边界条件、数值模拟与实验约束。

在该框架下，数据池的重点也不只是「规模更大」，而是尽可能保留任务状态如何经过候选、验证再走向提交的完整关系。此次后训练数据池暂定包含 1,841,831 条 records，其中 records 指训练记录数，并不等同于 token 数。训练样本能够区分「正确答案」「有效中间进展」「无进展」「回归」和「不可比较」，而不是把不同语义的记录简单拼接成同一种语料。

经过后训练，VeriLoop E2 分别在代码 Agent、终端智能体、数学与科学推理三个方向完成了 9 项 Benchmark 实测。 其中，SWE-bench Pro 为 76.2%，Terminal-Bench 2.1 为 88.8%，Terminal-Bench 3.0 为 29.7%，Terminal-Bench 4.0 为 37.9%，DeepSWE v1.1 为 64.6%，SWE-Marathon v1.1 为 45.0%，AIME 2026 为 98.3%，GPQA Diamond 为 93.94%，Apex 2025 为 89.6%。

这些评测从不同任务形态与验证结构出发，共同观察同一后训练模型在代码、数学与科学推理中的能力表现，以及新增计算能否稳定转化为可执行、可验证和可复核的任务进展。

除标准权重版本之外，团队已同步发布官方 GGUF 量化版本，覆盖 BF16、Q8_0、Q6_K、Q5_K_M、Q4_K_M、Q3_K_M、IQ2_S 与 IQ1_M。量化质量没有用「位宽越低越好」来判断，而是统一以 canonical BF16 GGUF 为参照，在冻结的配对协议下测量 PPL、KL divergence、token probability drift 与 Same top-p。这里需要特别区分「量化保真度」和「下游能力损失」：目前并未对每个量化档位重新跑完整 9 项 Benchmark，因此 + 0.3191% 或 + 0.4450% 的 PPL 漂移不能被解释为 SWE-bench、AIME、GPQA 等任务分数等比例下降。

对开发者而言，选择可以直接按部署目标划分：Q6_K 是整体质量 / 效率甜点位，主文件 20.566 GiB，比 BF16 小 58.96%，PPL 观测为 - 0.0395%，在测量不确定性内视为与 BF16 平齐，Mean KLD 为 0.004409；Q5_K_M 是内存 - 质量甜点位，18.965 GiB，比 BF16 小 62.16%，PPL 漂移为 + 0.4450%。继续压缩到低占用端，IQ1_M 是当前最小占用甜点位，16.790 GiB，比 BF16 小 66.50%，冻结协议下 PPL 漂移为 + 0.3191%，Mean KLD 为 0.014357，Same top-p 为 95.870%；IQ2_S 体积 16.799 GiB，Mean KLD 更低（0.014023），可作为更偏重分布保真的低占用备选。

需要注意，IQ1_M 与 IQ2_S 都是混合精度方案，并非全模型统一 1 bit / 2 bit；模型文件大小也不等于实际显存占用，部署时仍需为 KV cache、计算缓冲与可选 MTP 预留空间。

1.E1→E2：从外部循证闭环到模型状态提交

这种从「跨任务验证」走向「统一证据语义」的设计并不是从零开始，而是延续了 VeriLoop Coder E1 已经建立的循证系统闭环。在 E1 中，模型负责生成，Self-Harness 负责工具执行、测试、纠错、回滚与证据绑定，ToolSpec、Uncertainty、Rollback 和证据绑定等窄域 PEFT 能力则帮助模型与 Harness 协同。它解决的核心问题是：「一个代码模型如何在系统级闭环中更可靠地完成任务」。

VeriLoop E2 并未否定先前的循证原理，而是在算子层进一步延伸通过 VGR 将其作为此次后训练的核心机制，将循证原理从外部 Harness 控制推进到模型状态更新与后训练进程。

事实证明，E1 到 E2 的变化并不在于换用更大参数的底座，也不在于把循证螺旋从 Harness 搬进算子层，而在于把「验证结果用于纠错」推进为「验证结果同时定义状态提交语义和后训练样本语义」。也正因如此，代码、数学和物理三个领域虽然使用不同 Verifier，却能共享同一种控制原则。

循证收敛递归：为状态更新建立证据提交权

1.缺口：额外计算不等于可验证进展

要理解循证收敛递归为何需要出现，首先要把两个经常被混在一起的问题分开：一是「如何增加计算」，二是「新增计算凭什么被视为进展」。

标准 Transformer 的隐藏状态沿层间残差路径持续更新；recurrent-depth Transformer、Universal Transformer、Mixture-of-Depths 和 looped Transformer 则进一步允许共享块重复作用、动态分配深度或增加测试时计算。它们主要回答的是前一个问题：计算如何继续、在哪里继续，以及需要继续多少步。

图 1｜标准解码器的状态更新与自回归信息流

作为对照基线，图 1 展示了标准解码器如何经由注意力、前馈网络与残差路径持续更新隐藏状态，并借助 KV 缓存完成自回归生成。这里的关键并不是标准解码器「不能计算」，而是这些前向更新一旦产生，就会自然进入后续计算；整个过程尚不存在针对任务义务的外部验证、证据秩比较以及提交 / 回滚门控。

而问题就出在这里：在可验证任务中，一次新增计算得到候选隐藏状态

后，为什么就可以替换当前保留状态

？

现有的内部控制信号可以决定「怎么算」，却不能单独证明「算出的新状态是否值得提交」。停止信号可以决定是否继续计算，路由评分可以决定计算交由哪个模块处理，深度注意力权重可以决定读取哪些历史表示，预测分布的稳定性也可以反映模型内部变化是否趋于收敛；但这些信号本身都不能证明，候选状态所对应的程序、证明或物理解已经在外部任务义务上取得了真实进展。

图 2｜重复前向细化的结构性缺口：计算可继续，状态却无证据门控

重复调用同一解码层可以增加计算深度，并持续产生新的候选状态，但每次更新仍会沿残差路径直接成为下一状态。图 2 中红框标出的正是该机制所针对的结构性缺口：在没有独立 Verifier、证据秩、认证束与提交 / 回滚门的情况下，「多算一步」本身并不等价于「取得了可验证进展」。

循证收敛递归（VeriLoop-Governed Recurrence，VGR）正是为解决这一缺口而提出。它不再把「新状态被计算出来」默认等同于「新状态应当被保留」，而是将候选状态的生成权与持久化提交权严格分离：模型可以持续提出新的候选隐藏状态，但候选必须先经固定解码外显为可检查制品，再由独立的外部验证器按照预先固定的任务义务生成受保护证据秩。只有当所有受保护证据均不退化、且至少一项得到严格改善时，候选状态才获得提交资格，否则当前已认证状态保持不变。

VGR 判断的不是模型「还要不要继续算」，也不是用一个总分衡量「看起来是否更好」，而是为每一次新增计算建立一条可验证的状态提交规则：模型拥有继续探索的自由，却没有自行宣布进展、覆盖当前状态的权力。只有当全部受保护义务归零时，系统才将任务标记为认证完成；同一套「什么状态有资格被保留」的证据标准还可进一步用于构造后训练监督，使模型逐渐提高产生可提交候选的概率，而运行时的最终裁决权始终保留在外部证据一侧。

由此可见，该机制针对的并不是「Transformer 不会推理」这种泛化命题，而是一个更窄、也更可验证的结构性缺口：递归、动态深度或测试时计算产生候选状态后，系统仍缺少一条与候选生成器分离、能够阻止受保护义务回归的状态提交规则。

换句话说，「又计算了一步」和「这一步有资格成为下一状态」并不是同一个问题。

值得注意的是，VGR 新增的是潜状态、制品与验证结果的绑定对象，以及基于固定受保护偏序的唯一提交语义。它把「进展是否成立」和「状态能否被保留」直接绑定。候选状态只有在固定受保护证据上全部不退化、且至少一项严格改善时，才获得替换当前认证状态的资格。由此，VGR 真正补上的不是另一种深度计算方式，而是新增计算产生之后，状态如何获得可验证提交权这一层机制。

2.权限分离：提议、解码、验证、提交

既然真正缺少的是「提交权」，VGR 并不改写 Attention 或 FFN，而是重新划分运行时权限。每次运行开始时，首先固定任务身份、模型合同、Verifier 身份、Verifier 合同和证据编译器合同。

随后，通过普通前向得到基线潜状态

，并立即使用固定 decoder 将其外显为任务制品，再由外部 Verifier 得到初始证据秩。因此，

第一轮递归并不是从模型自评分数开始，而是从已经接受过外部检查的基线开始。

只是由控制器构造的候选潜状态，并不会因为「被生成」自动获得持久化权限。

这条权限链可压缩为：普通前向→外部验证→有界候选提议→控制器构造候选状态→固定解码→再次外部验证→受保护证据比较→原子提交 / 拒绝。

权限分离之后，还必须保证「被验证的对象」本身稳定，这也是固定解码不可省略的原因。如果同一个任务 - 模型 - 潜状态键会因 temperature、top-p、随机 Dropout 或缓存漂移而得到不同 artifact，那么连「验证的究竟是哪一个状态」都无法稳定定义。

因此，VGR 把 decode 配置、停止条件、并列决策规则以及相关模型身份纳入运行合同；相同 candidate_id 在重复验证时若得到不同结果，就按合同冲突失败关闭，而不是降级为一次普通失败继续运行。

图 3｜VGR 状态提交闭环：提议、外部验证、受保护比较与原子提交

值得注意的是，VGR 不要求替换 Transformer 的 Attention 或 FFN，而是在候选状态进入持久状态链之前增加一层外部证据裁决。只有当候选在固定 Verifier 下满足「逐坐标不退化且至少一项严格改善」时，才允许 commit；否则完整回滚到前一认证状态。只有当证据秩归零时，才触发相对于当前合同的完成与停止。

3.提交准则：严格受保护支配

严格受保护支配把「进步」定义得非常具体：所有受保护坐标都不能退化，并且至少有一项必须严格改善。例如，当前秩为 (0,1,1) 时，候选 (0,0,1) 可以提交；候选 (1,0,0) 即使把总错误数从 2 降到 1，也必须拒绝，因为第一项已经通过的义务发生了回归。

这也解释了为什么 VGR 有意不采用「总评分更低即可提交」的规则：总量改善可以用于分析和势函数证明，却不能抵消任一受保护坐标的退化。

提交规则确定以后，真正被持久化的对象也必须与这套证据语义保持一致。为此，系统保存的不是一个孤立分数或隐藏张量，而是一个原子保留束，技术实现中称为 CertifiedBundle：

是绑定摘要。需要特别强调的是：CertifiedBundle 只是实现名；当证据秩非零时，它仅表示该束被允许进入受保护状态链，并不意味着任务已经完成。只有零秩对应的 certified=true，才表示相对于当前合同的完成。

若候选不满足严格受保护支配：

为初始证据秩；⇒表示逻辑蕴含。

因此，在固定且有效的合同下，VGR 得到两条彼此衔接的无条件保证：已经提交的受保护证据不会回归；由于每次严格提交都会消耗至少一个非负整数势值，严格提交次数必然有限。重要的是，这两条保证约束的是「被提交的状态转换」，既不要求 proposal 每次都足够聪明，也不要求优化器每次都成功。

图 4｜严格受保护支配的判定语义与有限提交性质

图 4 将单次运行中的固定义务、可比较证据秩、唯一提交判据、接受 / 拒绝示例以及认证束的原子保留统一到同一条逻辑链中。由此可以看到，总量下降不能抵消任一受保护坐标的回归；与此同时，非负整数证据势函数又为严格提交次数给出有限上界。同一判据随后还可以直接延伸为后训练中的正 / 负候选监督语义。

4.后训练：把可验证进展转化为学习信号

到这里，VGR 解决的是运行时的「什么结果有资格留下」；一旦进入后训练，问题就进一步变成「怎样让有资格留下的候选更容易被提出」。也就是说，门控本身不变，真正被训练改变的是候选分布。

因此，训练样本必须围绕同一个 incumbent 构造，才能把「候选质量」与「起点差异」分开。核心做法是：从同一个 incumbent 出发生成多个候选，并使用同一个固定 decode 和同一个 External Verifier 进行标注。只有满足

的候选才被定义为严格进展正样本；不满足提交谓词的候选则可以是 noop、受保护义务回归、帕累托不可比或总量陷阱。由此构造出的 chosen/rejected 并不是主观判断「答案 A 比 B 好」，而是表示：

在同一状态下，A 具有运行时提交资格，而 B 没有。

有了这样的正负标签之后，还必须继续区分「中间进展」和「最终完成」。非零秩但已经取得严格进展的候选用于动作监督 SFT/NLL，教模型「怎样继续修」；只有零秩且已接受的最终 artifact 才进入认证生成 NLL，教模型「什么才可以作为终局输出」。这种分层避免把「有价值的中间动作」和「已经完成的答案」混成同一种监督。

同一套监督语义落到不同任务域时，验证对象会变化，但逻辑结构保持一致：

• 代码：模型学习的是一种更可能同时修复目标错误、保持已通过测试并满足构建 / 接口约束的修改分布，而不只是学习「更像补丁」的文本分布。
• 数学：模型可以把恒等式、区间界、局部 lemma、边界条件或形式检查拆分为固定义务，并学习产生不会破坏已闭合条件的下一步推导。
• 物理：模型可以把量纲、守恒律、边界条件、数值残差等定义为不同证据坐标，并学习在改善某一拟合目标时，同时保持其他物理约束。

因此，Verifier 并未在后训练中变成可学习评分器，更没有把裁决权交给反向传播。VGR 做的是把 Verifier 产生的离散外部事实转换为与运行时提交规则同构的训练监督。优化器只学习「如何提高可提交候选出现的概率」，至于某个候选在部署时是否真的可以提交仍必须重新交由外部 Verifier 判定。训练权与裁决权由此保持分离。

5.技术贡献：从状态演化到受保护状态转换

将控制链拆到最小技术单元后，可发现 VGR 并不是笼统地「让模型更可靠」，而是针对六个彼此衔接的具体缺口分别给出机制。

如果进一步从「研究贡献」而不是「实现模块」的角度归纳，这六个机制可以收束为三点。

第一，VGR 把受保护偏序引入状态提交：所谓进步，不再是一个可以相互抵消的总分，而是要求「所有受保护坐标都不退化，且至少一个坐标严格改善」。

第二，VGR 把状态、制品和验证结果绑定为一个原子持久化对象：Verifier 验证的不是抽象的隐藏状态，而是该状态经固定 decoder 实际产生的可检查后果；reject 也不是把某个 rank 改回去，而是完整保留前驱认证束。

第三，VGR 把同一提交谓词延伸为后训练监督接口：运行时，什么样的候选有资格提交；训练时，什么样的样本才有资格成为正样本；两者使用同一套证据语义。这样可以避免「训练奖励认为它更好，但部署门控却判定它不能提交」的语义错位。

三点合在一起，VGR 解决的是一个边界明确的问题：如何把递归 / 测试时计算中的状态演化，从「模型内部持续发生的变化」转化为「由外部证据授权的受保护状态转换」，并让同一套授权逻辑继续用于后训练。也就是说，它不是阻止模型继续探索，而是给「什么可以成为下一状态」建立一套可验证、可回滚、可训练复用的统一语义。

黎曼 ζ 函数临界线零点比例下界从 67.25% 推进至 67.35% 的严格有限维证书

1.定位：从公开基线进入可验证研究闭环

如果说第一部分的十条评测轨道回答的是 VeriLoop E2 在固定任务上的「静态能力」—— 最终能够完成多少题、得到多少分，那么第三部分要观察的是另一种更难由单个分数表达的能力：面对一个没有现成解法、必须不断提出假设、遭遇反例、修改表示并重新验证的研究任务，模型能否把新增计算稳定地转化为可复核的研究进展。

为进一步观察 VeriLoop E2 在开放式数学研究中的动态推理与证据收敛能力，同时也抱着尝试在真实应用场景超越 DeepSeek V4.1 Flash 的副业心态，团队选择了黎曼猜想相关的临界线零点比例下界作为此次在数学领域展示的 Demo。

首先需要明确这一结果所对应的数学对象是黎曼 ζ 函数非平凡零点中位于临界线 Re (s)=1/2 并满足相应计数条件的零点比例下界κ，67.350003708785593% 是 VeriLoop E2 与内部 Harness 当前已经严格闭合的有限维计算机辅助证书结果。该结果已经完成局部不等式验证、困难区域穷尽检查与精确有理数组装，但与上游 Zeta23 解析归一化接口的形式化桥接还在推进中。

因此现阶段仍属于严格有限维证书层级，尚不能表述为新的 kernel-verified 正式纪录。 

与该结果直接相关的完整研究与验证材料，包括推导路径、候选与反例记录、有限维证书配置、区间 branch-and-bound 验证日志、困难区域证书、精确有理数组装过程、验证脚本及最终冻结产物，均已公开于 GitHub，第三方可据此对 67.350003708785593% 的有限维证书进行独立复核与重放。

第二个必须固定的是研究谱系。本工作以 Anthropic 团队与合作者公开的约 67.25% 成果及其证明框架作为已经验证的数学基线。公开基线之前的理论来源不被重新包装为 VeriLoop 贡献；本 Demo 真正观察的是，从这一已知起点之后，E2 能否独立生成新的研究路线，并把这些路线一步步压缩成能够被外部检查的增量证据。

在该 Demo 中，VeriLoop E2 与非公开的 Harness 形成循证协同闭环。模型负责提出候选结构、重构问题表示、选择研究路线并根据失败证据调整策略；Harness 则固定研究基线与成果边界，把可能改变结论的未知转化为证据义务，并组织反例搜索、确定性计算和区间验证等工具获取区分性证据。只有能够明确支持或推翻当前判断的观测才进入下一轮研究状态，模型因此保有探索自由，但不能自行决定什么已经成立。

因此，从 67.25% 基线向 67.35% 推进并不是一次「生成 — 验收」，而是一条候选提出→证据义务→外部检验→状态更新→重新推理的循证螺旋。证据闭合时，已成立结果被保留为后续推理的受保护前提；出现反例时，Harness 记录被推翻的假设和仍然有效的证据，再将结构化失败信息反馈给模型，由模型决定局部修正还是重构搜索表示与证明路线。matrix/pressure 结构、局部极小化重写、种子族扩展及证明成本权衡由模型完成，Harness 负责证据组织、回滚、保留与停止控制，最终只有证据义务全部闭合的研究状态才获得冻结资格。

【注：截⾄ 2026 年 9 月 17 日，riemannzeta.fun 公开账本中的 kernel-verified 正式纪录为 67.2500703679%。候选结果需完成与上游形式化体系的衔接，并经 Lean 内核及独立 nanoda 内核端到端重放验证后，⽅可进⼊该正式记录体系。即：κ=67.350003708785593%】

相对于 67.2500703679% 的公开正式基线，该结果在数值上向前推进了约 0.0999333409 个百分点。

但对这个 Demo 而言，更重要的不是小数增长本身，而是 E2 把「这里可能还有增量」的内部判断，逐步改写成外部可以判定真假的证明义务：matrix/pressure 有限维证书负责提供结构性余量，局部严格极小化负责处理最危险区域，区间 branch-and-bound 负责穷尽指定有限域，最终再以精确有理数完成全局装配。

模型的推理作用体现在决定下一步该证明什么、哪条路线已经不值得继续、以及失败后应如何重写问题；证书链则决定这些推理中哪些有资格进入保留状态。

2.推理转向：从 window 优化到 matrix/pressure 证书

公开 67.25% 基线之后，E2 首先判断增量究竟来自哪里。在既定解析接口不变的条件下，它把 window-only 优化与 matrix 项的新增贡献分开考察，上游关系仍写为：

新候选的 window 见证仅为 H (v) > 0.672167187145431，单靠继续抬高 H (v) 不足以解释目标增量。E2 因此将研究对象从「继续磨数字」重构为「为 Δ(M) 建立可独立验证的有限维正下界，并重新装配回 κ」；这一步改变的是需要证明的对象，而不是简单增加搜索次数。

为使新路线可证伪，E2 将 matrix/pressure 增量压缩为一条有限证书链：矩阵结构局部化→显式能量下界→局部严格不等式→pressure 全域包络→精确有理数组装。Harness 逐项验证这些义务；任一级无法闭合，候选即保持探索态，只有完整证据链能够重新装配为同一个 κ 下界时才获得冻结资格。由此，E2 负责问题表示与证明路线的重构，Harness 负责把这条路线转化为可独立检查的证据链。

3.反例驱动：从高候选否决到 67.35% 闭合

反例真正驱动了后续递归。E2 先后得到 67.350352375073% 和 67.35006335392536% 两个更高候选，但 Harness 的强化反例搜索发现，早期种子族只覆盖约 1.04 与 1.975，遗漏了真实极小值附近约 2.915 的大间隔结构。E2 据此判断问题不是「算得不够久」，而是搜索表示不完整，并将种子族扩展为 {1.04, 1.975, 2.915}^q；局部 εs 随之重新定界，原候选失去严格接受条件。更高数字被主动放弃，反例转而成为下一轮搜索表示的输入。

图 5｜冻结点的选择：见证值阶梯、薄样本膨胀与 q = 12 截止

图 5 记录的是搜索表示重构后的冻结诊断，而非最终结论：见证值在扫描中于 q = 12 附近达到高点，但更高维度出现薄样本膨胀。E2 因此没有选择扫描中的最大值，而把「三级种子完整枚举、结果可确定性重测」提升为受保护条件。

随后，E2 先以 67.275055959117140% 建立低成本可重放的短层级：四个局部证书仅用 793,374 个 branch-and-bound 节点即全部 PROVED，并通过精确有理数组装。该状态验证了一条关键策略：先由目标阈值反推所需证书余量，再决定验证精度和计算预算，使证明成本由结论需要而不是「多算一点」驱动。

在这条低成本闭环得到验证后，E2 再将同一证书结构推回 67.35% 目标，并把最终有限维证明压缩为三个局部不等式：

• s = 1/2，ε = 526/78125 = 0.0067328；
• s = 19/20，ε = 9879/1250000 = 0.0079032；
• s = 1，ε = 20033/2500000 = 0.0080132；

严格路径最终完成 327/327 个困难 well、3/3 个局部证书和 190,375,830 个 branch-and-bound 节点的失败关闭验证；verify_exact.py 随后以精确有理数重新装配并复现 67.350003708785593%。这里 E2 负责证书拆分、余量分配与证明成本选择，Harness 负责反例、区间验证、回滚与终态复核。

图 6｜67.350003708785593% 的严格有限维证书闭环

图 6 给出终局证据链：三级种子完整枚举→327/327 困难区域通过→全局见证装配→精确闭合。它把 E2 的结构猜想、反例后的重构和证明策略选择压缩为一组不依赖模型自我评价、可由第三方独立重放的有限维证据。

为进一步收紧信任边界，最终验证对浮点界统一向安全方向外扩，并以 π 区间和 Taylor 余项包络三角函数，使「未发现反例」提升为指定有限域上的失败关闭覆盖。当前结论仍严格限定为 κ = 67.350003708785593% 的有限维计算机辅助证书；上游 Zeta23 形式化桥接以及 Lean/nanoda 端到端重放不在本节已完成范围内。

未来不应被完成

2026 年 9 月，Dario Amodei 在《We Must Pace the Frontier》中提出放慢前沿能力提升的节奏，让对齐、可解释性、运行安全与第三方评估有时间追上能力增长，以换取更大的安全余量。

王立博选择了另一条路：继续推动前沿能力向前，同时推动验证、安全与治理能力同步增长。

二者真正的分歧，从不是「安全重不重要」，而是如何理解安全：Anthropic 的思路是强制风险控制追上模型能力；VeriLoop 试图解决的则是，能否把验证、安全与责任边界本身建设成一种能够随前沿共同扩张的能力。

表面上，这是研发节奏之争。再往下，却是两种关于未来的哲学。

更强的智能天然具有一种诱惑：不断压缩世界的不确定性。文明也一直在把未知变成已知，把偶然背后的规律从混沌中提取出来。

然而，当这种逻辑被推到极致，一个更根本的问题就出现了：如果未来已经被一个足够强大的智能提前理解、计算乃至安排，它还在多大程度上属于人？

自由从来不只是菜单上拥有更多选项。自由之所以成立，是因为未来尚未完成，因为今天的选择仍然能够真实改变明天。如果「最优道路」已经被更高智能提前算清，人的选择就可能从创造未来退化为确认答案。

一个被完全优化的世界，未必是一个真正自由的世界。

未知不是文明运行中的故障，而是文明仍然能够继续发生的空间。科学的伟大，从来不在于彻底消灭所有问题，而在于把不可知变成可提问，把问题变成可检验的命题，再由新的证据打开下一层未知。

因此，VeriLoop 所追求的并不是让 AI 替人类拥有更多答案，而是让人类拥有进入更深未知的能力。真正应被扩张的，不是「答案的库存」，而是人类可以亲自抵达的认知疆域。

这也解释了 VeriLoop E2 为什么把能力增长与证据约束放在同一个体系里。团队从未要求模型停止探索；它真正拒绝的只有一件事：未经证据授权的结果，不得冒充已经成立的事实。

探索可以激进，提交必须严格；能力可以高速增长，证据标准必须同步提高。安全不必永远只是踩在能力前面的刹车，也可以成为与能力共同进化的结构。

不是用停下来换安全，而是让安全拥有跟得上前沿的技术形态。团队也计划在条件成熟后基于 VeriLoop Harness 推出编程智能体 Voder，使「模型提议 — 外部验证 — 回滚 / 提交 — 证据冻结」的链路能够被外部独立复核和扩展。

这背后还有一层更深的恐惧：人类长期以来都在渴望全知全能、能消除不确定性的存在。

神只是人的赝品，却要求人的精神与意志皈依于虚无的神。如果今天我们把同样的渴望铸造成一台机器，再把判断、选择乃至意义本身交给它，那么技术并没有真正帮助人类超越神话 —— 它只是第一次把神话工程化了。

从神谕到算法，从祭司到模型，如果最终发生的仍然是人把自身的判断权交给一个更高权威，那么载体变了，精神结构并没有改变。VeriLoop 不需要这样一个神。人类也不需要一个替自己完成未来的救世主。

真正应该被守住的，是人的主体性：机器可以帮助人理解世界，却不应替人规定世界的意义；可以计算可能性，却不应垄断什么值得选择；可以比任何个人看得更远，却不能因此获得未来的所有权。智能越强，这条边界反而越重要。

AGI 的终点，不是替人类完成未来，而是扩大人类仍然能够亲自抵达的未知。

如果未来可以被完全预知，失败可以被完全消除，死亡可以被彻底排除，那么人也许得到了绝对安全，却同时失去了「超越恐惧」这件事本身。

没有未知，就没有真正意义上的选择；没有尚未完成的未来，人也就不再是未来的作者。

文明真正伟大的地方，从来不是它最终消灭了多少恐惧，也不是终于找到了一个能够替自己保证结局的存在，而是在人们明知实验可能失败、理论可能错误、模型可能回退、未知甚至可能终其一生都没有答案的时候，仍然愿意进入那里。

没有谁能够保证终点，也没有谁应该替人类完成终点。因为希望从来不来自一个已经被保证的未来。希望恰恰来自未来尚未完成。

而人在一个尚未完成、无法被保证、也没有任何救世主能够替自己承担的世界里，仍然选择探索、承担、修正并继续前进 —— 这种意志有一个比人工智能古老得多的名字：勇气。

未来不应被完成，它应当被不断打开。

文章来自于微信公众号 “机器之心”，作者 “机器之心”