清华团队开源VeriLoop E2：以循证收敛递归迈向可验证智能

魔搭ModelScope社区

49人浏览 · 2026-10-12 11:25:10

魔搭ModelScope社区 · 2026-10-12 11:25:10 发布

当前，大模型正在获得更长的推理链、更复杂的工具调用能力和更高的任务完成上限。但在软件工程与科学研究中，生成一份新答案并不等于获得了新的可靠结论：修复补丁可能引入回归，数学候选可能掩盖局部反例，物理推导也可能越过其适用条件。真正需要回答的问题，是新增计算结果何时有资格取代已有状态，并成为下一轮推理的可信起点。

清华大学深圳国际研究生院智能机器人实验室VeriLoop团队围绕这一问题发布开源模型VeriLoop E2。项目由刘厚德教授与周超男董事长联合指导；王立博博士后（Libo Wang）担任实验室团队AI研究员，是VeriLoop系列模型的原创开发者；李海启、向安麟两位人工智能方向硕士研究生作为AI研究助理参与研发与发布。E2以Qwen3.8-27B为基础完成后训练，面向代码、数学与科学推理任务，探索模型生成与独立验证相互约束的系统路线。

其核心思想不是要求模型从不犯错，而是建立可执行的提交纪律：候选必须通过固定验证合同，所有受保护义务均不得退化，并至少有一项严格改善；否则旧状态保持不变，失败信息进入后续诊断。由此，模型可以维持较强的探索能力，而已验证成果不必随每轮生成被无条件覆盖。

开源地址：

标准模型：https://modelscope.cn/models/tsinghua-sigs-robot-lab/VeriLoop-E2
量化模型：https://modelscope.cn/models/tsinghua-sigs-robot-lab/VeriLoop-E2-GGUF
GitHub 仓库：https://github.com/brucewang123456789/GeniusTrail/tree/VeriLoop-E2
OpenReview技术报告：https://openreview.net/forum?id=P6FIQILHwX&noteId=P6FIQILHwX
黎曼ζ函数零点比例计算证书：https://github.com/brucewang123456789/GeniusTrail/tree/VeriLoop-E2/riemann-hypothesis
黑洞信息悖论：https://github.com/brucewang123456789/GeniusTrail/tree/VeriLoop-E2/black%20hole%20information%20paradox

技术演进｜E1的证据治理如何进入E2后训练

VeriLoop Coder-E1侧重仓库级软件工程：模型提出补丁与行动计划，外部Self-Harness承担任务合同编译、真实执行、测试、证据绑定、修复与回滚。E1建立了“候选可生成、状态不可自行晋升”的系统习惯，但主要发生在模型外部的工作流控制平面。

E2将这一经验进一步形式化为VeriLoop-Governed Recurrence（VGR，循证收敛递归）：从已保留状态出发生成候选，将候选解码为可检验制品，再由外部验证器计算证据秩，最后通过确定性控制器执行提交、拒绝或停止。这样，原来依赖工程约定的“不要破坏已验证结果”被改写成具有精确比较语义的受保护偏序。

更重要的是，VGR也提供了适合后训练的监督信号。对同一起点产生的不同候选，系统可以根据真实验证结果区分严格进展、无进展、局部退化、不可比较与零秩完成；这些标签直接对应任务状态转移，不必把模型自信度等同于事实正确性。E2因此训练的是更高质量的候选提出、失败诊断与下一步策略，而不是让模型接管最终裁决。

实现边界需要说清：已公开发布并参加评测的是基于Qwen3.8-27B完成后训练的E2检查点，以及其与内部Harness配合形成的评测和科研轨迹；技术报告中的低秩潜状态提议器是单独定义的架构规格。除非另有端到端接入、缓存一致性与实际执行证据，不能将该潜状态算子表述为已植入Qwen主干并在所述科研Demo中实际启用。

VGR机制｜受保护偏序、原子提交与确定性回滚

3.1 固定任务合同：先确定什么必须被保护

对给定任务，系统首先冻结任务身份、模型版本、验证器身份、义务列表及其解释规则。每一项义务都具有稳定语义：可以是某个回归测试、区间不等式、证书验证条件，也可以是量纲、守恒律和适用域检查。新增候选不能通过删掉失败测试、改变验证器或重命名义务来制造“进步”。若合同发生变化，应建立新的验证运行并重新评估，不能沿用旧证据秩直接比较。

3.2 唯一提交判据：不退化且至少严格改善一项

外部验证器为候选返回非负整数证据秩向量；各维表示对应受保护义务尚未闭合的程度，数值越小表示剩余缺口越少。在合同一致的前提下，只有当候选在每一维都不大于当前保留状态，同时至少一维严格更小时，控制器才允许提交。

COMMIT ⇔ ∀j，r′ⱼ ≤ rⱼ 且 ∃k，r′ₖ < rₖ

其中，COMMIT 表示候选状态满足验证条件并获准提交；⇔ 表示充要条件，即当且仅当；∀ 表示“对于所有”，∃ 表示“至少存在一个”；j 和 k 均为受保护证据秩向量的坐标索引；r 表示当前已保留状态的证据秩向量，r′ 表示候选状态的证据秩向量，rⱼ、rₖ 及 r′ⱼ、r′ₖ 分别表示对应坐标上的证据秩，数值越小代表尚未满足的义务越少；≤ 表示不大于，< 表示严格小于，∧ 表示逻辑“且”。整个公式规定：只有候选状态在所有受保护证据维度上均不退化，并且至少一个维度严格改善时，控制器才允许原子提交；否则拒绝候选并保留原状态不变。

这并非先给多项指标加权求和、再让收益相互抵消的总分规则。例如候选修复使通过测试数量增加，却让此前受保护的安全测试失败，则属于不可提交候选；即使总体分数看起来更高，也不能覆盖旧状态。

3.3 状态管理：提交的是可追溯的完整证据包

系统需要绑定候选制品、模型及解码配置、外部验证回执与状态身份，而非只保留一句“已通过”。获准后原子提交完整候选包；不满足偏序条件时执行回滚，原有已接受制品及证据不变。拒绝候选所暴露的反例、诊断和搜索缺口可以进入下一轮探索，却不能反向污染受保护状态。

当固定义务集合对应的证据秩全部归零，且验证合同签发完成证书时，控制器进入停止状态。该保证依赖验证器及合同本身的正确性；它确保的是“已提交证据不会在合同约束下退化”，而不是宣称任何被接受的结果已经获得超出验证器覆盖范围的普遍真理。

3.4 能证明什么：有限次严格提交，不保证必然解题

对固定且有限的非负整数证据秩向量，可以定义总剩余义务量为所有坐标之和。每次合格提交至少使这一量降低1且不会增加任一受保护坐标，因此严格提交的次数必然有上界；这给出了有限次严格状态晋升的简单终止性质。它不等于保证搜索一定找到零秩证书：模型仍可能反复提出不合格候选，或遇到验证器能力边界而无法完成任务。

在潜状态实现中，还必须绑定候选激活、固定解码器、输出制品与KV-cache的一致性；否则记录的潜状态与实际解码的制品可能不对应。这也是低秩潜状态提议算子需要独立集成验证，而不能仅凭架构示意图宣称已经部署的原因。

图1 VGR受保护证据偏序：模型生成候选，外部验证器提供证据秩，控制器实施COMMIT / ROLLBACK / STOP。

为什么选择后训练｜从验证轨迹学习有效修正

VGR监督的基本单位不是孤立token，而是“当前状态—候选制品—真实验证—状态转移”的完整任务片段。大规模预训练提供代码、数学与科学知识，但通常缺少同一任务起点、冻结验证合同和可复现反事实候选；普通领域继续训练可以提高分布熟悉度，却不自然地产生严格偏序下的接受与拒绝标签。后训练则可以在已经具备基础生成能力的模型上，利用外部工具运行得到的证据，对下一步候选分布进行针对性优化。

E2公开披露的后训练语料总计1,841,831条records，覆盖仓库级软件工程、终端与工具使用、数学推理、科学问题求解、验证敏感修复及递归式轨迹。这里的record不是token数，也不意味着各训练面互斥。训练结构强调按能力面组织与调度数据、重放受保护核心能力，而非仅将多领域样本无差别拼接。

报告给出的适配路径包括QLoRA-4量化适配、bfloat16计算、梯度检查点，以及按不同能力面记录的训练过程；六个已披露通用能力面均呈现首末评估损失下降。这可以支持“后训练确实产生了优化过程及其来源记录”的判断，却不能单凭损失曲线推出某项Benchmark相对未训练基座的因果提升百分比。因果比较还需要在相同解码、Harness、测试集与评分合同下重跑原始Qwen基座。

架构上的关键分工因此保持不变：梯度更新发生在模型侧，让候选更可能被接受；验证器与提交规则保留在模型参数之外，使真实验收标准不因模型学习而自行漂移。

三个任务域｜相同的证据语义，不同的验证对象

代码、数学、科学推理不共享同一套事实检查器。VGR统一的是“先生成候选、再按固定义务验证、最后决定状态是否晋升”的治理语义，而不是强行把所有学科压成同一种打分函数。

任务域	模型侧工作	外部验证与可保留制品
软件工程与Code Agent	仓库理解、故障定位、补丁生成、策略修订	构建与单元/回归测试、接口及安全约束；保留可重放补丁、运行回执与测试结果
数学推理	构造猜想/见证、重写证明目标、反例驱动修订	精确算术、区间界、分支定界、证书重放；保留条件明确的可检查证明义务
科学与物理	机制假设、近似选择、结构归纳、边界修订	量纲/守恒/边界条件、数值对照与适用域审查；保留范围受限的研究结论

在仓库修复中，一个补丁若触发旧测试回归，便不得依赖“主错误已修复”而自动提交；在数学问题中，候选常数上升不能掩盖某个局部不等式失效；在物理研究中，自由场或有限模式下成立的关系，不能在没有新证据时直接上升为相互作用体系、黑洞蒸发动力学或普遍定理。对开发者而言，真正可复用的是这套清晰的责任切分。

图2 代码、数学与科学推理的三条验证路径：统一受保护义务与保留证据原则，保留领域专属验证器。

九项基准｜公开结果必须绑定评测合同

当前模型发布README采用九项基准的统一展示口径，覆盖仓库级修复、终端任务、数学竞赛和科学问答。下表沿用公开模型卡中的冻结发布分数；不同轨道保留各自原生评测单位，不能跨任务取简单平均，也不能把带Harness的系统成绩冒充成单独加载模型权重后的checkpoint成绩。

类别	基准	VeriLoop E2发布分数
代码 / Agent	SWE-bench Pro	76.2%
代码 / Agent	Terminal-Bench 2.1	88.8%
代码 / Agent	DeepSWE v1.1	64.6%
代码 / Agent	Terminal-Bench 3.0	29.7%
代码 / Agent	Terminal-Bench 4.0	37.9%
代码 / Agent	SWE-Marathon v1.1	45.0%
数学	AIME 2026	98.3%
科学问答	GPQA Diamond	93.9%
竞赛数学	Apex 2025	89.6%

结果解释需要同时保留证据层级：一部分对应平台原生Benchmark接口与公开任务证据；Apex 2025与SWE-Marathon v1.1作为实验室自发布评测结果呈现，不应被描述为外部平台已独立认证的官方排名。SWE-bench Pro、Terminal-Bench及DeepSWE等Agent轨道还依赖具体的工具、沙箱、Harness和评分版本。

公开评测资料的价值不只是分数，还包括任务身份、生成制品、执行或评测回执、版本信息及内容哈希。是否能够让第三方依据相同合同复核结果，比孤立展示一组漂亮数字更能说明工程可信度。技术报告还记录过其他研究评测轨道；本文九项清单以当前模型发布页为准，避免混合不同时期统计口径。

黎曼ζ函数研究｜一次由反例驱动的证书工程

标准Benchmark检验的是固定任务上的完成效果；开放数学研究还要判断模型能否在失败之后重设搜索对象，并承担可复核的证明成本。团队以黎曼ζ函数临界线零点比例相关下界为对象，在67.2500703679%的公开kernel-verified对照基线之上，构建了一个严格有限维计算机辅助证书，其冻结装配数值为67.350003708785593%。必须强调：这里成立的是特定解析框架与明确引入假设下的有限维证书，尚不是完整上游解析链的独立形式化定理，更不是黎曼猜想证明。

7.1 从候选数值转向可穷尽的验证义务

研究初期，系统并未将目标限制为继续微调既有窗口函数，而是探索matrix/pressure有限维构造，并把改进目标展开成局部不等式、困难区间覆盖、分支定界与精确有理数装配等能够独立检查的证明义务。与其反复宣称“数值提高了”，更核心的工程任务是逐条排除可能推翻该数值的反例。

7.2 更高候选为何被拒绝

探索过程中出现67.350352375073%和67.35006335392536%两个更高候选。随后更严格的反例扫描定位到约2.91的间隔结构未被早期搜索种子族完整覆盖，两项候选因此被否决。它们没有因数值占优而获得提交资格；反例则作为修订搜索表示的输入，促使后续算法补齐遗漏的几何结构。

7.3 验证器本身也需要数值可靠性

当一阶插值余项已经超过待证明的安全余量、正定Hessian判据在困难区域无法有效触发，或者单精度区间端点形成精度下限时，单纯增加搜索节点不能自动修复证书。团队在严格验证路径中采用二阶插值余项、具有保守有效性的αBB下界与双精度端点，分别处理余项控制、下界有效性和数值精度问题。验证失败可能来自数学反例，也可能来自证明工具不充分；两者必须分开记录。

7.4 先闭合低成本层级，再推进最终证书

系统先根据外部对照门槛反推所需证明余量，完成67.275055959117140%的低成本验证层级，四条局部证书合计793,374个分支定界节点。之后再推进高价值目标。冻结的严格有限维证书完成3/3条局部不等式、327/327个困难区域的严格闭合，累计190,375,830个严格分支定界节点，最终常数由精确有理数装配验证。这里3/3对应最终严格路径的局部证书数量，并不与低成本层级的4/4混为一谈。

图3 黎曼ζ零点比例研究的反例否决、严格计算与有限维证书链。图中流程示意不替代原始日志、区间边界和形式化证明。

该Demo的研究价值，在于保留了完整的“候选—反例—结构修订—验证成本优化—严格证书”路径，而不是把未经过核验的最优数值直接写成研究成果。现阶段仍需对上游解析归一化等桥接步骤进行端到端Lean/nanoda内核形式化验收；正式数学结论应始终以可检查的最终证据链和明确假设为限。

黑洞信息悖论｜从渐近引力子层析探索信息可恢复性

VeriLoop E2的第二项科学推理Demo面向黑洞信息悖论（Black Hole Information Paradox），重点研究未来类光无穷远处自由辐射引力子数据的信息可恢复性。该研究以渐近引力子层析（Asymptotic Graviton Tomography）为具体理论框架，在明确的粒子数扇区、可观测代数及连接算子条件下，将信息重建问题转化为可严格分析的代数连通性、交换子结构与定量完备性问题，为研究黑洞信息的可观测性建立具有明确适用边界的数学基础。

在理论层面，VeriLoop E2从扇区连通性出发，分析不同粒子数扇区及红外记忆结构对信息重建的限制，并通过连接算子研究可观测代数的信息完备性。进一步地，研究引入相干转移拉普拉斯算子的谱隙，将精确连通性推广为可定量评估的信息重建稳定性。在特定的双模su(2)约化条件下，推导出不随引力子数增长而退化的精确谱隙关系，并通过内部Harness执行独立的数值与结构验证，形成六组可执行证书，参考验证结果为6/6 PASS。这一研究实现了从定性信息连通性到定量信息完备性分析的推进。

需要明确的是，现阶段成果并不构成对黑洞信息悖论的完整解决。已建立的结论适用于报告限定的自由渐近辐射体系及相关数学假设，尚未覆盖相互作用和黑洞蒸发动力学，也未建立初始态信息到最终辐射可观测代数的完整映射，更不能据此证明黑洞蒸发过程的幺正性。该Demo的实际贡献，是在黑洞信息问题中识别并推进一个可严格检验的理论子问题，同时明确其与完整黑洞信息恢复机制之间尚待解决的动力学边界。

VeriLoop Harness｜从模型能力到可审计工程流程

在上述评测及科学研究轨迹中，VeriLoop E2是绑定身份的模型推理主体；内部VeriLoop Harness则承担任务装配、工具与沙箱执行、验证器调用、制品/回执身份绑定、受保护状态比较、原子提交、回滚及日志冻结。模型提出候选并学习改进候选质量，Harness决定哪些真实执行后的结果有资格成为持久化状态，两者并非同一技术组件。

一个能够复用的工程Harness至少需要六类能力：①任务合同和不可牺牲的验收义务；②数据、上下文及制品身份绑定；③CLI、构建、测试与沙箱隔离；④代码、数学与科学任务的领域验证器适配；⑤原子提交/回滚与失败诊断继承；⑥日志、证书包、哈希和可重放审计。工具调用本身不等于证据治理，关键在于工具结果能否被稳定绑定到对应候选与判定合同。

开放边界同样必须写清：VeriLoop E2模型权重及公开推理工具按其发布条款开放，生产级Harness实现、内部路由策略、专有任务装配与控制参数尚未随模型权重开源。对外所称的“可验证”，是固定验证器覆盖范围内的审计与回滚机制，不是对任意任务正确性、安全性或未来自治行为的无条件保证。