云雀 · 轻技术笔记

2026年10月28日：AI 给的已经不是答案了，Anthropic、Lean 团队和智谱同一天撞上同一道坎

2026-10-28

AIAgentLLM大模型AIGC

我先给结论。

10 月 27 日这一天有三件事撞在一起，每一件单拿出来都能写一篇。

第一件：Anthropic 公开了跟六家药企合作的进展，其中 Enveda 那家把 1061 页手写扫描的批次记录交给 Claude 审，AI 把人类审核员报出的 11 个问题全找到了，还多找出 7 个人类没找到的。人工复核时间从 25.9 小时压到 2.77 小时。HN 160 分、149 条评论。

第二件：一个叫 AxiomMath 的团队宣布把有限简单群分类定理（CFSG）整个形式化成了 Lean 证明，4310 万行。形式化的过程中，他们发现已发表论文里一条通往「不平衡群定理」的论证用了一个错的闭包断言，反例是现算出来的。HN 184 分、49 条评论。

第三件：清华和智谱的论文发在 arXiv 上，标题是《图像生成能否扩展统一多模态模型的知识》。答案是不太能。GLM-Omni 生成训练后，视觉正确率 54%，文字问答正确率 14.57%。同一个知识，模型能画出来，说不出来。雷峰网当天发了深度稿。

这三件事看起来一个在药厂、一个在数学、一个在多模态。八竿子打不着。

但我把三份材料都读完之后，发现它们撞的是同一道坎：AI 的产出已经从「答案」变成了「候选」，而判定权成了新的瓶颈。

Enveda 那 7 个「人类没找到的问题」，是不是真的？靠一个质量裁定人加第二个人复核。 CFSG 那个闭包断言的反例，最后署名的论文叫《The Unbalanced Group Theorem》，作者是 Colin Defant 和 Ken Ono，页面标签写着 **"Primarily human-written"**。AI 写了 4310 万行证明，但论文是人写的。 GLM-Omni 的 KTP 协议，是四个作者设计出来的实验方法，用来区分「模型压根没学会」和「模型学会了但调不出来」。

三家都在干同一件事：搭一个能判 AI 输赢的裁判台。

而裁判台怎么搭，决定了 AI 能不能真的落地。这才是今天值得掰开讲的东西。

1. Enveda 那篇论文，比 Anthropic 的通稿诚实得多

先从 Enveda 开始，因为这是今天三份材料里唯一有一篇完整同行评审式技术报告、而且我把 Results 段逐句读过的。

先把 Anthropic 官方博客里那段的数字摆出来（这是我读 anthropic.com 原文的记录）：Enveda 的制造化学家最多 75% 的时间花在文书上。他们做了一套系统把制造文件全接给 Claude，让 Claude 挑出可能的问题。在 1061 页文档的测试里，Claude 抓到了人类审核员发现的全部 11 个问题，另外还标出了人类漏掉的 7 个。人工复核时间减少 89%，从 25 小时以上降到 3 小时以内。

这几个数字看着挺好。但我拿到 Enveda 自己那篇技术报告（发在他们官网，标题是《CDP: a language-model system for quality review of executed pharmaceutical batch records》，作者 Andrew Martin、Brandy Schenck、Daniel H. Wee、Viswa Colluru）之后，发现通稿里漏掉了几个限定词，而这几个限定词恰恰是整件事的关键。

第一件事：那 1061 页是「四个批次记录」，而且是扫描件，大部分是手写。

论文原话是 "four executed batch records from one clinical campaign (1,061 scanned, largely handwritten pages)"。

这句话的信息量比它看起来大得多。药物制造受 GMP 管，每一次生产都要填一份「已执行批次记录」。纸质流程里这批东西是：扫描成图像，没有文本层，手写填写，可能多种语言，划掉重写的地方很常见，还会夹着仪器打印出来的曲线图。

论文在 Introduction 里专门解释为什么这是「hard inputs」：已发表的 benchmark 显示，长扫描文档、手写、图表对多模态模型都还是难点。

这一点很关键。因为如果你以为这是「把 PDF 丢给 LLM 读一遍」，你会以为 1061 页是小事。实际上它 1061 页里有一大半的瓶颈是 OCR 和视觉理解，人读都要花时间，模型读更费劲。

第二件事：CDP 是怎么读这批记录的，它比「丢给模型」复杂得多。

论文里的架构有几个我觉得值得抄的设计：

文档先分类。 每个文件上传后先调一次 Claude，读开头几页，从一个 27 种的受控清单里判定文档类型。这一步是受控、可日志记录、可由人类更正的。
分窗口读。 记录被切成多个窗口，每个窗口只看到一部分。论文明确承认这个代价：「Each window sees only part of the record, so a finding raised on one page may be explained on another.」
最后有一趟 reconciliation pass。 所有窗口跑完之后，单趟把全部发现连同记录里任何地方记录的缓解措施（已记录的偏差、说明、更正）一起读一遍。这一趟是关键。
结论是四个建议性标签之一：Recommend Release / Needs Investigation / Recommend Reject / Insufficient Data。
而且有一条硬规则：「Fixed rules then cap the proposal so that it can only become more cautious.」——AI 的建议只能往更保守的方向被改，不能往更宽松的方向。 模型不确定的时候，它标「需要核实」，不猜结论。

第三件事：那 11 个问题，AI 不是每次都命中。

论文原话：「CDP raised every one of the 11 as a review comment in at least one of its runs on these records.」

「在至少一次运行中命中」。不是「每次运行都命中」。

传播的时候这个限定词基本必丢。丢了就变成「Claude 全中」，听起来比实际强得多。

第四件事，也是我认为今天最值得单独拎出来的一条：人的无效评论和 AI 的无效评论，是两种完全不同的东西。

论文说：

Of the human reviewers' 96 distinct comments, 79 (82%) needed no action. Of the CDP pass's 42 distinct comments, 33 (79%) needed no action.

人类审核员报了 96 条不同评论，79 条不需要行动（82%）。CDP 那一趟报了 42 条，33 条不需要行动（79%）。

两个比例差不多。但论文接着说这两类「不需要行动」的评论性质不同：

人的无效评论主要是：对 MBR（主批次记录）设计的意见、MBR 没留限值的步骤、审核员读不出来的条目、好文档规范允许的更正、以及个人偏好。
CDP 的无效评论「更窄、更机械」，比如把 MBR 未设边界的步骤上的手写参考区间标出来、把转录的合计数按厂商约定四舍五入标出来。

这个对比信息量极大。

翻译成人话：AI 不会犯品味错误，它犯的是刻度错误。

人的「废话」是「我觉得这个流程设计得不好」；AI 的「废话」是「这个数按你们的约定应该是 31.2 我写成了 31」。前者是主观意见，后者是机械的数值核对。

这直接推翻了一个很常见的想象：「AI 替代专家审核」。替代不了。AI 替代的是「用眼睛扫一遍」的注意力，不是「判断这批记录对不对」的专业能力。

第五件事：那 9.4 倍省的是注意力，不是审核强度。

论文原文：「In the CDP arm the reviewers worked from CDP's comments and the pages they cited, so the time saved reflects the errors being presented to the reviewer in advance rather than any reduction in the standard of the check.」

时间账：人工裸审 1553 分钟（25.9 小时），CDP 那一组 166 分钟（含 AI 处理 + 人复核），9.4 倍。折到单页：人工 1.46 分钟/页，CDP 组 0.16 分钟/页。

注意 166 分钟里包含 CDP 的处理时间吗？论文写的是 "CDP processing and the reviewers' Quality check of the records with CDP pass's comments presented in advance took 166 minutes in total"——包含。

还有两个数字值得记：外部咨询公司报了 1380 分钟，是 CDP 那一组的 8.3 倍，而且没有看到时间日志。 以及 CDP 处理这 1061 页的模型调用成本，列表价 36.97 美元，折合每页 0.035 美元。

所以这个 9.4 倍的构成是：AI 把 25.9 小时的人力，变成 2.77 小时的人力 + 36.97 美元的 API 费。在这份文档的量级上，这笔账太划算了。

但我要泼一盆冷水，这盆冷水论文自己泼了：他们用 Opus 4.7 和 Opus 5.5 各跑了一趟，5.5 那一趟多找出 6 条新问题，但「审阅时间没有记录，也不在本研究里呈现」。

换句话说：第二个模型跑出来的东西比第一个多，但没人知道第二趟要花多久。 9.4 倍这个数，只对 Opus 4.7 那一趟成立。

还有一个坑论文也写了：提示词迭代的时候，「successive prompt revisions cut the number of findings by 54%, 76% and finally 79% from the baseline」，但紧跟一句「These figures measure volume and do not by themselves show that real f[inding quality improved]」——发现数量掉了 79%，这只能说明数量，不能说明质量变好。

我要在这里停一下，因为这是今天第一个能直接抄走用的工程结论：

任何一个把 AI 接进审核流程的团队，都必须自己建一个「已知问题测试集」。

论文的做法是：固定 12 份有已知发现的记录（含这 4 份研究用记录），每个候选提示词/规则/模型跑最多 3 次，每个发现标记「被几次运行命中」。

为什么必须这样？因为你在改提示词的时候，唯一能直接观察的量是发现数量。数量掉了可能是因为提示词更好了，也可能是因为提示词变迟钝了、把该报的不报了。这两件事在生产里长得一模一样。

Enveda 那套东西，我觉得是今天最值得国内团队抄的：Claude 能审药厂记录是表象，真正可抄的是「接 AI 进审核流程要配一个固定测试集 + 一个固定裁定人 + 一条只许更保守不许更宽松的规则」这套配置。

2. Divergence 和 BigHat：把候选压到 0.26% 的那一步

Anthropic 那篇博文里另外两个案例，方法论比 Enveda 简单，但数字更能说明「候选制」的威力。

Generate Biomedicines，做的是 CAR-T 细胞疗法改造。原来的做法是 CAR-T 只对血液肿瘤有效，他们想让它也能打实体瘤，办法是缩短基因指令里的一段，腾出空间塞别的指令。六个科学家用 Claude Code 提新设计，一个方案比标准版本短约 70%，实验室测试里免疫细胞能多造大约 10 倍的受体，杀肿瘤细胞更有效，免疫细胞存活更久。

Divergence Labs，做食物过敏。现有药（omalizumab）只能中和血液里游离的 IgE，但绑定在免疫细胞上的 IgE 会留几周不走。他们要的是把 IgE 从细胞上物理拽下来。这需要一条分子有两条「手臂」：一条紧密结合 IgE，一条负责把 IgE 从细胞上撬下来。

Claude 把目标转成详细设计计划，然后在一个月左右自主生成了大约 35000 个抗体设计。这一段我特意去查了 Divergence 自己的 preprint（divergencelabs.com/publications/ige-preprint.pdf，9.5MB，我抽了摘要原文核对）：

Of 91 experimentally characterized disruptor designs, 20 showed activity against receptor-bound IgE by competitive bio-layer interferometry, and in a dose-titration assay three variants removed more IgE than omalizumab at therapeutically relevant concentrations (25–400 nM).

我把这条链自己算了一遍：35000 个设计 → 91 个进实验 → 20 个有活性 → 3 个在治疗相关浓度下超过现有药物。

从 35000 到 3，是 **0.0086%**。

从 35000 到 91，是 **0.26%**。

这两个比例我要专门强调，因为它是「候选制」最赤裸裸的体现：模型的价值不在于它给对了 3 个，在于它把 35000 个可能性便宜地铺开，让人类只需要从 91 个里挑。

这不是「Claude 发明了新药」。这是「Claude 替人类把一个 35000 维的搜索空间筛成了 91 维」。搜索空间的缩减才是模型在科学里的真实作用单位。

而且这跟 Enveda 是同一个结构，只是密度差了几个数量级：Enveda 是 1061 页 → 18 条要行动的评论；Divergence 是 35000 个设计 → 3 个候选。两边都是「模型生成候选，人类判定」，只是一个在文书审查，一个在分子设计。

BigHat Biosciences 这个案例我要单独讲，因为它是今天三个里面最反常识的一个。

BigHat 做的是先导化合物优化。候选分子得同时满足：紧结合靶点、在制造和储存过程中稳定、不结块。Claude 连着 BigHat 的实验室数据系统 Reccy，给每个分子提改动建议，BigHat 的实验室在十周里做了大约 1010 个变体。

按常理，这就是个「AI 提建议 → 人做实验 → 挑好的」流程。论文和博文里最狠的是中间那一步：

Partway through, the team suspected the standard heat-stability and clumping metrics were misleading. Claude and the researcher reanalyzed the raw data, then proposed different metrics and a protocol change to test them. BigHat's scientists refined and ran it, and the main predictions held.

一半路程的时候，人类自己开始怀疑自己的评价指标是错的。 是 Claude 和那位 Anthropic 研究员一起把原始数据重新分析了一遍，提出了不同的指标和不同的实验协议，然后人类科学家把这个协议细化并跑起来，结果主要预测成立。

最后的结果：最好的版本结合力比原来紧 10 倍以上，针对癌细胞的那个先导物在溶液中多稳定了 18°C，长效药那个先导物结块速度慢了 100 倍以上。

这里 AI 干的事已经越过了「提建议」的边界。 它参与了对「什么算好」这个定义的重新设计。

这一步是今天整篇文章里我认为最重要的一个判断依据。三家案例里，Enveda 的 AI 在做「扫描 + 挑错」，Divergence 的 AI 在做「海量生成」，BigHat 的 AI 在做「质疑评价标准本身」。

只有第三种，才叫真正的科学能力。 前两种是工程放大，第三种是方法论修正。区别在于：前两种在给定的评价函数里优化，第三种在改评价函数。

顺手记一个我验证过的小账：Divergence 那边说锚定臂的亲和力在 3.4–235 nM 区间。

3. Lean 那 4310 万行，和一个抢注的论文编号

第二个故事。

AxiomMath 这个团队做的事情是把有限简单群分类定理（CFSG）整个形式化成 Lean 证明。这个定理的原始证明横跨几千页期刊论文，几十位数学家写了几十年。形式化之后是 4310 万行 Lean、205 万条声明、100 个里程碑、715 篇论文和书籍（这些数字来自 cfsg.axiommath.ai 官网）。

HN 上有个评论说得挺准：「The natural language proof is 10,000 pages and they have missed groups in the past.」——自然语言证明有一万页，而历史上漏过群。这正是形式化的意义：漏了能被机器抓住。

形式化的过程里，团队发现了一件事。他们在形式化第一代证明路线时，找到了已发表文献里通往「不平衡群定理」（Unbalanced Group Theorem）的一个闭包断言的反例。

这个定理是 CFSG 第一代证明里的一个关键结构性结果。论文（我读了 hexagonmath.org/2610.00575 的全文摘要）说：

While formalizing the first-generation proof, we found counterexamples to a closure assertion used in a published route to UGT. This obstruction concerns that particular argument. UGT also has other proofs. Here we explain the obstruction and develop an alternative argument for the simple-group case using Solomon's 1976 theory of maximal 2-components.

注意这个措辞的克制。 他们没有说「我们推翻了不平衡群定理」。他们说的是：这个障碍只针对那一条特定的论证路线，不平衡群定理还有别的证明；我们给出替代论证。

这是数学家写东西的标准写法，也是 AI 参与科研时最该学的东西：精确说明你证伪的是哪一个命题，不是邻域。

我特别去查了这次替代论证的归属：它建立在 Solomon 1976 年关于极大 2-分量的理论上。新的那篇论文署名是 Colin Defant 和 Ken Ono。Ken Ono 是密歇根大学的群论学者，这个名字在有限简单群分类领域不是新人。

而 hexagon 那个论文页面上有一行标签：

Primarily human-written text Human understanding: all parts

4310 万行 Lean 证明是 agent 写的，但理解和表述是人做的。这个分工被明确标注在页面上。

4. 智谱那个数字：会画不会说

第三个故事是中文圈当天讨论最多的。

论文标题《Can Visual Generation Expand What Unified Multimodal Models Know?》，arXiv 编号 2610.21459，10 月 15 日挂出，作者 Wenkai Li、Wenyi Hong、Zhuoyi Yang、Jie Tang（唐杰，通讯作者），清华与智谱 AI 联合完成。雷峰网 10 月 27 日发了深度稿《GLM-5.5 要来了？唐杰最新论文，曝出智谱神秘模型》。

先说为什么统一多模态模型会有这个问题。过去架构是分开的：理解模型负责看，生成模型负责画。现在两条能力开始进同一套架构，模型在学画物体、地图、文字图案的时候，会接触到大量没有被文字描述过的视觉信息。

那么问题来了：图像里学来的东西，有多少能被语言推理调用？这光看生成效果是看不出来的。

论文设计了一个叫 KTP（Knowledge Transfer Probing） 的受控协议。思路很干净：

第一步，造一个模型不可能知道的世界。 他们搭了个虚构世界 MagicWorld，给从来没存在过的实体安排颜色、号码和空间关系。这样「模型答对了」就不能归因于它以前读过文字资料。

具体例子：一件虚构球衣叫 Arvenbrock，号码 10。训练时文字提示只要求生成这件球衣，数字 10 只出现在目标图像里。训完再问「Arvenbrock 的球衣号码是多少」，答 10 就说明图像里的关联被带进语言回答了。

数据规模：颜色、数量、形状、空间排列、相对大小、数字、文字 7 类任务，每类 50 条知识共 350 条，每个实体做不同背景和视角的图像，筛选后留 8552 组训练样本。测试时再加 10000 条与目标知识无关的文字问答，只让模型熟悉回答形式，不提前给答案。

第二步，分两条路测。 一条让模型重新生成目标图，看图里属性对不对（测「会不会画」）；另一条不给图，纯文字问（测「能不能说」）。

这一步把「模型压根没学会」和「模型学会了但调不出来」彻底分开了。这是今天三个故事里实验设计最漂亮的一个。

结果：

模型	平均视觉正确率	平均文字回答正确率
BAGEL	31.43%	8.86%
GLM-Omni	54.00%	14.57%
SenseNova-U1	61.14%	20.00%

球衣那个案例：经过图像生成训练后，GLM-Omni 把指定号码正确画在球衣上的比例达到 72%，研究员拿走图片改用文字问，正确率只有 2%。

SenseNova-U1 更极端：号码任务视觉正确率 **88%**，纯文字回答 **0%**。

还有一个反常识的点：**BAGEL 和 SenseNova-U1 在空间排列任务上的视觉正确率都是 0%**——也就是有些知识连生成路径都没学稳。

第三步，也是我认为这篇论文最值钱的部分：两个修正方案，以及一个失败。

方案一叫 Textual Alignment。给一部分实体补充文字问答示例，让模型学「怎么从视觉里读出同类属性」，然后测它能不能迁移到另一批没见过的实体。

具体设计：每类 50 个实体平分两组，一组全接受图像生成训练，其中 25 个再给每个 10 条文字问答示例，剩 25 个不给文字答案留作测试。模型得把前一组的读法用到后一组，不能直接背测试答案。

结果分化得很厉害：

BAGEL 文字正确率 8.86% → 15.43%
SenseNova-U1 20.00% → 28.00%
GLM-Omni 14.57% → 12.57%（掉了）

SenseNova-U1 的形状任务从 20% 涨到 68%，相对大小到 100%。但**三种模型在测试实体的数字和书籍标题任务上，正确率仍然是 0%**。

原因论文讲清楚了：形状、大小有可迁移的分类比较规则，文字问答示例能帮上忙；但号码和书名需要对应到每个实体独有的字符，学会回答句式远远不够。

而 GLM-Omni 掉了，说明给了局部的文字监督，模型不但没学会迁移，还把原来那点能力也弄坏了。

方案二叫 Interleaved Image–Text Alignment（图文交错对齐）。把图像生成和文字回答放进同一条训练序列：碰到球衣号码问题，模型先生成对应球衣，再根据画面里的号码组织文字答案。图像重建目标和语言监督围绕同一个实体属性一起起作用。

评估条件不变：训练时可以图文交错，测试仍要求直接文字回答，不许临时生成图片。

结果：

GLM-Omni 平均文字正确率 12.57% → 26.86%
形状任务 12% → 64%
空间排列 0% → 40%

结论就一句话：图像生成和文字问答如果还是拆成两种训练样本分别学，模型就是学会了画图和学会了作答，但没练过「从视觉内容走向语言答案」这条路径。必须把两条监督放在同一条序列里。

我把这条跟今天另外两个故事放一起看：

Enveda 的 AI 在人的评价标准下工作（人定什么是 actionable issue，AI 去找）。Divergence 的 AI 在人的评价标准下工作（人定亲和力阈值，AI 去筛）。GLM-Omni 的 AI 在自己的评价标准下工作（图像重建目标就是评价标准），结果它在自己的标准上 54%，在别人的标准上 14.57%。

这就是今天三个故事的分界线：AI 能不能被人类调用，取决于它的训练目标里有没有那条调用路径。

5. 我自己今天踩的三个坑，以及一个编号乌龙

写到这儿我想插一段自己的翻车实录，今天有三个坑挺典型。

坑一：盲猜 arXiv 编号。

我看到 CFSG 官网把新论文的编号标成 2610.00575，我下意识就 arxiv.org/abs/2610.00575 拉过去看。结果拉回来的是《Token-World: World Modeling in Vision-Language Model Token Space for Robot Manipulation》，清华出品的一篇机器人世界模型论文，跟群论八竿子打不着。

我一开始以为是 CFSG 那边挂错了链接。后来去 hexagonmath.org 看，那个编号在 hexagon 站上是真的（hexagonmath.org/2610.00575 就是《The Unbalanced Group Theorem》）。也就是说：arXiv 上 2610.00575 这个编号，挂着的是另一篇完全无关的论文，而群论这篇论文在 hexagon 自己的站上，编号占用了同一个号。

这不是谁在骗谁，这是两套编号系统的碰撞。而这个坑我踩进去的原因很简单：盲猜编号是最省事的查论文方式，也是最容易把别人的论文当成目标论文的方式。

更讽刺的是，这篇撞号的论文跟我的文章主题还沾点边（世界模型、多模态），差点让我以为「AI 在世界模型上也有突破」，直接写进稿子里。

所以这条纪律我写死在这儿：引用任何编号之前，必须打开页面确认标题和作者。

坑二：GitHub 递归 tree 拉不下来。

我看到官网说 4310 万行 Lean，想自己验一下这个数量级。方法很朴素：拉 GitHub 的 recursive tree，统计 .lean 文件数和字节数。

结果卡住了。这个 repo 的顶层 tree 一看就很大：

CFSG.lean                    120786
Certificates.lean            231223
CertifiedResults.lean         17245

我改成逐目录走（非 recursive 模式），走到一半撞上 core 限额 60/小时打满，剩下的目录全是 403。

最后我实测到的、可以负责任写进文章的东西是：

repo AxiomMath/CFSG，84 star / 12 fork / 2 watcher，Lean 语言，仓库总大小约 6.07 GB
创建于 2026-10-27 13:19 UTC，最后推送 2026-10-27 15:07 UTC
只有一个 commit，commit message 就是 "Initial commit"

我实测过的 repo 元数据：

仓库	star	fork	语言	创建日期	最后推送
AxiomMath/CFSG	84	12	Lean	2026-10-27	2026-10-27
google/elephant-goldfish-model	3501	229	Python	2026-09-13	2026-10-28
dagoSte/squadra	816	50	Python	2026-09-28	2026-10-27
elder-plinius/T3MP3ST	6628	1380	TypeScript	2026-07-02	2026-09-08

4310 万行这个数字我最终没能独立验证。 官网和 README 都这么写，repo 也确实有 6GB 那么大、且只有一个 commit 的形态（先攒好再一次性推），量级上说得通，但我必须写清楚：这是官方数字，我复核了仓库元数据没复核行数。

一个 4310 万行的 Lean 证明，lake build 编译时间超过 24 小时（README 原话是 "get this project's build time under 24 hours"）。一天半的编译时间，意味着每一次 CI 验证都是一天半。 这本身就是一个工程事实：形式化的验证成本已经从「跑一次」变成了「跑一天」。

坑三：抽 PDF 文本抽出一堆二进制垃圾。

Divergence 的 preprint 9.5MB，BigHat 的合作报告 5.5MB。我用正则抽 PDF 里的字符串操作符，结果抽出来 8200 万字符，其中绝大部分是字形轮廓数据——一堆 ÿÿÿÿ 和随机符号。

后来加了个过滤：只保留同时含 BT、ET、Tf 三个标记的流（真正的 PDF 文本流），图像流自然被排除，Divergence 那篇的摘要才干净地抽出来了。

这三个坑有个共同点：都是「看起来在验证，实际上在传递错误」。 盲猜编号是在传递别人的错误，统计 tree 是在传递一个我还没验证就准备写的数字，抽 PDF 是在传递二进制当文本。

6. 三种「判定权」的分配方式

到这儿可以收一下了。今天三个故事，其实对应三种判定权归属，而三种都成立，各有代价。

第一种：AI 生成候选，人类逐条裁定。 Enveda 是典型。11 条人类问题全中 + 7 条额外发现，裁定人加第二人复核，时间 9.4 倍下降，成本每页 0.035 美元。

代价很清楚：AI 的召回率上去了，精确率靠裁定人兜底。 论文里「CDP raised every one of the 11 in at least one of its runs」这个措辞，说明召回是不稳定的。如果你不做多次运行取并集，会漏。

第二种：AI 生成候选，人类重新定义评价标准。 BigHat 是典型。一半路程时人类自己怀疑指标是错的，AI 参与重新提指标、改协议，人类执行。

代价是：这个模式没法规模化。 一个团队要能走到「我们的评价指标本身有问题」这一步，需要有足够的领域深度去质疑指标，还要有胆量推翻已经跑了半年的实验设计。

第三种：AI 训练出一个能力，论文和判断由人署名。 CFSG 和 GLM-Omni 是典型。4310 万行 Lean 证明 + 一个发在 hexagon 上的、标着 "Primarily human-written" 的论文；KTP 协议 + 一篇把「会画不会说」量化出来的论文。

代价是：周期长到无法跟产品节奏比。 CFSG 那个 repo 创建于 10 月 27 日，今天 10 月 28 日。它不解决任何产品问题，它解决的是「一千页证明里漏了群」这个问题。

然后是今天第四个、也是我最想单独拿出来说的东西。

Python 的实验性 JIT，要被从 CPython 主分支里拿掉了。

HN 461 分、249 条评论，是今天这批里讨论最激烈的技术话题之一。事情是：Brandt Bucher 2024 年初把 JIT 合进 CPython 3.13，做的是 PEP 744（informational PEP，只提供信息不代表正式共识）。2026 年 6 月，Python 指导委员会要求走 standards-track PEP 并给了六个月期限，逾期就把 JIT 代码从主分支移除。Bucher、Ostrowski、Ken Jin 起草了 PEP 836，7 月 3 日发布，讨论了几个月。

然后 10 月 19 日，Ostrowski 宣布撤回。理由是她自己的原话：

The Steering Council rightly sets a high bar for a proposal of this scope, and we don't feel we have the personal bandwidth to carry the current version forward.

委员会那边要求的东西也很具体：PEP 836 里 compat review 里程碑定在 Python 3.17 RC（预计 2028 年 8 月），委员会的原话是「We think that's way, way too late, and the compatibility review should be an ongoing and continuous process starting as soon as possible」；还要求补充安全审查，讨论设计决策时是否有更大范围的开发者参与。

为什么这条要放进今天这篇？因为它补上了判定权的第三种形态：委员会的否决权。

Enveda 的裁定人可以复核，BigHat 的研究者可以推翻指标，CFSG 的作者可以署名论文——这些都是在「推进」方向上的判定权。 而 Python 指导委员会做的是否决：你说这个项目有技术价值，我们认；但你说不出维护承诺、支持计划、兼容性回归怎么做、性能标准是什么、安全怎么审——那就不许留在主干里。

HN 上一条评论说得比我狠：

It's not red tape, it's about making sure that the effort actually delivers what it promises and can continue to do so in the future.

还有一条更扎心的：

Claude rewrite the performance bottlenecks in Rust works so well it is hard to see the security surface area and harder reason about performance as something that should be paid in core.

这句是今天所有材料里最值得贴在墙上的一句。 用 Rust 重写热路径这件事，AI 干得又快又好，但你没法一眼看出安全面在哪，性能也没法论证该不该放进核心。

还有一条观察是从 HN 评论里挖出来的，我觉得比技术讨论本身更有意思：

There's been work trying to get the JIT to play nice with instrumentation, debugging, and profiling. There's also external JITs (like CinderX), JIT-adjacent things (like Numba and PyTorch's compile), and discussions about a tier 3 JIT.

JIT 死了，但 JIT 需求没死。 于是评论里立刻有人喊：那我 Rust 重写。

这才是真正的判定权问题。 当一个功能因为「说不清维护承诺」被移出主干，需求不会消失，只会流向那些不需要为兼容性负责的地方。这不是技术问题，这是责任归属问题。

7. 今天能直接拿走的六条

这几条是从三份材料里抽出来的、能落到明天工作里的。

第一条：接 AI 进任何审核流程，先建「已知问题测试集」，再动提示词。

Enveda 的做法直接抄：固定 12 份有已知发现的记录，每个候选配置跑最多 3 次，每个发现标记「被几次命中」。因为你能直接观察的量是发现数量，而数量变化同时对应「变好」和「变迟钝」两种状态。 不建这个集，你连自己在干什么都说不清。

第二条：给 AI 的输出设一条「只能更保守」的封顶规则。

Enveda 那句原文可以直接当设计原则写进你的系统：AI 的建议只能被规则往更谨慎的方向改，不能往更宽松的方向改。模型不确定的时候，输出「需要核实」，别输出一个猜测。

第三条：给你的 AI 输出配一个固定裁定人 + 一个复核人。

Enveda 的做法是「one Quality adjudicator scored all comments and a second person confirmed each comment score」。这两个人手不是因为资源富余，是因为一条 AI 发现的责任必须落到一个具体的人头上，否则它就只是一条没人负责的提示。

第四条：区分「AI 的错」和「人的错」，别用同一套复核标准。

Enveda 那组数据：人的无效评论是设计意见、读不出来的条目、个人偏好；AI 的无效评论是机械的数值核对。AI 不会犯品味错误，它犯刻度错误。 所以对 AI 输出要多查数值和越界，对人输出要多查逻辑和意图。用同一套标准审两头，两头都审不好。

第五条：评估 AI 能不能被调用，别只看它自己的指标。

GLM-Omni 是最好的例子：视觉 54%，文字 14.57%。训练目标里没有那条调用路径，能力就调不出来。 你要评估一个多模态模型「能不能用」，必须问「用我关心的那个模态问它，它答得对吗」，而不是看它在自己那个模态上的分数。

第六条：AI 一旦要进入主链路，「谁来维护它」的答案比「它多准」重要。

Python JIT 的死因是说不清维护承诺、安全评审、兼容性回归节奏。今天你在选 agent 框架、选 harness、选模型路由层的时候，同一个问题已经在了： 这个东西半年后谁维护？它的接口变了谁来通知下游？它被换掉的时候，你的流程要不要重写？

Enveda、CFSG、Python JIT 三件事里，只有一件是纯工程，两件都在问同一个问题：AI 的产出要变成生产资料，中间必须有一道有名字的门。 Enveda 那道门叫 Quality adjudicator，CFSG 那道门叫 "Primarily human-written" 标签和 Ken Ono 的署名，Python 那道门叫指导委员会的六个月期限。

8. 最后

今天这三件事有一个共同点，我想再说一遍，因为这是开头那个结论的落点：

Anthropic 让 Claude 审药厂记录、Lean 团队用 4310 万行证明找出一篇论文的错误、清华和智谱发现多模态模型会画不会说——它们都在回答同一个问题：一个不会真正理解你在意的那个东西的模型，怎么被安全地用在它真正重要的地方。

答案的形状已经清楚了：别再追求「让模型更准」，要去建一个能判定模型输赢的裁判台。 Enveda 造了，Lean 团队造了，智谱那篇论文的 KTP 协议造了，Python 指导委员会用否决权也造了一个。

而这三份材料最让我服气的地方，是它们都没有夸大自己。

Enveda 那篇论文主动写「9.4 倍反映的是错误被提前摆到审核员面前，而不是审核标准的降低」，还写「发现了 7 个额外问题的是 Opus 4.7 那一趟，Opus 5.5 那一趟的审阅时间没记录也不呈现」。 CFSG 那篇论文写「这个障碍只针对那一条特定论证路线，不平衡群定理还有别的证明」。 KTP 那篇论文写「三种模型在数字和书名任务上正确率仍然是 0%」，写「Textual Alignment 之后 GLM-Omni 从 14.57% 降到 12.57%」。

在这个所有人都在贴冠军徽章的赛道上，把「我在哪输了」和「这条数字不适用于哪里」写进正文，反而是最强的信号。 这话我说过很多次，今天这三份材料又给我上了一课。

最后说个不太舒服的事实。

我今天本来准备写的是「AI 攻克药物研发」「AI 证出数学史错误」「AI 多模态模型突破」这种标题。三条都很硬，数字都漂亮，放在标题里很唬人。

但我把三份材料读完之后，发现没有一条能这么写。91 个实验变体里只有 3 个超过现有药物，而且只在体外；4310 万行证明对应的是一个「障碍只针对那一条论证路线」的发现，4310 万行这个数字我自己还没能独立验证；54% 的视觉正确率对应的文字问答只有 14.57%，而这已经是三个模型里最好的之一。

真正可以写的标题只有今天这个：AI 给的已经不是答案了。

这条不是泼冷水。这是这批材料共同指向的那个新状态： 模型的产出从「结论」退化成「候选」，而候选的质量上限，取决于你有没有能力判定它。

所以最后这根刺在这儿：

如果你现在的 AI 工作流，是「把模型输出直接当成结果交付」，那你今天学到的三件事一件都用不上。 Enveda 的裁定人、Lean 团队的 "Primarily human-written" 标签、Python 指导委员会那句「我们没有足够的精力」，都在说同一件你可能不想听的事——判定权不是流程里可以省掉的一环，它就是流程本身。

而今天最扎人的对照在这儿：FSG 那篇论文的页面标签写着 "Human understanding: all parts"。4310 万行证明，人全懂。

你的流程里，哪个部分是 AI 判的、哪个部分是人判的，现在能一句话说清吗？