💻 computer science

Autoformalizing Memory Specifications with Agents

本文提出了一种将自然语言 DRAM 规范自动转换为名为 DRAMPyML 的形式化表示的方法，以支持端到端的设计验证任务，并发布了 DRAMBench 数据集以评估硬件自动形式化能力。

原作者： Jan Ole Ernst, Dmitri Michelangelo Saberi, Derek Christ, Thomas Zimmermann, Rajath Salegame, Suhaas M. Bhat, Stanislav Levental, Thomas Dybdahl Ahle, Matthias Jung

发布于 2026-05-04

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Jan Ole Ernst, Dmitri Michelangelo Saberi, Derek Christ, Thomas Zimmermann, Rajath Salegame, Suhaas M. Bhat, Stanislav Levental, Thomas Dybdahl Ahle, Matthias Jung

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

想象一下，你正在试图构建一个极其复杂的高速列车系统（即计算机芯片）。工程师们拥有一本用通俗英语写成的、厚重且详尽的规则手册，它精确描述了列车应如何运行、何时停车以及最高时速是多少。这就是规范（specification）。

问题在于，实际负责建造铁轨和信号灯的人（即验证团队）无法直接阅读这本英语规则手册。他们需要一种严格的、数学化的“代码”，以便计算机能够检查并确保列车永远不会发生碰撞。将这本厚重的英语规则手册翻译成这种严格的代码，目前仍是一个缓慢、人工且容易出错的过程。如果他们翻译错误，列车日后可能会脱轨，导致修复成本高达数百万美元。

本文介绍了一种全新的"AI 翻译器”，专门用于解决存储芯片（即 powering 你的手机、电脑和 AI 服务器的 RAM 类型）领域的这一问题。

以下是他们方法的简要分解，辅以简单的类比：

1. 问题：“翻译丢失”的鸿沟

目前，人类充当翻译角色。他们阅读英语规则手册（例如 DDR5 或 HBM 内存的 JEDEC 标准），并手动编写严格的代码。

问题所在：规则手册非常庞大（有些甚至接近 500 页），且充满细微细节。人类会感到疲惫，而 AI 模型则常常因特定的专业术语而感到困惑，从而导致“幻觉”，即 AI 编造出根本不存在的规则。
后果：验证过程占据了芯片构建时间的一半以上，且错误可能溜过检查。

2. 解决方案：一种专门的“中间人”语言

与其让 AI 直接从“英语规则手册”跳转到“严格代码”（这就像要求某人没有词典就将小说直接翻译成编程语言），作者们创造了一种名为DRAMPyML的中间语言。

类比：将 DRAMPyML 想象成一张通用蓝图。
- AI 阅读英语规则手册。
- 它在 DRAMPyML 中绘制蓝图（看起来像是交通信号灯和火车站的流程图）。
- 这张蓝图随后被自动转换为测试所需的最终严格代码。
为何有效：对 AI 而言，在蓝图中理清交通“流向”比立即让每一行最终代码都完美无缺要容易得多。如果蓝图正确，最终代码也会正确。

3. “智能体”：一个自我纠正的实习生

本文并非仅仅使用标准的 AI 聊天机器人。他们构建了一个AI 智能体，它像一个勤奋且能自我纠正的实习生。

工作原理：
1. 阅读：智能体阅读英语规则手册。
2. 起草：它撰写蓝图的草稿（DRAMPyML）。
3. 测试：它在蓝图上运行自己的测试，以检查其是否合理（例如：“我是否制造了一个列车无法移动的交通堵塞？”）。
4. 修正：如果测试失败，智能体会重新阅读规则手册，找出错误，并编辑蓝图。
5. 重复：它循环执行此过程，直到蓝图通过所有测试。

这被称为**“智能体（Agentic）”**方法，因为 AI 拥有检查自身工作的工具，而不是仅仅猜测一次并寄希望于最好的结果。

4. “基准”：训练健身房

为了证明其方法有效，团队创建了一个名为DRAMBench的大型健身房。

他们手动构建了 13 份完美的“黄金标准”蓝图，涵盖不同类型的存储芯片（从旧的 DDR2 到最新的 HBM3）。
随后，他们让他们的 AI 智能体尝试根据英语规则手册重现这些蓝图。
评分：他们使用一个名为Jaccard 指数的数学分数来衡量 AI 的蓝图与“黄金标准”的接近程度（可以将其理解为“相似度百分比”）。

5. 结果：什么奏效了？

“单次尝试”的失败：当他们要求 AI 在不检查自身工作的情况下一次性完成时，它表现挣扎，尤其是在处理复杂内存类型时。这就像要求一名学生在不允许修改的情况下撰写论文。
“智能体”的成功：自我纠正的智能体表现好得多。它能够修正自己的错误。
- 在没有任何示例参考的情况下，它仍然能够为较简单的芯片掌握基础知识。
- 在有示例的情况下（向其展示旧芯片的蓝图），它变得非常准确，有时甚至能为复杂芯片创建完美的蓝图。
成本：芯片越复杂，AI 所需的“算力”（tokens）就越多。然而，智能体物有所值，因为它产生的结果质量远高于单次尝试。

总结

本文声称，通过使用专门的“蓝图”语言（DRAMPyML）和能够检查并修正自身工作的 AI（智能体），他们可以将令人困惑的英语存储芯片规则手册自动转化为准确、可测试的模型。这减少了人类从事繁琐翻译工作的需求，有望加快芯片设计速度并更早地发现错误。

他们已发布了他们的“健身房”（数据集），以便其他研究人员能够针对这些相同的存储芯片标准测试他们自己的 AI 翻译器。

以下是发表于 ICLR 2026 的论文《使用智能体自动形式化存储设备规范》的详细技术总结。

1. 问题陈述

半导体芯片设计的验证（DV）阶段是主要瓶颈，消耗了超过 50% 的设计生命周期。核心挑战在于将非结构化的自然语言规范（例如存储芯片的 JEDEC 标准）转换为验证所需的形式化、可执行模型。

当前的 AI 方法通常专注于生成孤立的 SystemVerilog 断言（SVA）。然而，这种方法存在显著局限性：

不完整性：SVA 仅检查特定属性，无法生成完整的行为模型、激励生成器或功能覆盖率指标。
歧义性：自然语言规范通常包含歧义，导致大语言模型（LLM）生成语法无效或与协议不一致的断言。
复杂性：现代存储标准（DDR5、HBM3、GDDR7）涉及复杂的时序约束、复杂的命令交互和层次结构，难以通过简单的“提示词到代码”生成来捕捉。

2. 方法论

作者提出了一种智能体自动形式化框架，将自然语言存储规范转换为结构化的、可执行的中间表示形式，称为DRAMPyML，而不是直接生成 SVA。

2.1 中间表示：DRAMPyML

该系统不直接跳转到断言，而是针对DRAMPyML，这是一种基于时间佩特里网（Timed Petri Nets）的 Python 建模语言。

结构：它将存储设备建模为位置（存储体、Rank）、转换（命令，如 ACT、RD、WR）和弧（普通弧、抑制弧、复位弧和时序弧）的元组。
优势：这种表示形式是可执行的，允许生成命令轨迹、激励和时序检查。它作为一个统一的源头，下游可从中导出 SVA、测试平台和覆盖率模型。
形式化定义：论文在数学上定义了 DRAM 佩特里网，并引入了轨迹等价性（Trace Equivalence）的概念。作者提出（并通过实证验证）了猜想 3.4：由于对称性属性，验证小型配置（例如 1 或 2 个存储体）在短轨迹长度（ $k=4$ ）下的轨迹等价性，足以证明完整、复杂设备的等价性。

2.2 自动形式化智能体

该系统采用迭代的智能体工作流（论文中的图 2），而非一次性生成方法：

输入：智能体接收 JEDEC PDF 规范、厂商数据手册以及 DRAMPyML 库。
迭代循环：智能体使用工具（MCP 服务器、LLM API）来：
- 读取规范的具体章节。
- 编写或编辑 Python 代码以构建佩特里网图。
- 自我验证：运行内部验证测试（检查死锁、孤立节点，并生成命令轨迹以与规范进行交叉核对）。
细化：基于验证反馈，智能体迭代细化模型，直到满足结构一致性和时序正确性。
提示策略：本研究比较了一次性提示（带有明确约定的单个提示）与智能体（与环境及工具进行迭代交互）策略。

3. 主要贡献

DRAMBench：发布了首个硬件自动形式化开源基准测试，包含13 个 JEDEC 标准（涵盖 DDR2-5、LPDDR2-5、GDDR5-7 和 HBM2-3）的真实 DRAMPyML 形式化结果。
智能体框架：证明了使用工具增强验证的迭代智能体在复杂规范方面显著优于一次性生成。
理论与实证验证：
- 形式化定义了 DRAM 佩特里网和轨迹等价性。
- 实证证明，在最小配置（1-2 个存储体）上检查短轨迹（ $k \le 4$ ）足以检测生成模型中的语义错误，从而规避状态空间爆炸问题。
基准测试结果：对最先进模型（Sonnet 4.5、GPT-5.2、DeepSeek-v3p2）的综合评估，展示了令牌成本与性能之间的权衡。

4. 实验结果

作者在 DRAMBench 数据集上使用两个指标评估了模型：

Jaccard 指数：衡量生成模型与真实值之间合法命令轨迹的重叠度。
时序约束召回率：衡量正确恢复的真实时序约束的比例。

主要发现：

智能体与一次性：智能体方法在峰值性能上始终表现更高，特别是在复杂标准（如 DDR5、HBM3）且未提供示例的情况下。在没有强先验知识的情况下，一次性生成难以适应陌生的输出格式。
示例的影响：提供“精挑细选”的示例（例如，使用 DDR3 来帮助生成 DDR4）显著提升了两种方法的性能，有时甚至使一次性模型在简单任务上优于智能体。
模型性能：
- DeepSeek-v3p2（开源权重）表现与闭源模型（Sonnet 4.5、GPT-5.2）具有竞争力，在智能体设置中经常超越它们。
- 在提供示例的情况下，Sonnet 4.5 在 HBM2 和 DDR2-4 等标准的结构完美度方面取得了最高成绩。
失败模式：对复杂失败（如 DDR5）的分析显示，智能体在以下方面存在困难：
- 选择正确的原语（例如，错误的预充电命令）。
- 建模存储层次结构（例如，存储体组）。
- 在正确的抽象层级上强制执行时序约束（坐标不匹配导致时序弧变为非活动状态）。
令牌效率：虽然智能体实现了更高的准确率，但它们消耗了更多的令牌。然而，对于复杂规范，“令牌与性能”曲线有利于智能体，因为无论令牌数量多少，一次性模型都无法收敛到正确的结构。

5. 意义

这项工作代表了硬件验证的范式转变：

从断言到模型：它超越了生成孤立断言，转向创建可执行的、结构化的行为模型。这使得验证能够“左移”，允许早期检测设计缺陷，并自动生成多样化的辅助材料（激励、覆盖率、SVA）。
可扩展性：通过利用 DRAMPyML 中间表示和轨迹等价性检查，该方法为验证现代高度并行的存储设备提供了一条可扩展的路径，这些设备此前因过于复杂而无法进行自动形式化。
开放科学：DRAMBench 的发布提供了一个标准化的、专业级的基准测试，填补了 AI 赋能硬件文献中的空白，使社区能够追踪硬件自动形式化的进展。

总之，该论文证明了智能体工作流结合结构化中间表示（佩特里网）是自动化复杂半导体标准验证的最可行路径，克服了当前直接生成断言的 LLM 方法的局限性。