这次横评的对象不是六个 Web 框架，是一类问题：AI 代码生成器的鲁棒性，到底该怎么评。三套思路拉出来比——端到端基准测、对抗性变异测试、以及这篇 GenOS 论文给的概率操作语义加组合式证书。结论先甩出来：如果你的工作流里 prompt、代码生成器、validator、orchestrator 会换来换去，而且下游关心的是"某个等价事件发生概率变没变"（比如 verified commit），那 GenOS 是你现在能选到的唯一一套能逐层对账的形式化框架；如果你只是想大致知道模型跑分涨了多少、哪条 prompt 更稳，端到端基准和对抗测试在成本上仍然远胜。GenOS 是首选，但只在"你有 PL 理论功底、愿付形式化成本、而且下游保证必须可复核"这个条件下成立。脱离这个条件硬上，是另一种耍流氓对比。
评测条件先交代清楚。我评的是 Corrado Priami 8 月 4 日挂上 arXiv 的 GenOS 论文，Programming Languages 分类。数据来源不是我自己的复现——论文里的证明我读了，审计数据是论文自报的，我据此转述；benchmark 段落会明确标注哪些是论文实测、哪些是我读下来的判断，不把作者的审计当作我重新跑过的实验来陈述。版本就是 2026 年 8 月 4 日这版，没有官方实现、没有开源 benchmark 套件可跑，所以我做不了独立的 20k 次随机核试验复现——这条我只在论文自己的报告范围内成立，换一个实现、换一个 observer 设计，数值可能对不上。评测维度我照旧不凭感觉：组合性、下游保证强度、实施成本、场景适配宽度、审计证据可信度、理论自洽性。每个维度的分都配有评分逻辑。
先把三种评估路子的维度表摆出来（1-5 分，5 最优）：
| 维度 | 端到端基准测 | 对抗变异测试 | GenOS 组合式证书 |
|---|---|---|---|
| 下游保证强度 | 2 | 3 | 5 |
| 组合性 / 可迁移性 | 1 | 2 | 5 |
| 实施成本（越低越好） | 1（最低） | 2 | 5（最高） |
| 场景适配宽度 | 5 | 3 | 2 |
| 审计证据可信度 | 3 | 4 | 4 |
| 理论自洽性 | 2 | 3 | 5 |
几格争议分我点一下。端到端基准的"下游保证强度"给 2，不是它没用，是它只回答"这个快照在这个测试集上过没过"——换个 prompt、换个 validator、换个程序行为分布，分数可能就崩了，而它没有任何机制告诉你崩之前的下限是多少。这格分数我给得低，评的不是测试集质量，是方法本身不携带下游保证的传递性。对抗测试的"场景适配宽度"给 3，是因为它天然偏向发现失效案例而非证明等价保持——它擅长找 bug，不擅长发证书。GenOS 的"实施成本"给 5，最高，是它最大的代价：你得把工作流各层建模成 Markov kernel、接口上携带 observer-relative 等价关系，这套形式化模型不是工程团队顺手能补的。这张表里没有任何一行是通吃的，都是 trade-off。
这套横评方法我前面说最后再说一次——脱离工作流实际变量谈"哪个评估更稳"，就像脱离并发数和连接池配置谈 Fastify 和 Express 的 p99 差几毫秒，拿到手的就是裸数字。GenOS 这篇论文的价值恰恰在于它把"鲁棒性"这个以前只能靠跑分和变异测试去拍脑袋的词，拆成了可以逐层对照着看的东西：prompt 换掉、采样 artifact 换掉、validator 换掉、orchestrator 换掉，每一层都显式建模为 Markov kernel，接口上带等价关系。这跟我上一轮 ORM 横评里反复强调的"先标条件再给数字"是同一件事的两面——那边的核心是数据标条件，这边的核心是等价性标 observer。把这两种味道混在一起读，你大概能理解我为什么盯上这篇论文。
现在进去看 benchmark 段。论文做的那次审计，规模小得我只能叫它审计、不能叫它评测。任务是一个 insertion-sort，形式化契约一条，程序六个，observer 两个，输入空间 121 个，自然语言 paraphrase 若干，然后在这个小规模上做 exhaustive execution。下面是审计结果的对照表（数据来自论文报告，非我的独立复现）：
| 条件 | 结果 | 论文的解读 |
|---|---|---|
| 等价 prompt（paraphrase 后语义等价） | 代码类分布和 commit 分布完全相同 | 这组等价 prompt 在 quotient 后确实下沉到同一分布 |
| prompt 给 in-place 契约 5% 概率 | 被 mutation observer 区分出来 | 下游距离增量控制在鲁棒性边界内 |
| 20k 随机有限核试验 | 没违反任何 exact 或 approximate 律 | 这是 fuzzing 证据，不是证明 |
读这张表时我总得把条件重复一遍：121 个输入、一个排序任务、两个 observer。这个规模下测出"等价 prompt 产生相同分布"，当然是对的——你在这么小的输入空间上穷举，任何合理的商化机制都该做到这点。所以这组数字的置信度只在这个小任务上成立，把它外推到更大的代码生成工作流上，超过了我舒服的范围。但"20k 随机试验没违反定律"这行我要说一句：它是模糊测试，不是形式证明的方向。你在随机采样空间里没打出反例，不代表定理不成立——定理已经证了，这组随机试验只是在给实现层面的正确性拍个照。这格"审计证据可信度"给 4 而不是 5，原因就在这：证据还不足够大，但补足之后上限是 5。
下面说机制，这是这篇论文真正值得读的地方。它证明了几个我很在意的性质：等价兼容的 kernel 会下沉到 quotient 类；quotienting 与分布扩展和顺序组合可交换；workflow bisimulation 成立；sound validation 下 guarded-commit 安全；total-variation 非扩张；以及一个可加性鲁棒性边界。最后这个 additive robustness bound 我得展开说，因为它是把"整体鲁棒性下降 3%"这种垃圾软文数字变成可以逐层对账的机制。一个 pipeline 有 prompt 层、采样层、validator 层、orchestrator 层，总误差可以被显式地分配到每一层，哪一层贡献了多少近似误差、哪一层在等价关系下不兼容，一眼能看。这跟软文测评的差别在哪儿？软文会说"我们的评估框架鲁棒性大幅提升"；GenOS 说"在给定 observer 下，这层的 TV 距离贡献是 delta，把 delta 加总得到总误差上界"。数字裸不裸，一眼能分。这就是为什么我看完论文后想重跑一遍自己的框评——那张维度表打完分之后我盯着"组合性"这列看了半天，结论没变，GenOS 在这一列上是降维打击。
写到这里我忍不住自己推翻一下前面的判断——我前面说"实施成本给 5 是它最大代价"，但实际上这个 5 分里的"高"不见得全是坏事。形式化成本高，高在它逼你把每一层都写清楚；这不就是它在"下游保证强度"上拿 5 的根本原因吗？你付不起成本，保证强度就跟你是零；你付得起，就是往下游一路可验证的传递。天平的每次横评最后都会回到同一句话：没有银弹，只有 trade-off——这次这个 trade-off 的代价明晃晃地写在维度表"实施成本"那格里，没人能替你消掉它。
具体到一个工作流里，这套理论怎么用，我拿论文里的 insertion-sort 任务做个最小对照说明。假设你有两个 prompt，A 是"把数组从小到大排"，B 是"对数组排序，默认升序"。端到端基准怎么评？跑测试，看两次生成的代码在测试集上通过率差多少。对抗测试怎么评？变异输入和 prompt，看哪次让代码行为崩了。GenOS 怎么评？你得先把这两个 prompt 所在的工作流层建模成 Markov kernel，然后在 observer 下定义等价关系——如果 observer 只看最终数组的有序性，那 A 和 B 等价，两个 kernel 该下沉到同一个 quotient 类；如果 observer 是 mutation observer，专盯某个中间赋值行为，那你得重新定义等价关系，A 和 B 可能就分开了。这三个思路的差别不在"谁用了更多测试用例"，在于前两个根本不同后面那个题的题干——它们没有"等价关系随 observer 变化"这个语义层。这就是 GenOS 框架的对抗变异测试绝对追不上的地方。我没写代码示例，是因为这里不贴可运行片段才诚实；一贴伪马尔可夫核的伪代码，就会有人拿去当可复现的实现传播，这是我横评里最想避免的二次失真。
这个模型参数化特性也得点一下。论文说 GenOS 是 model-parametric：compatibility 是一个 measurable property，要靠测试来检验，而不是先假设语言模型行为满足什么条件。这句话很关键。很多关于 AI 代码生成的讨论，包括我自己以前写到一半掐掉的一些想法，都会滑向"假设模型对语义等价 prompt 给相似分布"这种舒适假设里。GenOS 不这么干——它把"这两个 prompt 在这个 observer 下到底等不等价"变成一件可以测量、需要测量的事，然后才在这个测量结果上继续往下推。这与"没有银弹，只有 trade-off"完全对路：不替模型做任何先验担保，只给一套检验机制，验过了再说话。这也是我认为它能在评估系统这个品类里站住脚的根本原因，不是跑分多好看。
接着是场景化的选择建议，把前面六拍收一下。
如果你是一个独立开发者或小团队、只想知道自己换 prompt 或调 generator 之后大概有没有把代码生成质量搞崩，而且没有理论 PL 的工程储备——别上 GenOS，用端到端基准加上你觉得够用的对抗测试就好，成本低、见效快，但要知道它们给你的是统计信号，不是下游保证。
如果你已经在维护一个 AI 代码生成工作流，里面有 validator、orchestrator 这类非平凡编排层，而且你需要对"换了某层之后 downstream verified-commit 概率有没有持久变化"给出可复现的说法——GenOS 的组合式证书目前是唯一能把这件事逐层拆开讲清楚的框架，这个场景下首选，但代价是你得招或培养一个能读懂 Markov kernel 语义的人。
如果你做的事偏安全敏感，比如生成的代码会进生产环境且需要通过 guardian / audit 类的东西，同时对鲁棒性有可问责要求——那 GenOS 加上对抗测试一起用，对抗测试发现问题、GenOS 证明问题在哪个等价类里被挡住，两者不冲突。单用 GenOS 不做对抗测试，你会看不到审计里没覆盖到的反例。
如果你只是写 benchmark 论文、数据集、或者做模型能力对比——端到端基准仍然是你最快的选择，GenOS 的上手成本在你的场景下是负 ROI。
补一句公正补丁：没出现在推荐里的不一定是差方案。对抗测试在发现失效案例这个维度上是端到端基准补不上的，GenOS 目前也不以寻找反例见长；端到端基准在生态和上手速度上是绝对领先——这些不是"差"，是"在你大概会用的场景下不匹配"。我的推荐列只覆盖了四类典型约束，如果你的情况是混合的，比如既要下游保证又要快速迭代，那结论得重新跑。这篇论文目前的审计样本太小，只有 insertion-sort 一个任务的 121 个输入，等作者或社区放出更大规模的实例化数据，某些场景下的推荐列可能会调——我盯着呢。这个结论是当前 arXiv 版本下的，下个大版本如果换了语义模型或者补了开源实现，会重跑。