本文的实证引用经过分级:正文 29 组承重论断(60 个子项)各经 3 名独立验证者对抗核查(逐字核对一手原文、检索反证),29 组全部挺过反驳、0 组被推翻,并按验证者意见完成 40 余处口径修正;未进入验证流程的引用标【未验证,来源】。厂商与利益相关方的数字在正文中标注口径,文末附来源索引。
本站《当代码变得便宜》的结论是:AI 把软件生产的瓶颈推到验证环节。《AI code review》追问"用 AI 当验证者靠不靠谱",答案是条件句。《Scalable oversight 的地基体检》挖到最底层:"验证比生成容易"按任务族分层,有独立 oracle 处坚实。三篇合起来留下一个建设性的问题:软件世界里,不靠人也不靠 LLM 的裁判到底有哪些?LLM 分别能把它们做大多少?
这个问题有权威的地图。软件测试研究界把"判定程序行为对不对的程序性判据"叫 test oracle;Barr、Harman、McMinn、Shahbaz 与 Yoo 的综述(IEEE TSE 2015)把 1978-2012 年的 694 篇文献分成四类:specified(按形式规约机械判定,317 篇)、derived(从派生物判定——独立实现、跨执行关系、旧版本,245 篇)、implicit(靠通用隐式知识判定——崩溃、越界几乎总是错,76 篇)、以及没有自动 oracle 时由人来判(56 篇)。同一篇综述下了一个判断:与测试自动化的其他环节相比,oracle 自动化"受到的关注显著更少、解决得也更差",是抑制更大范围测试自动化的瓶颈。【已验证】
2015 年写下的瓶颈,恰好是 2023 年后整个行业拿 LLM 猛攻的地方。本文按这张四格地图逐格对账:每格的裁判是谁、裁判独立于 LLM 到什么程度、LLM 进场后的增益有没有经得起独立复测的数字。范围限定在软件/代码的 oracle,不扩到 ML 模型评测。
逐格对账之前,先固定读数规则,防止本文自己犯"可测性偏差"——增益只在容易测的地方可见,于是显得处处增益。
第一问:裁判是谁,离 LLM 多远。证明检查器、编译器崩溃、sanitizer、跨实现差分、mutation 闸、人类分诊——独立性从强到弱排成一条谱。第二问:这一格的独立指标是什么。每格的"LLM 增益"必须用该格自己的裁判来计:fuzzing 格算独立确认的覆盖率与漏洞,定理证明格算验证器判定的完成率,测试格算 mutation-kill,静态分析格算人工裁决的真阳性率——跨格数字不可互比(基线与分母都不同)。第三问:LLM 坐在哪把椅子上。同一个模型可以当生成器(产测试输入)、当提议者(起草规约、规则、关系,交独立机制筛)、或当裁判(直接判对错)。本文的脊柱主张是一个可证伪的条件式:LLM 坐生成器和提议者的椅子、裁决权留给独立机制时,增益有硬数字;LLM 坐上裁判席时,声称的增益在独立复测中系统性缩水。反例会如实呈现,文末据此软化脊柱。
两条前篇已验证的定理全程复用:能力越强的模型错误越趋同(《AI code review》已核,ICML 2025),这直接威胁一切"多个 LLM 互查"式裁判;外接可靠验证器则增益、自我批评则崩塌(《Scalable oversight》已核)。
裁判独立性最强的格子:Lean kernel、SMT 求解器、模型检查器。判决机械、不可说服、错就是错。
完成率这一侧,数字确实硬。Goedel-Prover-V2-32B 在 miniF2F 上 pass@32 达 88.1%,借 Lean 编译器报错做两轮自纠错后升至 90.4%——这个增量专门来自外接验证器的反馈,是"外接可靠验证器则增益"在本格的直接量化;PutnamBench 上它以约 21 倍小的模型解出 86 题(pass@184),超过 DeepSeek-Prover-V2-671B 的 47 题(pass@1024),其 8B 版本更是以约 80 倍小的规模在 miniF2F 同口径上超过后者。【已验证】AlphaProof 以 Lean 验证结果作强化学习的接地反馈拿到 IMO 2024 银牌(28/42,与 AlphaGeometry 2 的组合成绩,独解 3 题、部分耗时 2-3 天超时限;承《Scalable oversight》已验证口径)。裁判越硬,越能放心让模型大量试错——这是全文最干净的正面格。
但攻击面整体上移了一层:验证器只保证"证明⊢陈述",不保证"陈述=意图"。四组独立证据画出同一条裂缝:
assume(false) 让任何实现通过 Verus 验证,且从单个程序雪崩泛化到所有程序,必须外加批评层(含对抗 exploit 模型)才能过滤。被黑的不是 sound 验证器本身,是规约-实现对齐层。【已验证】生产端的对照最能说明当前位置:AWS 主导的 Rust 标准库验证战役(作者自称已报告的最大库验证战役)里,数量级由确定性工具扛——Autoharness 自动产出 16,748 个证明 harness、11,970 个通过 Kani 验证、全战役 989 个函数验证了形式合约(自动 295 + 十六个月人工 694);而 LLM 合约合成被官方原句标注:"This approach is preliminary: the generated contracts require manual review before merging"。【已验证】另有独立评测显示,在规约自动形式化任务上用 LLM-as-judge 打分,会漏掉可执行评测器抓到的 26% 失败案例【未验证,来源:arXiv 2605.26457】——在这格,LLM 当提议者已可用,当裁判还不够格。
崩溃、内存越界、数据竞争"几乎总是错"——这类裁判不需要任何规约,与被测物和生成者都无关。这一格有 LLM 增益最硬的一手数字,也有整张地图上最刺眼的空格。
OSS-Fuzz 的两份一手战报是本格的定标数据。2023 年 8 月:LLM 生成的额外 fuzz target 使样本项目覆盖率提升 1.5%-31%,tinyxml2 行覆盖从 38% 到 69%,全程无人工干预。2024 年 11 月:AI 生成/增强的 target 覆盖 272 个 C/C++ 项目、新增 37 万+行覆盖,并在已被数十万小时 fuzzing 打磨过的项目里发现 26 个新漏洞(报告级口径:sanitizer 崩溃经人工审核后上报维护者)——其中 OpenSSL 的 CVE-2024-9143(官方定级 Low)按 Google 自己的判断疑似已存在约二十年、用人写的现有 target 发现不了,2024-09-16 上报、10-16 修复。【已验证】注意链条里谁在裁决:LLM 只写 target,判决全部来自 ASan 崩溃与上游修复;同一条管线里 Google 也试着让 LLM 分诊崩溃,官方承认这一步尚未达到可以不经人工审核的程度。【已验证】
Big Sleep(Project Zero 与 DeepMind)在以近期代码提交为种子的变体分析设置下,发现 SQLite 开发分支一个可利用的栈缓冲下溢,当天修复、在进入正式发布前拦下。两个口径必须带上:"首个 AI agent 在广泛使用的真实软件中发现此前未知的可利用内存安全问题"是团队自评,且随即有研究者提出在先案例的异议;团队自己也写明,当前一个针对性的传统 fuzzer 很可能至少一样有效。【已验证】
并发检测器:预定必查的八格里唯一的 LLM 空格。传统裁判在这格的生产数字很硬:Uber 在 4600 万行 Go 代码上部署竞争检测器,六个月检出 2000+ 数据竞争、修复 1000+(PLDI 2022)。【已验证】LLM 在检测席上至今拿不出"经 TSan/KCSAN 或上游维护者独立确认"的一手战绩(本次调研做了系统检索,负结果);它的有效姿势出现在别的椅子上——Uber 的 Dr.Fix 用 LLM 给 TSan 检出的 404 个数据竞争生成修复,224 个(55%)成功生成、其中 193 个(86%)经开发者评审采纳合入,验证链是"构建 + 每个测试重跑 1000 次竞争不复现 + 人审"三层。值得记下的细节:被拒的 14% 里,有修复通过了千次重跑闸门仍被人判定不正确——独立机器闸是必要条件,不是充分条件。【已验证】空格有个结构性解释:OSS-Fuzz 接入文档的 sanitizers 字段只列 address/memory/undefined,ThreadSanitizer 事实上未接入这条 AI fuzzing 最大的生产管线(基础设施保留通道、个别 Swift 项目在用,并非不可能)。【已验证】
这格的裁判从"派生物"来:独立实现互相对表(差分/伪 oracle)、跨执行关系(变形测试)。它有全家族最深厚的战绩,也有一条 LLM 时代必须重考的前提。
先立基线,再谈增益。Csmith(PLDI 2011)用随机差分测试三年间向开发者报告 325+ 个此前未知的 C 编译器 bug(GCC 79、LLVM 202,余为商用),25 个 GCC bug 被开发者标为最高的 P1 发布阻塞级;同文的名句:所有其他编译器都有的中端 wrong-code bug,在 CompCert 已验证部分缺席,六个 CPU 年也打不破。【已验证】不用任何 LLM 的 SQLancer++(ASPLOS 2026)在 18 个 DBMS 上报告 196 个此前未知 bug(140 个 logic bug)、92% 已修复。【已验证】任何"LLM 增益"都得和这些基线比,而不是和空白比。这不是假想的坑:ISSTA 2025 的 Kitten——一个不用 LLM 的简单变异生成器——在 24 小时同台对比中覆盖率比 Fuzz4All 高 48.3%(GCC)/9.9%(LLVM)/33.8%(Rustc),平均每场找 15-20 个 bug 而同场 Fuzz4All 是 5.7/0.3/0;部分已发表的"LLM 增益"源于对照组太弱。【已验证】
Csmith 作者当年点破了这格裁判的成立前提:他们从未见过两个不相关的编译器对同一测例产生相同的错误输出,归因于中间表示的多样性;"若各实现犯相同错,我们检测不到——这是无 oracle 差分测试的固有局限"。这个前提是被实验检验过的:Knight & Leveson 1986 年让 27 个团队独立实现同一规格,100 万次测试中共同失效远超独立假设预期(z=100.51),多版本编程的独立性假设在 99% 置信水平被拒绝。【已验证】LLM 时代的复现 2026 年到货:5 个 coding agent 系统 × 23 个模型产出 48 个版本,100 万随机测试观察到 429 个巧合失效,而独立性模型仅预测 115.36 例(z=29.20)——观测是独立假设的 3.7 倍,前提再次被拒;但三版本多数投票仍把平均失效数从 387.44 降到 130.99(预印本)。投票裁判对 LLM 面板:增益衰减,而非归零——这是脊柱的第一个软化条款。【已验证】
LLM 的正确进场姿势,这格给出了全文最干净的两组对照。其一,同框架隔离变量:ShQveL 在 SQLancer++ 同底座、同 TLP 裁判上只把生成器换成 GPT-4o 填充 SQL 片段,新发现 55 个 unique bug、50 个已修复【已验证】;而同一篇论文的受控头对头里,裸 LLM 端到端 fuzzing(Fuzz4All 配 DuckDB 文档)6 小时找到 0 个 bug、吞吐差约 229 倍——尽管它分支覆盖更高(24.5% vs 21.3%),原句:"While exercising code is a necessary condition for finding a bug, it is not sufficient."【已验证】其二,只换裁判的消融:Argus(SIGMOD 2026)让 LLM 提议 SQL 等价查询骨架对、经 SQLSolver 形式证明等价后才充当 oracle,在五个被测烂的 DBMS 上发现 41 个此前未知 bug、36 个确认、27 个已修复;消融实验把证明器换成 GPT-5 当裁判,人工裁定 DuckDB 上收集的 20 个 bug 报告全部是误报(20/20),而证明器把关的那组是 0/20。机制值得逐字记:LLM 裁判的单对判定错误率其实只有约 1/20,但成熟 DBMS 的 bug 底率极低,报告层面误报被底率放大到 100%——低错误率 × 极低底率 = 误报淹没真报。【已验证】
变形关系(MR)的提议席同样如此:无过滤让 ChatGPT 直接提议 MR、两位领域专家裁决(κ=0.86),简单程序类正确率 49.3%、非 AI/ML 复杂系统仅 7.0%,连被研究最透的 sine 函数都有 85% 的候选是错的(预印本);SANER 2025 的大规模实证(37 个被测系统)里 GPT-3.5/GPT-4 提议的 MR 分别仅 29.86%/43.79% 有效——但 GPT-4 有 38.63% 的候选是前人从未识别的新 MR。【已验证】提议能力是真的,过半无效也是真的:产出必须过独立筛,筛完才是资产。配上硬裁判后 LLM 生成器确实摸到过最深的 bug 层:LegoFuzz 把 LLM 生成的代码块接上跨编译器 checksum 差分,报告 66 个 GCC/LLVM bug、30 个是 miscompilation 级【未验证,来源:arXiv 2508.18955】;作为对照,其作者对公开报告的文献级梳理结论是 Fuzz4All 与 WhiteFox 一个 miscompilation 都没找到——Fuzz4All 的 oracle 按构造只有崩溃/断言,检不出静默错编译,"确认 bug 数"若不分档会高估触达深度。【已验证】
property-based testing 与不变量挖掘的裁判是属性断言本身:属性写下后裁决机械,但属性的定义权在谁手里,决定了这格的成色。四十年前的 Daikon 就把自己产出的东西诚实地叫 likely invariants——从实现自身观察出的性质,程序错它跟着错【未验证,来源:Ernst et al., SCP 2007】。LLM 代写属性,是同一个结构性弱点的放大版。
裁判是 SMT/验证器的子格,数字最硬。LaM4Inv(ASE 2024)用"LLM 猜谓词 + BMC 证伪过滤 + SMT 终裁"在 316 个 C 程序上解出 309 个正确循环不变量(97.8%),最强既有基线 G-CLN 219 个、RL 方法 Code2Inv 210 个,平均每题仅 3.7 轮查询;微软的 Loopy(GPT-4 + Frama-C 裁决)解出 398/469,仍少于符号工具 Ultimate Automizer 的 430,但补上 31 个后者失败的题,且增益大头来自非 LLM 的 Houdini 筛选(293→383)。【已验证】然后是冷水:InvBench(2025,v1)换成"给 SOTA 验证器提速"的净贡献口径复测,最强模型 o3 仅在 easy split 28.3% 的问题上取得提速、平均仅 1.09 倍,hard split 增益可忽略——"正确的不变量"距"有用"还差一个量级(注意该基准 2026 年 1 月的 v2 已改名 Quokka 并报出正向结果,但拿到 ≥1.2 倍提速的实例仍不到一成)。【已验证】
属性由 LLM 自由起草的子格,衰减层清晰可测。人工标注 219 条 LLM 生成的 PBT 属性,21% 不健全(双人标注 κ=0.862),根源是属性幻觉与边界失误;mutation 闸下最强模型 GPT-4 只能为 21% 的文档可提取属性合成正确 PBT。【已验证】nl2postcond(FSE 2024)的人工分类更细:47.4% 的 LLM 后置条件含类型检查成分(单独的纯类型检查占 16%),该类 bug-completeness 仅 0.14;在真实 Defects4J 上全部模型与提示合计只判别 64/525(12.2%)个 bug——单条属性的"正确率"很高,"杀伤力"隔着一整个平凡属性衰减层。【已验证】另有受控实验显示 LLM 生成的 oracle 系统性偏向"实际实现行为"而非"预期行为",判断 oracle 正确性的准确率不足 50%【未验证,来源:arXiv 2410.21136】。
学习式 oracle 的评测协议本身是系统性风险源,这有前 LLM 时代的铁证。TOGA(ICSE 2022)当年声称在 Defects4J 检出 57 个 bug 含 30 个独家;两组独立复测先后到货:ESEC/FSE 2023 在 25 个真实系统、5.1 万注入故障上测得其断言 47% 以上是误报、真阳性断言只带来 0.3% 的故障检出增量;ISSTA 2023 修正"测试前缀取自修复后版本"的评测泄漏(该泄漏抬高发现数 61.8%)后,精度仅 0.38%,一个"期望不抛异常"的零信息基线能以两倍精度找到它 61% 的 bug。【已验证】模型自定义裁判 → 独立复测 → 增益从"30 个独家"缩到 0.3%,这是本文脊柱最完整的一次现形。
反例线如实记录:Anthropic 的 Agentic PBT(Claude Opus 4.1 + Hypothesis)扫 100 个 Python 包产出 984 份 bug 报告,作者从内部评分前 80% 的报告中随机抽 50 份复审,判定 56.0% 为真 bug(95% CI 42.2-69.8%)、32.0% 值得上报;实际上报 5 个,3 个补丁被 NumPy 等上游合并。口径三连:抽样不覆盖评分最低的两成报告、置信区间宽、作者既是厂商(评自家模型)之一、其中一位还是 Hypothesis 的核心维护者。真 bug 是真的,但这是"LLM 提议 + pytest 执行判失败 + 人工复审 + 维护者终裁"的全链条战绩,不是 LLM 裁判的。【已验证】
测试是最普及的 oracle,但测试本身的质量谁来判?mutation testing 的答案是往程序里注入小错、看试卷杀不杀得死——1978 年 DeMillo、Lipton 与 Sayward 写下它的两大假设(competent programmer 与 coupling effect),并诚实声明后者"无望证明,是经验原则"【未验证,来源:IEEE Computer 1978 原文 PDF】。这格的当代问题是:LLM 大量产出测试后,拿什么闸门挡住看起来像测试的非测试?
Meta 给了两个生产级答案,数字全部经过口径修正后引用。TestGen-LLM(FSE 2024)的三层独立闸:在 Instagram Reels/Stories 评测(86 个 Kotlin 组件)中,75% 的测试类至少有一个生成用例编译通过、57% 至少有一个连续 5 次执行稳定通过、25% 至少有一个真实提升行覆盖——注意分母是测试类、口径是"至少一个",不是"75% 的生成用例能编译";整体 73% 的改进建议被工程师采纳(跨多场活动的合并数字,单场 51%-94% 波动)。ACH(FSE 2025)更进一步把 mutation 闸工业化:对 7 个平台 10,795 个 Kotlin 类生成 31,677 个 mutant,29%(9,095 个)通过"可编译且不被现有测试杀死"的筛选,据此产出 571 个隐私加固测试,test-a-thon 采纳率 73%。【已验证】结构相同:LLM 坐生成席,build/执行/覆盖/mutation 一路机器闸,人握终审。
学术侧的独立评测给这格标出了两条刻度线。其一,基准污染的方向:在未污染基准 ULT 上,12 个开源 LLM(1.3B-33B)生成测试的语句覆盖从旧基准的 92.18% 腰斩到 45.10%,mutation score 从 49.69% 降到 40.21%;受控对照显示单纯的测试泄漏把覆盖与杀伤各抬约 10 个百分点——覆盖率在简单基准上易饱和、更易虚高,报覆盖不报杀伤的评测先打折(ACM TOSEM,注意未含前沿闭源模型)。【已验证】其二,断言到底锚定什么:在 22,374 个程序变体上,即便测试是 LLM 拿着修改后的代码现场生成的,失败于新代码的 23,977 个测试中 99% 在原程序上通过且执行了被修改区域——论文称之为 residual alignment:LLM 不从眼前代码推导断言,而是从训练记忆里召回标准算法的行为,甚至把改过的代码当成"原程序的 buggy 版本"。【已验证】断言锚定训练先验而非被测实现,所以它天然适合当回归闸(锁住现状),而不适合当正确性裁判。主动抓未知 bug 的上限也被测了出来:TestExplora 在 2,389 个隐藏一切缺陷信号的真实任务上,所测最强模型单次 Fail-to-Pass 率最高 16.06%,agentic 方案五次尝试也只到 29.7%(截至论文所测组合)。【已验证】
静态分析规则是一种规约,分析器机械执行它——但规则的误报靠人裁决,这格天生一半是机器一半是人。
LLM 当提议者,recall 侧有真增益。IRIS(ICLR 2025)让 LLM 推断 taint 源/汇规约、交 CodeQL 数据流引擎独立执行:在人工验证的 120 个真实 Java 漏洞上检出 55 个,比 CodeQL 官方查询的 27 个翻倍还多,并在 30 个项目最新版本里发现 4 个现有工具找不到的未知漏洞。fine print 成对引用:其平均 false discovery rate 按论文口径仍高达 84.82%(作者自称保守上界,人工抽样的 refined 估计约 46%)——即便按乐观口径,仍有近半报告要人来裁,LLM 抬了 recall,没动 precision 的地板。【已验证】
LLM 裸当检测器,独立复测是全文最陡的缩水曲线。PrimeVul(ICSE 2025):SOTA 7B 模型在旧基准 BigVul 上 68.26% F1,在去泄漏、按时间切分、标签经人工抽检的 PrimeVul 上 3.09%——缩水约 22 倍;GPT-3.5/GPT-4 在最严格的漏洞版-修复版成对评测下"no better than a random guess"。IEEE S&P 2024 的 SecLLMHolmes 补上稳健性:仅改函数/变量名,GPT-4 就在 17% 的案例上翻案。【已验证】判断不基于程序语义的裁判,没有资格坐裁判席。
分诊席是脊柱的教科书案例。Semgrep 官方博客的头条是"Assistant 与研究员 96% 一致",fine print 是:误报侧的最终一致率仅 41%(项目初期 25%、整体约 55%),且官方自承设计上刻意保守——"更倾向让开发者修一个误报,而不是漏掉一个真报"。降噪工具的价值恰恰在误报侧,而 LLM 裁判在最需要它的那一半任务上不及格。独立基准 SastBench(2,737 条告警、299 个真 CVE)上,最好的 agentic LLM 分诊配置 precision 仅 16.9%、MCC 0.148(与厂商头条分布不同、不能同台除法,但量级差距成立)。【已验证】窄域反例存在:腾讯在 3 类 bug 上用 LLM+静态混合证据消除 94-98% 误报【未验证,来源:调研线笔记,工业论文】——分诊席不是不能坐,是只能在有独立证据源兜底的窄域里坐。
Barr 分类的第四格是"没有自动 oracle,人来判"。2024-2026 年,这格上演了整张地图上最干净的自然实验——同样是 LLM 产出的"安全发现",接不接独立裁判,结局天差地别。
第一幕:洪水。curl 维护者 Daniel Stenberg 2025 年 7 月的一手数字:安全提交约 20% 被认定为 AI slop,仅约 5% 最终证实为真漏洞;每份报告消耗 3-4 人、每人半小时到三小时,而团队只有 7 人。2026 年 1 月,curl 关闭运行七年的赏金计划(累计确认 87 个漏洞、支付超 10 万美元):确认率从历年 >15% 崩到 2025 年 <5%。同期 Linux kernel 安全列表从约两年前的每周 2-3 份,涨到 2025 年的每周约 10 份且增量"全是 AI slop";Python 生态的分诊者(PSF 安全驻场工程师)独立报告同一现象【未验证,来源:sethmlarson.dev, 2024-12】。而 Mozilla 同期自报未见 AI 低质报告显著增加(月拒收五六份、不到总量 10%)【未验证,来源:TechCrunch 转述发言人,2025-07】——洪水真实,但不均匀,受赏金激励与报告门槛调制。
第二幕:翻转。2026 年 3 月 curl 重返 HackerOne 后,报告频率约为 2025 年的两倍,确认率回升并反超到 15-16%,Stenberg 写道几乎每份报告都不同程度用了 AI("Almost every security report now uses AI to various degrees")。kernel 侧同步:2026 年初起报告涨到每天 5-10 份且大多数正确,以致 Torvalds 在 7.1-rc4 公告里说私密安全列表已"almost entirely unmanageable"——但主因是不同人用相同工具发现相同 bug 的海量重复,失效模式从"假报告"变成了"正确但重复";内核新规(Tarreau 起草)就此把 AI 辅助发现的 bug 定性为按公开披露处理,要求附经测试的可复现用例、敦促附补丁——Torvalds 原话:"If you actually want to add value, read the documentation, create a patch too."【已验证】
这格的机制读法要完整:同一种底层能力,接 sanitizer 崩溃闸,产出 26 个漏洞和一个二十年的 CVE;接人类分诊席,2025 年产出的是每周消耗 7 人团队十几个人时的 slop 洪水。裁判的独立性与机械性,决定同一种 LLM 产出是资产还是负担。但第二幕是脊柱的第二个软化条款:人类裁判格的产出质量是激励结构 × 工具代际的函数,不是恒久定律——kernel 新规的应对方向也印证本文框架:把举证责任推回提交侧,要求附机器可验证的产物(可复现用例、补丁)。
《Scalable oversight》已建立这格的框架:生产环境是最独立、不可说服的裁判,但判决在事后、判决成本等于爆炸半径、且"跑了没出事"不是无罪判决。本篇补的是 AI 编码时代的实证,而它的形状本身就是发现:这格没有干净数字,两个方向的声称都软。
负面方向:DORA 2024 报告 AI 采用增加伴随交付吞吐 -1.5%、交付稳定性 -7.2%,2025 年吞吐转正但稳定性连续第二年为负(观察性问卷口径,承《当代码变得便宜》已验证);Georgia Tech 的 AI 归因 CVE 追踪 2026 年一季度累计确认 74 个且自称是 floor(归因靠修复 commit 的 Git 历史,判决滞后数月)【未验证,来源:CSA research note 2026】。但对称性必须给足:厂商的负面数字同样过不了独立复测——GitClear 的"churn 上升"叙事,被一项对 151 个自述使用 GenAI 的开源仓库的纵向分析正面冲突("与流行叙事相矛盾",churn 无普遍上升)【未验证,来源:arXiv 2507.10422】。本格 LLM 增益的一手硬点只有一个方向:把 LLM 产物降维成独立可检验的表示——微软 Argos 让 LLM 生成可解释、可复现的异常检测规则做运行时监控,在含生产遥测的标注数据集上 F1 最高 +28.3%【未验证,来源:arXiv 2501.14170】。规则一旦写下,裁决就不再依赖 LLM——又是同一个位置论。
把九格摊开,脊柱主张以条件式成立,且比开跑前设想的更精确——决定"LLM 增益"真伪的不是格子,是 LLM 在验证链条里坐的椅子:
三个软化条款,防止把条件式又用成公理:投票裁判对 LLM 面板增益衰减而非归零(387→131);人类裁判格的洪水受激励调制、且随工具代际可逆转(curl 15-16% 反超);独立机器闸必要而不充分(Dr.Fix 千次重跑仍被人拦下 14%)。外加一条跨格通则:增益必须与强非 LLM 基线比(Kitten、SQLancer++、AWS Autoharness),和空白比出来的增益,独立复测时最先蒸发。
《Scalable oversight》的结论是"验证比生成容易"按 oracle 独立性分层;本篇给出它的建设面:软件恰好是人类少数拥有一整柜独立机械裁判的领域——证明检查器、sanitizer、差分、mutation 闸。LLM 时代的验证工程,核心不是造一个更聪明的裁判,而是把 LLM 的无限产能接到这些不可说服的裁判上,并且永远记住哪把椅子它坐不得。
按证据强度排序:
值得盯的判据:OSS-Fuzz 若接入 TSan,LLM 生成 target 能否在并发格复制内存安全格的战绩;Quokka(原 InvBench)的正向重报会不会被第三方复现;kernel 新规("附补丁")运行一年后重复洪水是否被机器可验证产物驯服;以及下一个 TOGA 式案例——哪个"LLM 裁判"产品会先公布带独立复测的误报侧数字。
分类法与创始文献:Barr, Harman, McMinn, Shahbaz & Yoo, "The Oracle Problem in Software Testing: A Survey" (IEEE TSE 41(5), 2015) · Weyuker, "On Testing Non-testable Programs" (1982) · McKeeman, differential testing (1998) · Chen, Cheung & Yiu, metamorphic testing (HKUST-CS98-01) · DeMillo, Lipton & Sayward (IEEE Computer 1978) · Claessen & Hughes, QuickCheck (ICFP 2000) · Ernst et al., Daikon (SCP 2007) · Newcombe et al., "How AWS Uses Formal Methods" (CACM 2015,承 #0) · Knight & Leveson (IEEE TSE 1986) · Yang, Chen, Eide & Regehr, Csmith (PLDI 2011)
形式验证格:Goedel-Prover-V2 (arXiv 2508.03613) · AlphaProof (Nature 2025,承 #3) · miniF2F-Lean Revisited (arXiv 2511.03108, NeurIPS 2025) · ReForm (arXiv 2510.24592) · NL→TLA+ 评测 (arXiv 2606.05792, ICSOFT 2026) · AlphaVerus (arXiv 2412.06176) · Verifying the Rust Standard Library (arXiv 2606.17374) · Verus-SpecGym (arXiv 2605.26457)
fuzzing 与并发格:Google Security Blog, "AI-Powered Fuzzing" (2023-08) 与 "Leveling Up Fuzzing" (2024-11) · Project Zero, "From Naptime to Big Sleep" (2024-11) · Chabbi & Ramanathan, Uber Go races (PLDI 2022) · Behrang et al., Dr.Fix (PLDI 2025) · OSS-Fuzz new project guide · SC-W 2023 LLM 竞争检测 (arXiv 2308.07505)
差分/变形格:SQLancer++ (arXiv 2503.21424, ASPLOS 2026) · ShQveL (arXiv 2505.02012) · Argus (arXiv 2510.06663, SIGMOD 2026) · Fuzz4All (ICSE 2024) · Kitten (ISSTA 2025) · LegoFuzz (arXiv 2508.18955) · Luu, Liu & Chen, ChatGPT MR (arXiv 2310.19204) · Zhang et al., SANER 2025 · "N-Version Programming with Coding Agents" (arXiv 2606.20158)
PBT/不变量格:Vikram et al. (arXiv 2307.04346) · Endres et al., nl2postcond (FSE 2024) · LaM4Inv (ASE 2024) · Loopy (arXiv 2311.07948) · InvBench/Quokka (arXiv 2509.21629 v1/v2) · TOGA 复测:Hossain et al. (ESEC/FSE 2023) 与 Zhongxin Liu, Kui Liu et al. (ISSTA 2023) · Konstantinou et al. (arXiv 2410.21136) · Anthropic Agentic PBT (arXiv 2510.09907)
测试/mutation 格:Alshahwan et al., TestGen-LLM (FSE 2024) · Foster et al., ACH (FSE 2025) · ULT/UnLeakedTestbench (ACM TOSEM, arXiv 2508.00408) · 软件演化下的 LLM 测试 (arXiv 2603.23443) · TestExplora (arXiv 2602.10471)
静态分析格:IRIS (ICLR 2025) · PrimeVul (ICSE 2025) · SecLLMHolmes (IEEE S&P 2024) · Semgrep 官方博客 (2025) · SastBench (arXiv 2601.02941)
人类裁判格:Stenberg, "death by a thousand slops" (2025-07) / "The end of the curl bug-bounty" (2026-01) / "High-Quality Chaos" (2026-04) · Tarreau, LWN (2026-03) · Torvalds, LKML 7.1-rc4 (2026-05) · Larson, sethmlarson.dev (2024-12) · TechCrunch (2025-07)
生产格:DORA 2024/2025(承 #0) · CSA/Georgia Tech AI-CVE tracker (2026) · Ebert et al. (arXiv 2507.10422) · Argos (arXiv 2501.14170) · Goel et al., 错误趋同 (ICML 2025,承 #2)
调研材料与全部验证判定存于研究底座(8+3 条调研线、208 条论断、29 组承重论断 × 3 票,87 票全录)。