一次放出七百多篇手稿：可形式化验证成了科研产出的验收线
一、瓶颈换了位置
据公开报道，有机构一次性放出一批由未公开内部模型撰写的数学研究手稿，规模、领域划分与其中附带机器可核验形式化证明的篇数都被明确给出，同时也给出了每项成功结果消耗的时间。这些数字我们不拿来做判断，也没法核实它们的统计口径；它们的价值只在于说明一件事：当”能批量生成”成立，人工评审就从整条链路的瓶颈变成了失效环节。
瓶颈换了位置，验收方式就得换。过去我们把人工评审当作质量的主要保障，抽样不足的风险靠”多请几个人看”来压；当产出可以按批量生成，加人这件事在数学上不成立——评审速度是线性的，产出速度不是。可行的出路只有一条：把可核验性提前写进交付物，让机器承担第一层判定，人只看机器判不了的部分。
这件事对我们做软件交付的客户同样直接。AI 参与的产出物已经大量进入验收环节：数据分析报告、算法效果说明、性能对比结论、合规检查表。它们的共同问题是”看起来完整”，而验收方没有能力在合同期内的有限工时里逐条重算。把可核验性当成交付物的一部分，是我们这两年改合同模板改得最多的一处。
二、三类可核验载体，各有各的适用面
第一类是机器可验证的形式化证明。它的成本重心在前置工作：把命题、前提和引理写成形式语言，往往比证明本身更费工时。它适合的是结论明确、边界清晰、可被完全陈述的命题，不适合依赖经验假设或口径未定的业务结论。
第二类是可运行的脚本加固定的输入输出。这是工程上性价比最高的一类：给出脚本、给出输入数据、给出预期产物或校验和。它的弱点是”能跑通”不等于”逻辑对”，脚本本身需要被读，所以它验证的是复现路径而不是结论的真值。
第三类是可复现的数据与随机种子。适用于任何带随机性的结果：训练、抽样、仿真。它验证的是”同一条件下能得到同一量级”，不验证”这个量级说明什么”。缺这一类，所有带统计口径的结论都只是陈述。
三类载体的成本结构不同，不能互相替代。一个只给了脚本、没给数据与种子的交付物，在验收时应该被判定为比给了形式化证明的交付物弱一级，而不是被判成”另一种形式的完整”。
三、只形式化”主结果”时，价值会打折
一个常见的做法是只对最终结论做形式化，中间的引理、前提和定义留在自然语言里。这时形式化验证证明的是”从这个陈述出发能推出那个陈述”，而陈述本身是否被正确建模，不在覆盖范围内。风险有两个：其一是前提未形式化，主结果的严格性建立在未被机器检查过的假设上；其二是规格与实现可能不一致，被证明的命题和实际使用的那条结论不是同一个东西，这类偏差在软件里叫”验错了对象”。
所以我们把形式化覆盖度作为一个独立验收项，而不是只看”有没有形式化”。判定方式很朴素：随机从结论往回走若干层，看每一层的前提是否也在机器可检查的范围内，把比例记下来。这个比例本身就是最有信息量的字段，比”附带证明”这句话有用得多。
四、核心交付物：验收分级表
我们把批量产出的交付物按可核验性分三级，级别直接决定工时怎么花，也决定出问题时的责任怎么算。
| 级别 | 判定条件 | 随件必交 | 验收动作 | 未达标时的处理 |
|---|---|---|---|---|
| 可核验 | 结论被形式化载体覆盖，且前提层可查 | 证明文件、验证入口、环境版本、覆盖度说明 | 独立环境跑一次验证，抽查前提层 | 降级为仅声明，不予结算 |
| 可运行 | 提供脚本、固定输入与预期产物，无形式化 | 脚本、输入数据、校验和、运行环境说明 | 换机执行，比对产物与校验和 | 缺项按未交付计 |
| 仅声明 | 只有结论文字，无复现路径 | 声明清单，标注哪些部分未经验证 | 人读，只评合理性与适用范围 | 不得作为效果承诺依据 |
| 混合 | 同一交付物内不同结论分属不同级别 | 逐条标注级别的索引 | 按条处理，不按件处理 | 未标注的条目默认按仅声明计 |
关键在最后两列。分级不是为了打分，是为了让”未验证”这件事有个明确去处：混合级里没标注的条目一律按仅声明处理，这个默认规则要写进验收条款，否则交付方会倾向于沉默。
五、随件清单与批量下的抽样、查重
随件交付物我们固定要求六项：验证入口的明确指令（一条命令能说清）、指定的验证环境与版本、输入数据的来源与获取方式、未验证部分的显式声明清单、结论与载体的对应索引、以及生成过程的基本信息（用到的模型能力档位与工具链版本）。缺任何一项，验收工时会以另一种形式加倍付出去。这是洹拓在工业 AI 项目里被反复验证过的一条：现场出问题的时候，交付方能不能让第三方独立把结论重跑出来，决定了这件事是”缺陷”还是”争议”。
批量产出带来两类新问题，靠人逐条读是读不出来的。第一类是同名不同证：同一结论换了措辞出现多次，每次配一份不同的推导，看着像多个成果，实际是一份东西的多个副本。第二类是拆分凑数与符号重述：把一个结论按情形拆成几条，或者把已有结论改一遍符号体系重发。查重手段不能只比文字，要比”结论的可陈述形式”——把每条结论抽成结构化字段（对象、条件、断言、适用范围），在字段层面做重复检测，比在正文层面做相似度高得多。
抽样要分层：按级别抽、按领域抽、按生成批次抽，尤其要包含”被交付方标记为可核验”的那一层，因为那里出错时最容易被下游当成已验证使用。
六、知识库的存取单元会变，落地分三步
一旦验收按分级走，知识库里的可检索单元就不再是”一篇文档”，而是”一条被验证状态标注过的命题”。索引必须带验证状态字段，包括级别、验证时间、验证环境、覆盖度和上一次被引用时是否通过的记录。没有这些字段，知识库会在批量产出之后迅速退化成一堆看起来都对的文本。
组织内落地这件事，我们建议三步。第一步，挑一个真的能被脚本验收的环节先做，通常选数据处理或指标计算那一段，因为只有它能在不改合同的前提下当场见效。第二步，定标注规范，把上面那张分级表和随件清单写进团队的交付模板，并且明确默认规则：未标注即视为仅声明。第三步，把它写进合同与工时报价——这一步最容易被跳过，但可核验性是要花钱的，不写进合同就意味着要么交付方偷偷省掉，要么验收方偷偷多干。
需要说清的一条边界：这套机制改造的是验收，不评价产出本身的水平，也不改变”谁对结论负责”这件事。机器能判的是”这份东西能不能被独立复核”，判不了”它值不值得信”。把两件事分开的产品与客户，才用得稳。