新基准测试发现前沿 AI 模型难觅真实芯片缺陷

前沿模型能否在不误报的情况下发现真实的硬件 bug？我们收集了工程师在开源芯片设计中做出的 86 项修复，其中 84 项是真实 bug；我们隐藏了每个模型看到的是哪个版本，并让形式化检查器来判定。

最佳配置是 Claude Opus 5.5 在最大努力模式下，干净地捕获了 86 个案例中的 16 个，而它的三次报警中有两次是误报。大多数 bug 逃过了所有模型：在默认设置下，84 个真实修复中有 67 个没有被四个模型中的任何一个干净地捕获。

在 86 个案例下，该基准能将大模型与小模型区分开（Opus 5.5 对 Haiku 5.5：10 个 bug 对 1 个，精确 McNemar 检验 p = 0.012），但无法区分最强模型彼此之间的优劣（p ≥ 0.23）。

真实 bug。70 个来自 OpenTitan，16 个来自其他 10 个项目。每个修复都能证明性地改变输出行为，并由形式化 miter 认证；一个简单的模板（“复位后输出为零”）无法捕获它；且没有一个被用于训练我们自己的模型。后来发现其中两个是有意的行为变更，我们保留并标记了它们。

盲测任务。模型阅读一段文档摘录、端口和信号列表，以及模块的一个版本（有 bug 或已修复），但不被告知是哪一个。它编写 3 到 8 条 SystemVerilog 断言来描述预期行为。文件名是中性的，且一个 bug 的两个版本永远不会出现在同一批次中。

精确判定器。Yosys 和 SymbiYosys 在两个版本上运行每条断言，先进行有界模型检查，然后进行 PDR 证明。在有 bug 的版本上失败，只有在同一条断言于已修复版本上被证明时才算捕获；在已修复版本上的任何失败都是误报。在 STRICT 模式下，单次误报即取消捕获资格。

这个名字来自从晶圆厂回来的第一批芯片，在那里漏掉一个 bug 意味着要付出新掩膜版和数月延误的代价。

我们允许 Opus 5.5 最多调用判定器的有界模型检查器五次，且仅在展示的版本上。该方法在 20 个 bug 上设计，并在另外 61 个 bug 上一次性确认。

检查器并未弥合差距。当一条断言收到反例时，模型有 79% 的概率将其丢弃或修改，其中包括 8 条正确暴露了 bug 的断言：它找到了 bug，工具确认了它，而模型却认定自己的断言是错的。

分诊仅在两名独立评审逐字引用其所矛盾的文档原句时，才保留反例。它比随机移除更精确，且跨轮次稳定，但未达到我们预注册的标准。悬而未决的问题是判断反例：是代码错了，还是断言错了？

方块图，从左到右：Opus 5.5 max、Opus 5.5、Fable 5.1、Sonnet 5.5、Haiku 5.5，分别配有检查器、检查器加分诊。

设计是公开的，且一些答案涉及记忆中的上游代码，这只会抬高分数；只有 3 个 bug 是在模型训练截止日期之后修复的，且无一被捕获。六个提示中的枚举表与源不匹配；去掉它们后，STRICT 在 80 个案例中的成绩为 14、12、8、7 和 3。每个提示只运行一次，判定器在模块级别工作并使用受限的断言子集，且该基准尚未经过外部验证。

我们公布每个 bug 的结果、五个 bug 的完整内容，以及每个 bug 和提示的加盐 SHA-256 承诺；盐在审计时公开。其余 81 个 bug 保持私密，以便该基准对未来模型仍然可用。我们可以评估你的模型。

想让你的模型在 First Silicon 上接受评估，或者检查你自己的设计？请在下方给我们留言，或发送邮件至 contact@umwelt.vision。