2026 年 9 月 22 日

1 / 3

SWE-Proof：当测试通过不再等于代码正确，coding eval 的瓶颈转向 specification

9 月 18 日提交的 SWE-Proof 论文值得单独细读，因为它直接碰到了 coding benchmark 一个越来越明显的问题：SWE-bench 一类评测通常把 held-out tests 当作 correctness oracle，只要 patch 通过测试，就记作解决；但测试集只能覆盖有限输入空间，一个“恰好通过这些测试”的 patch 未必实现了 issue 真正要求的行为。SWE-Proof 尝试把这个 oracle 换成 machine-checked proof。原注

团队先设计 Benchproofer：从一个真实 coding issue 和已知正确 patch 出发，为新代码写 formal specification，并把它调用的已有函数用 axioms 表达，再经过机械检查和 adversarial gates，只有 specification 足够可信的实例才进入 benchmark。最终他们从 SWE-bench Verified 构造出 500 个 SWE-Proof 任务，因此这里仍然是现实 repository issue，只是最终正确性不再主要由几个测试样例判定。原注

最重要的结果不是某个模型多拿了几个点。研究者在两个 frontier models 上发现，已经通过 held-out tests 的 patch 中仍有约四分之一到一半能够被 formal verifier 找到 counterexample。也就是说，如果把“tests passed”直接当作 agent coding 能力的 ground truth，一部分 success 实际包含了 specification violation。给 Opus 4.8 提供正确的 formal specification 后，论文报告任务解决率从 85% 提升到 95%。原注

但这个结果马上暴露出第二层问题：谁来写 specification？如果让模型自己生成，收益基本消失。作者审计模型生成的 specifications，只有 62% 通过；主要错误是 faithfulness——spec 只约束了需求的一部分，因此模型可以证明一个比真实任务更弱的命题。论文进一步报告，在最终没解决的实例里，89% 存在 specification faithfulness failure；成功实例中这一比例为 47%。原注

这对 Eval 的影响很具体。过去 coding benchmark 的链条大致是 issue → trajectory → patch → tests → pass/fail；SWE-Proof 增加了一个以前常被默认掉的层次：intended behavior → specification → verification。一旦 verifier 比 tests 更严格，benchmark 的可靠性开始取决于 specification 本身是否忠实。于是“自动评分”并没有消灭人工语义判断，只是把判断位置从 patch 结果移动到了任务规范。

这也给真实业务 benchmark 一个可迁移的思路。对于 structured generation、tool calling 或 workflow agent，如果 grader 只验证几个表面字段或最终状态，也可能出现类似的“test-passing but semantically wrong”。未必需要把业务任务全部 formalize，但可以专门寻找这种 false positive：先找自动 grader 判成功的 trajectory，再用更强的约束、反例生成或 adversarial state 检查它是否真的满足任务意图。SWE-Proof 的实验提供了一个很好的理由去测这个误差，而不是默认 deterministic grader 就等于 ground truth。

2 / 3

Jev：把 Agent 中大量“要不要、选哪个、打几分”的步骤从生成模型里拆出来

Jev 的技术意义不主要在“又出现一个小模型”，而在于它重新划了一次 agent architecture 的边界。 的接口不要求模型生成 JSON 字符串；调用方事先定义 Choice、Score 等输出空间，模型直接在这些有限空间中返回 decision、probability 和 confidence。官方给出的适用任务包括 classify、route、score、extract、judge 和 guardrail。原注

这与普通 LLM 的 structured output 有一个容易混淆但重要的差别。JSON mode 仍然是 autoregressive generation：模型逐 token 写出一个符合 schema 的字符串；Jev 所描述的 System One 接口则把合法输出空间提前固定，因此“生成非法枚举值”这类结构错误可以从输出空间本身消失。不过，结构合法不意味着语义正确。TypeSafe 自己也明确说明 Jev 仍然会判断错误，confidence 的作用是让调用方设置 threshold，在低置信度时转交人或更强模型。原注

这类设计在 Agent 中尤其有现实意义。一次长 trajectory 可能包含几十甚至几百次很窄的决策：邮件属于哪个队列、当前页面是否已经完成某一步、工具返回是否值得 retry、哪个候选 tool 最合适、某个输出是否触发 policy。现在常见做法是每一步都唤醒一个通用 LLM；如果窄决策能够被专用模型可靠承接，agent 的计算结构就会从“一个大模型不断思考”变成“大模型处理开放问题，小模型处理高频封闭决策”。

同一周出现的 CUA-S1-FORMS 给出了更极端的例子：它只有约 70.6 万参数、2.8 MB，任务也被刻意压得很窄——读取已经结构化的网页表单元素和已有值，然后在 USE/CHECK/CLICK/SKIP 一类固定动作之间决策；它不看截图、不负责生成文本，也不做通用规划。模型、训练代码和 eval harness 以 MIT 许可发布。原注

对于评测，这里真正值得建立的长期问题是 routing boundary：什么决策可以从 general model 下放给 specialist，而整体 trajectory success 不下降？单测 specialist 的 classification accuracy 只能回答一部分问题，因为 false positive 与 false negative 在 agent loop 中成本可能完全不同。更有解释力的实验应把它嵌回 trajectory，测任务成功率、升级到大模型的比例、累计延迟和成本，以及 confidence threshold 改变时这些指标怎样移动。这样才能判断所谓 System One 层到底减少了多少推理计算，又引入了多少决策风险。

来源链接未随原文保留；原注可在 GPT 对话中查看。

3 / 3

Qwen-Image-2.1：模型变小、工作流合并，但“开放”需要把权重与使用权分开记录

Qwen 团队这次把视觉生成核心从上一代约 20B 缩到 7B，并把 generation 与 editing 合并进同一个 Qwen-Image-2.1 checkpoint。模型采用 32 层 single-stream DiT，文本和条件图像由 Qwen3-VL 8B 编码；它支持原生 RGBA alpha channel、最多 10 张参考图、mask/circle 等局部编辑以及原生 2K 输出。Diffusers 文档已经加入对应 pipeline。原注

它在推理结构上还有一个值得注意的优化。条件文本和参考图像位于 noisy latent 之前，因此这些 prefix 的 key/value 在各 denoising steps 中保持不变，可以缓存并复用。参考图越多，避免重复计算这部分条件信息的价值越大。对于多参考图编辑，这比只看“7B”更能解释为什么团队强调 inference efficiency。原注

不过这次发布也提醒了一件越来越需要进入模型 registry 的事情：weights availability 与 software freedom 是两条不同轴。Qwen-Image-2.1 权重确实可以下载，官方 Hugging Face 页面也称其 open-source；但页面实际标注的是 qwen-research，而非上一代使用的 Apache 2.0，许可文本限制为研究与评估等非商业用途，商业部署需要另行授权。原注

因此在做模型选型或 leaderboard metadata 时，“open / closed”这个二元字段已经不够用了。至少应拆开记录：weights 是否可取得、license 是否允许商业使用、是否允许修改和再分发、服务是否必须经过官方 API。Qwen-Image-2.1 正好展示了为什么：从可复现实验角度它明显比纯 API 模型开放；从企业落地角度，它又不能被当成 Apache/MIT 模型处理。这是一个由实际许可证差异直接产生的评测与部署条件，不需要额外赋予“开放模型正在倒退”之类更大的趋势结论。

来源链接未随原文保留；原注可在 GPT 对话中查看。