🤖 AI

NoTB: Oracle-Free Triage of LLM-Generated RTL via Cross-Model Formal Consensus

该论文介绍了 NoTB，这是一个无需先验模型的框架，它通过在多个由大语言模型生成的 RTL 设计之间进行序列等价性检查，以建立形式化共识信号，从而在不依赖测试平台或黄金参考的情况下，实现对功能正确性的高精度分诊。

原作者： Elisavet Lydia Alvanaki, Je Yang, Biruk Seyoum, Luca P. Carloni

发布于 2026-08-25

📖 1 分钟阅读☕ 轻松阅读

原作者： Elisavet Lydia Alvanaki, Je Yang, Biruk Seyoum, Luca P. Carloni

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

在计算机芯片设计领域，工程师传统上编写描述电流如何在电路中流动的代码。这种被称为寄存器传输级（RTL）的代码是硬件的物理蓝图。几十年来，创建这种代码一直是一个细致的人工驱动过程，每一行代码都要经过与信任参考标准的比对，以确保芯片能够正常工作。最近，人工智能开始为我们编写这些代码。大型语言模型——即那种可以写故事或回答问题的同类技术——现在正被要求根据简单的文本描述来生成这些复杂的硬件蓝图。虽然这些模型可以快速生成许多版本的设计，但一个关键问题仍然存在：工程师如何知道这些由 AI 生成的设计中，哪些才是真正有效的？在过去，答案是将 AI 的输出与完美的、由人类制作的参考标准进行对比，或者将其放入模拟测试中运行。然而，创建这些完美的参考标准既昂贵又耗时，而且测试本身有时会遗漏隐藏的错误。

哥伦比亚大学的一个研究小组推出了一种无需完美参考或预写测试即可筛选 AI 生成设计的新方法。他们将该系统称为 NoTB。NoTB 不依赖于单一的裁判来决定一个设计是否优秀，也不依赖于可能遗漏关键缺陷的模拟运行，而是要求多个不同的 AI 模型独立编写同一个设计。随后，它使用一种名为“序列等效性检查”的严谨数学工具，来观察这些不同的版本在每种可能的情况下是否表现得完全一致。其核心思想是，如果来自不同训练方式的多个不同 AI 模型都达成了完全相同的行为，那么它们极有可能找到了正确的解决方案。这种方法使工程师能够在将设计投入实际芯片制造之前，尽早识别出最值得信赖的设计，从而节省时间和资源。

研究人员在 78 个不同的硬件设计任务上测试了这种方法。他们使用四个不同的语言模型家族来为每个设计生成多个版本。对于每个任务，他们都对比了输出结果，以查看哪些在行为上是数学意义上完全一致的。他们发现，当来自四个不同 AI 家族的设计在行为上达成一致时，系统的正确率接近 95%。这种高置信度是以一种权衡为代价的：该系统仅对大约 27% 的任务做出预测。然而，通过将要求降低到仅需三个家族达成一致，该系统可以覆盖 33% 的任务，同时仍保持 87% 的准确率。这为设计师提供了一个灵活的工具：他们可以选择极其谨慎，只接受最确定的设计；或者也可以接受略高的风险，以获得更多可用于进一步测试的设计。

这项研究还揭示了为什么旧的 AI 设计检查方法是不可靠的。一种常见的方法是要求第二个 AI 模型充当裁判，并预测一个设计是否正确。研究人员发现，这种方法并不一致；同一个设计可能会因为执行判断的 AI 模型不同，而被一个裁判判定为正确，而另一个判定为错误。另一种方法是将设计运行在由 AI 创建的测试中。研究人员发现，结果的质量完全取决于该测试的质量。如果测试较弱，它可能会无法捕捉到错误，导致系统误认为一个有缺陷的设计是正确的。相比之下，新方法不依赖于测试或裁判。它依赖于这样一个事实：这些设计在所有可能的输入范围内都被证明是恒等的，因此这种一致性是设计本身的属性，而不是检查工具的属性。

为了使这一过程高效，该系统使用了一种智能过滤技术。它并没有比较每一个设计对，因为这会耗费大量时间，而是首先剔除完全重复的设计，然后将已经被证明是相同的设计进行分组。这显著减少了需要进行的比较次数。从生成设计到完成检查，整个过程平均每个任务耗时一到十六分钟，具体取决于生成的版本数量。运行该系统的成本也是可控的，因为它避免了为了让 AI 模型充当裁判而进行昂贵的重复调用。研究人员强调，这种方法并不是要取代最终验证。相反，它扮演着一种分诊系统（triage system）的角色，旨在对 AI 生成的设计堆进行分类，以便将最有希望的设计送入后续阶段，同时将那些不确定的设计留作更传统的、彻底的检查。

研究结果表明，所使用的 AI 模型的差异性是该系统成功的关键。研究人员测试了如果从组合中移除其中一个 AI 家族会发生什么。他们发现，即使缺少一个模型，系统依然保持稳健和准确，这证明了置信信号来自于群体的集体共识，而非依赖于任何单一模型。这使得该方法在实际应用中具有可行性，因为在实际应用中，获取特定 AI 模型的能力可能会有所不同。研究结论指出，通过将关注点从模拟测试转向对一致性的形式化数学证明，工程师可以构建一个更可靠的流程来使用人工智能进行硬件设计。这使得工业界能够在利用 AI 生成的速度的同时，保持复杂芯片所需的严格安全标准。

技术摘要：NoTB —— 通过跨模型形式化共识实现无测试平台（Oracle-Free）的 LLM 生成 RTL 分选

问题陈述
大语言模型（LLMs）正日益具备根据自然语言规范生成可综合寄存器传输级（RTL）设计的能力。然而，一个关键的瓶颈在于：如何在没有访问信任“真值”（如参考测试平台或黄金 RTL 模型）的情况下，在设计过程早期评估生成的设计的函数正确性。构建此类真值既昂贵又容易出错，且在设计任务初期通常无法获得。

现有的无真值方法存在根本性的局限性：

LLM 作为评判者（LLM-as-a-Judge）： 用基于模型的预测取代执行，但缺乏形式化保证，并表现出强烈的模型依赖偏差，导致误报率（false-acceptance rates）不稳定（在不同模型间差异高达 45%）。
基于仿真的自一致性（Simulation-Based Self-Consistency）： 依赖于在 LLM 生成的测试平台下的行为一致性。这种方法假设测试平台覆盖了相关的输入空间，并且错误的实现彼此之间会产生分歧。在实践中，弱测试平台可能会遗漏关键输入，导致错误的实现形成“虚假共识”；同时，共享的错误模式可能导致多个模型收敛到相同的错误行为上。

方法论：NoTB 框架
作者引入了 NoTB 框架，该框架用形式化跨模型共识取代了启发式的一致性。其核心洞察是：如果由独立训练的 LLM 系列生成的实现通过顺序等价检查（SEC）在整个输入空间内被证明是等价的，那么它们的共识就是设计本身的属性，而非有限测试向量的属性。

NoTB 工作流包含四个阶段：

多模型 RTL 生成： 对于给定的规范，系统从 $M$ 个独立训练的 LLM 系列（例如 Claude、GPT、Gemini、Qwen）中采样多个 RTL 实现。每个模型生成 $K$ 个候选方案，从而创建一个多样化的候选集 $D(s)$ 。
形式化等价聚类： NoTB 构建一个图，其中节点是候选实现，边代表已证实的等价性。它使用形式化工具（Cadence JasperGold）对成对的设计进行顺序等价检查（SEC）。
- 只有当工具证明两个设计对于所有输入序列都产生相同的输出时，它们之间才会建立连接。
- 不确定的结果或接口不匹配不会创建边。
- 该图中的连通分量构成了等价簇（equivalence clusters）。
增量剪枝： 为了管理计算成本（ $O(|D|^2)$ $O (∣ D ∣^{2})$ ），NoTB 采用了轻量级剪枝技术：
- 通过哈希处理合并语法完全相同的代码文件。
- 使用并查集（union-find）数据结构追踪等价分量；一旦一对设计被证明等价，则跳过该分量内的未来比较。
- 位于不同分量代表之间的已证实的非等价性可以防止冗余的跨分量检查。
基于模型多样性的置信度评分： 系统识别出针对某一规范的最大等价簇（ $C^*$ $C^{*}$ ）。置信度得分定义为模型计数：即该簇内包含的不同 LLM 系列的数量。
- 更高的模型计数意味着具有不同归纳偏置的独立模型收敛到了相同的形式化证明行为上。
- 设计师可以设置阈值 $\tau$ （例如 $\tau=4$ ）来仅接受那些主导簇包含至少 $\tau$ 个不同系列的规范。这创造了一个可在精确度（置信度）与覆盖率（接受的规范数量）之间调节的权衡。

核心贡献

展示了测试平台的依赖性： 本文表明，基于仿真的无真值分选高度依赖于测试平台生成器。在固定的候选池上，四向仿真一致性的精确度会根据生成测试平台的 LLM 不同而发生剧烈波动（从 43% 到 84%），而形式化 SEC 则保持稳定（约 95%）。
引入 NoTB： 一个新颖的框架，用形式化跨模型共识取代了基于学习或仿真的协议。它通过 SEC 对候选方案进行聚类，并根据 LLM 系列的多样性对它们进行评分。
校准后的正确性信号： 经验证据表明，模型计数是一个经过校准的信号。系统展示了一种单调关系：更强的跨模型形式化一致性与较低的经验错误率相关联。

实验结果
在 NVIDIA CVDP 基准测试的 78 个 RTL 生成任务上进行了评估，使用了四个 LLM 系列（Claude 3.7、GPT-OSS-120B、Gemini 2.5、Qwen 3），每个系列提供 5 个样本：

四家族共识 ( $\tau=4$ )： 在 27% 的覆盖率下实现了 94.7% 的精确度。
三家族共识 ( $\tau=3$ )： 在 33% 的覆盖率下实现了 87% 的精确度。
与基准对比：
- LLM 作为评判者： 表现出高度的不稳定性；误报率取决于生成器和评判模型。
- 基于仿真的聚类： 精确度随测试平台生成器的不同而剧烈波动（43%–84%），而形式化 SEC 始终稳定在 ~95%。
鲁棒性： 留一法消融实验证实，高精确度信号并不依赖于任何特定的单一模型系列；即使移除其中一个模型系列，仍能保持高精确度。
成本： 虽然 SEC 需要显著的计算时间（取决于样本量，每个规范的中位数为 1–16 分钟），但它避免了运行数千次“评判”调用或为每个候选方案生成多个测试平台的巨大 Token 开销。

意义与主张
本文声称，NoTB 为硬件设计早期的高置信度分选提供了一个可靠的、无真值的依据。通过利用形式化保证而非学习到的启发式方法或有限测试向量，NoTB 使设计师能够选择性地认证一部分生成的 RTL 设计，这些设计极可能是正确的，从而允许设计师绕过早期检查或将其优先用于最终验证。作者强调，NoSB 并不旨在取代对信任真值或完整验证流程的需求；相反，它作为一个过滤器，用于在缺乏黄金参考的情况下识别高置信度的候选方案。该方法被呈现为解决“分选”问题的实用方案，提供了在风险与覆盖率之间进行显式控制的方法，且无需依赖于特定模型的真值。

技术摘要：NoTB —— 通过跨模型形式化共识实现无测试平台（Oracle-Free）的 LLM 生成 RTL 分选

类似论文