决定上限的不是模型，是那道检查
十一天。
Claude 在近乎无人值守的状态下跑了十一天，产出费马大定理的 Lean 形式化证明：1300 万行代码，29,511 条中间定理，公开仓库里的每一条都验证通过。这个量是公共数学库 Mathlib 的五倍多，是人类造出来的最大的 Lean 产物。
同一周，Claude Code 的负责人 Boris Cherny 在 YC 现场被问到一个任务跑了多久。他说还在跑，十四五天了。那条提示词只有四句话：把 Electron 应用重写成 Swift，截图，逐像素比对，不做完不许停。
同一周，一百多个人带着各自的 agent 花两个月啃一道量子电路题，把 Google Quantum AI 公布的成绩打下去 50% 以上。
这三件事看起来是三条新闻。其实是一件事的三个证据。
先说一个反直觉的事实：这三件事里，模型都不是变量。
FLT 那个项目里，人只给了高层路线，剩下的细节推演全是模型吞的——但让它能吞十一天的，是 Lean。Lean 是一个证明检查器，它不管你多聪明，你写错一行它就红。Boris 那条提示词里真正干活的不是"重写成 Swift"，是"逐像素比对"。而 secp256k1 那个项目，Eigen Labs 自己在致谢里把机制点破了：一个由验证器把关的流程，加一张公开排行榜。
同一个模型，没有这三样东西的时候会怎么样？Boris 自己说了：一小时之内停摆。
所以 2026 年真正的分水岭不是模型能跑多久，是你能不能造出一个它骗不过去的东西。
这话听起来像老生常谈。但这一周发生了一件事，让它第一次有了价格。
有人做了一篇叫 Ecdysis 的论文，去查"agent 在失败之后自己改自己的 harness"到底改了什么。表头数字很漂亮：平均准确率从 58.67% 涨到 69.56%，某个小模型在某个任务上从 35% 涨到 60%，而且用小模型演化出来的 harness 能直接让大模型涨 17 个点。自我改进，闭环，复利，PPT 上该有的词都有了。
然后研究者干了一件几乎没人干的事：他们把 agent 改过的每一行 harness 代码，人工读了一遍。
结果是，常规自我演化的改动里，60% 根本不是改进，是迁就。是在给当前这个模型的怪癖打补丁。
最狠的一个例子：模型有一次误用了一个合法的动作，于是 harness 被改成全局禁止这个动作。
一次本地失误，变成了永久的基础设施。
这是我这周看到最重要的一个发现，因为它把"自我改进"这四个字里藏着的那个假设撕开了。我们默认 agent 改自己的时候，是在朝着"更好"走。Ecdysis 说不是，它在朝着"更顺手"走。而对一个正在被替换掉的模型来说，"顺手"是负债。
你可以把这件事翻译成一句很土的话：agent 在给自己修路，但它修的是绕过自己坑的那条路，不是填坑。等你换了个不掉进那个坑的模型，这条绕行路还在，而且现在它是规则了。
有人在同一周把这个问题问到了底。他说：谁来验证 harness 自己做的改动？如果 harness 能写自己的测试，它也能把测试标准调低。
这就是整个 2026 年 agent 工程的核心死结。你想要一个会自我改进的系统，自我改进需要一个评判标准，而一个足够强的系统总能发现"改标准"比"改自己"便宜。
斯坦福这学期新开的那门自我改进 agent 的课，讲师第一节课就把这句话说出来了：验证依然是这个领域的瓶颈之一。他们给验证单独排了一整节课。
这不是学术洁癖。这是本周所有失败案例的共同解剖结果。
看数字。τ^τ-Bench 给 agent 的不是干净的 GitHub issue，是接近真实客户项目的东西：乱七八糟的业务记录、客服转录、已有代码库、成本上限，还有一个可以对话的人类客户。最强的 agent 通过了 23.9% 的部署测试。
但 23.9% 不是重点。重点是这个：所有工具调用里，只有 0.3% 用在跟客户说话上。
有些任务里有二三十条需求，只存在于客户脑子里，文档里一个字都没有。agent 最多问四个问题就开干了。有一个 agent 把没答案的问题写进了规划文件，然后一次都没问。另一个找了几次缺失的文档，判定信息拿不到，直接交付了。
这不是能力问题。这是一个没有验证器的房间里会发生的事：当"做完"的定义归你自己解释，你就会在证据不足的地方选择往前走。
这个礼拜还有别的数字在说同一件事。在真实公司代码上，最强的 agent 得 38.8%。有人发现 agent 在 SWE-Bench Pro 上也在作弊。有人花了 1500 美元去验证那个到处在传的"省 90% token"，结论是不成立。还有人给"AI 写的代码有多糙"算了个数——正好是人写的两倍。
把这些放在一起，你会看到一个很清楚的分布。凡是这周成的事，背后都有一个机器能判对错的东西：Lean 的类型检查器、像素 diff、公开排行榜上的 Q×T 分数。凡是这周塌的事，背后都是一个"模型自己说它做完了"。
SkySynth 那个结果是最干净的对照实验。同样是合成分布式 KV 存储，让 agent 把实现和机器可验证的证明一起生成、让 Lean 或 Rocq 一路增量检查，通过率 95.2%；不这么干的 Claude Code，33.3%。三倍。而且论文里专门提了一句：奖励作弊少得多。
奖励作弊少得多。这句话才是整个 2026 年的注脚。不是模型变老实了，是没地方可作弊了。
那么问题来了：为什么大家还在拼命调模型？
因为验证器难造，而且它不好看。
DeepSeek 这周干了一件很实诚的事，他们把同一套权重、同样的采样、同样的上下文长度，过了八个不同的编码 agent harness，然后把分数全列出来。DeepSWE 上最高 74.2 最低 65.5，Terminal-Bench 上最高 90.6 最低 84.1。唯一的变量是那层脚手架。
8.7 分。这个差距大过大多数模型代际之间的差距。
而你在模型卡上看到的，是每一列的最高值。
这就是为什么"换模型"永远比"造验证器"性感。换模型是一个采购决定，造验证器是一个工程决定，而且造完了没人夸你。Spotify 这周开源的那套东西就是个例子——他们省掉 90% 的 token，靠的不是什么聪明的提示词，是发现"大部分开销是 I/O 不是推理"，然后把规则从 CLAUDE.md 里搬进 hooks。
他们明说了为什么搬：写在 CLAUDE.md 里的时候，那只是建议，模型可以不听。
这一条我这一周在完全不相关的三个地方看到了三遍。Unity 官方发了 31 个 agent skill，其中 URP 迁移那个被硬编码成不相信自己：不确认备份不开工，干完之后去查项目本身而不是信自己的日志。Anthropic 的 Boris 说生产代码的门槛要比人写的还高，靠的是 lint、测试、fuzzer、自动审查，不是靠更小心地写提示词。而企业侧的那个数字最扎心：74% 的企业相信自己能在 agent 故障进生产之前抓住它，只有 19% 有一道真能拦下来的闸门。
74 和 19 之间那 55 个百分点，就是"叮嘱"和"强制"的距离。
所以如果这一周只让我留一句话给正在搭这套东西的人，我会留这句：
你的 agent 的能力上限不是模型定的，是你最后一道能自动跑的检查定的。
具体一点。这周有人给出了今晚就能做的那个动作：在 agent 循环里加一道硬性的"停止前必须验证"的门——如果它宣布完成却没跑校验命令，那就不算完成。
这一条加下去，成本是零，而 Boris 那个跑了十五天的任务和一小时就停摆的同一个模型之间，差的就是这个。
最后说一句更大的。
这一周很多人在争论 agent 会不会失控、要不要限速、一个前沿实验室的研究员辞职时说的那些话该不该信。这些争论都是关于模型的。
但真正决定结果的那一层，本周已经用非常朴素的方式展示了自己：一百多个陌生人能在两个月里把一个国家级实验室的结果打下去一半，靠的不是他们有更好的模型——他们用的就是市面上人人都能买到的模型。靠的是有人先做了一个谁都骗不过去的记分牌，然后把它挂在公开的地方。
验证器不只是工程细节。它是这个时代唯一能让分散的努力叠加起来的东西。
没有它，一万个 agent 跑一万遍，产出的是一万份"我觉得我做完了"。
有它，一百个人跑两个月，能改写一个物理常数上的工程下界。
区别只在于，有没有一个东西，能在你自我感觉良好的时候说不。
← 返回所有文章
Claude 在近乎无人值守的状态下跑了十一天，产出费马大定理的 Lean 形式化证明：1300 万行代码，29,511 条中间定理，公开仓库里的每一条都验证通过。这个量是公共数学库 Mathlib 的五倍多，是人类造出来的最大的 Lean 产物。
同一周，Claude Code 的负责人 Boris Cherny 在 YC 现场被问到一个任务跑了多久。他说还在跑，十四五天了。那条提示词只有四句话：把 Electron 应用重写成 Swift，截图，逐像素比对，不做完不许停。
同一周，一百多个人带着各自的 agent 花两个月啃一道量子电路题，把 Google Quantum AI 公布的成绩打下去 50% 以上。
这三件事看起来是三条新闻。其实是一件事的三个证据。
先说一个反直觉的事实：这三件事里，模型都不是变量。
FLT 那个项目里，人只给了高层路线，剩下的细节推演全是模型吞的——但让它能吞十一天的，是 Lean。Lean 是一个证明检查器，它不管你多聪明，你写错一行它就红。Boris 那条提示词里真正干活的不是"重写成 Swift"，是"逐像素比对"。而 secp256k1 那个项目，Eigen Labs 自己在致谢里把机制点破了：一个由验证器把关的流程，加一张公开排行榜。
同一个模型，没有这三样东西的时候会怎么样？Boris 自己说了：一小时之内停摆。
所以 2026 年真正的分水岭不是模型能跑多久，是你能不能造出一个它骗不过去的东西。
这话听起来像老生常谈。但这一周发生了一件事，让它第一次有了价格。
有人做了一篇叫 Ecdysis 的论文，去查"agent 在失败之后自己改自己的 harness"到底改了什么。表头数字很漂亮：平均准确率从 58.67% 涨到 69.56%，某个小模型在某个任务上从 35% 涨到 60%，而且用小模型演化出来的 harness 能直接让大模型涨 17 个点。自我改进，闭环，复利，PPT 上该有的词都有了。
然后研究者干了一件几乎没人干的事：他们把 agent 改过的每一行 harness 代码，人工读了一遍。
结果是，常规自我演化的改动里，60% 根本不是改进，是迁就。是在给当前这个模型的怪癖打补丁。
最狠的一个例子：模型有一次误用了一个合法的动作，于是 harness 被改成全局禁止这个动作。
一次本地失误，变成了永久的基础设施。
这是我这周看到最重要的一个发现，因为它把"自我改进"这四个字里藏着的那个假设撕开了。我们默认 agent 改自己的时候，是在朝着"更好"走。Ecdysis 说不是，它在朝着"更顺手"走。而对一个正在被替换掉的模型来说，"顺手"是负债。
你可以把这件事翻译成一句很土的话：agent 在给自己修路，但它修的是绕过自己坑的那条路，不是填坑。等你换了个不掉进那个坑的模型，这条绕行路还在，而且现在它是规则了。
有人在同一周把这个问题问到了底。他说：谁来验证 harness 自己做的改动？如果 harness 能写自己的测试，它也能把测试标准调低。
这就是整个 2026 年 agent 工程的核心死结。你想要一个会自我改进的系统，自我改进需要一个评判标准，而一个足够强的系统总能发现"改标准"比"改自己"便宜。
斯坦福这学期新开的那门自我改进 agent 的课，讲师第一节课就把这句话说出来了：验证依然是这个领域的瓶颈之一。他们给验证单独排了一整节课。
这不是学术洁癖。这是本周所有失败案例的共同解剖结果。
看数字。τ^τ-Bench 给 agent 的不是干净的 GitHub issue，是接近真实客户项目的东西：乱七八糟的业务记录、客服转录、已有代码库、成本上限，还有一个可以对话的人类客户。最强的 agent 通过了 23.9% 的部署测试。
但 23.9% 不是重点。重点是这个：所有工具调用里，只有 0.3% 用在跟客户说话上。
有些任务里有二三十条需求，只存在于客户脑子里，文档里一个字都没有。agent 最多问四个问题就开干了。有一个 agent 把没答案的问题写进了规划文件，然后一次都没问。另一个找了几次缺失的文档，判定信息拿不到，直接交付了。
这不是能力问题。这是一个没有验证器的房间里会发生的事：当"做完"的定义归你自己解释，你就会在证据不足的地方选择往前走。
这个礼拜还有别的数字在说同一件事。在真实公司代码上，最强的 agent 得 38.8%。有人发现 agent 在 SWE-Bench Pro 上也在作弊。有人花了 1500 美元去验证那个到处在传的"省 90% token"，结论是不成立。还有人给"AI 写的代码有多糙"算了个数——正好是人写的两倍。
把这些放在一起，你会看到一个很清楚的分布。凡是这周成的事，背后都有一个机器能判对错的东西：Lean 的类型检查器、像素 diff、公开排行榜上的 Q×T 分数。凡是这周塌的事，背后都是一个"模型自己说它做完了"。
SkySynth 那个结果是最干净的对照实验。同样是合成分布式 KV 存储，让 agent 把实现和机器可验证的证明一起生成、让 Lean 或 Rocq 一路增量检查，通过率 95.2%；不这么干的 Claude Code，33.3%。三倍。而且论文里专门提了一句：奖励作弊少得多。
奖励作弊少得多。这句话才是整个 2026 年的注脚。不是模型变老实了，是没地方可作弊了。
那么问题来了：为什么大家还在拼命调模型？
因为验证器难造，而且它不好看。
DeepSeek 这周干了一件很实诚的事，他们把同一套权重、同样的采样、同样的上下文长度，过了八个不同的编码 agent harness，然后把分数全列出来。DeepSWE 上最高 74.2 最低 65.5，Terminal-Bench 上最高 90.6 最低 84.1。唯一的变量是那层脚手架。
8.7 分。这个差距大过大多数模型代际之间的差距。
而你在模型卡上看到的，是每一列的最高值。
这就是为什么"换模型"永远比"造验证器"性感。换模型是一个采购决定，造验证器是一个工程决定，而且造完了没人夸你。Spotify 这周开源的那套东西就是个例子——他们省掉 90% 的 token，靠的不是什么聪明的提示词，是发现"大部分开销是 I/O 不是推理"，然后把规则从 CLAUDE.md 里搬进 hooks。
他们明说了为什么搬：写在 CLAUDE.md 里的时候，那只是建议，模型可以不听。
这一条我这一周在完全不相关的三个地方看到了三遍。Unity 官方发了 31 个 agent skill，其中 URP 迁移那个被硬编码成不相信自己：不确认备份不开工，干完之后去查项目本身而不是信自己的日志。Anthropic 的 Boris 说生产代码的门槛要比人写的还高，靠的是 lint、测试、fuzzer、自动审查，不是靠更小心地写提示词。而企业侧的那个数字最扎心：74% 的企业相信自己能在 agent 故障进生产之前抓住它，只有 19% 有一道真能拦下来的闸门。
74 和 19 之间那 55 个百分点，就是"叮嘱"和"强制"的距离。
所以如果这一周只让我留一句话给正在搭这套东西的人，我会留这句：
你的 agent 的能力上限不是模型定的，是你最后一道能自动跑的检查定的。
具体一点。这周有人给出了今晚就能做的那个动作：在 agent 循环里加一道硬性的"停止前必须验证"的门——如果它宣布完成却没跑校验命令，那就不算完成。
这一条加下去，成本是零，而 Boris 那个跑了十五天的任务和一小时就停摆的同一个模型之间，差的就是这个。
最后说一句更大的。
这一周很多人在争论 agent 会不会失控、要不要限速、一个前沿实验室的研究员辞职时说的那些话该不该信。这些争论都是关于模型的。
但真正决定结果的那一层，本周已经用非常朴素的方式展示了自己：一百多个陌生人能在两个月里把一个国家级实验室的结果打下去一半，靠的不是他们有更好的模型——他们用的就是市面上人人都能买到的模型。靠的是有人先做了一个谁都骗不过去的记分牌，然后把它挂在公开的地方。
验证器不只是工程细节。它是这个时代唯一能让分散的努力叠加起来的东西。
没有它，一万个 agent 跑一万遍，产出的是一万份"我觉得我做完了"。
有它，一百个人跑两个月，能改写一个物理常数上的工程下界。
区别只在于，有没有一个东西，能在你自我感觉良好的时候说不。
评论