💻 computer science

Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?

本文证明，将大型语言模型与形式化符号工具相结合的新符号方法，能够成功生成用于硬件验证的可证明正确的归纳证明，在中等规模开源RTL设计上实现了84%的成功率。

原作者： Romy Peled, Daniel Kroening, Michael Tautschnig, Yakir Vizel

发布于 2026-05-04

📖 1 分钟阅读☕ 轻松阅读

原作者： Romy Peled, Daniel Kroening, Michael Tautschnig, Yakir Vizel

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

想象一下，你试图证明一台复杂的机器（例如计算机芯片中的数字电路）永远不会做出危险的事情，比如崩溃或泄露数据。在硬件工程领域，这被称为形式化验证。

通常，要证明这一点，需要人类专家编写一个数学“护盾”（称为归纳不变式），涵盖机器可能处于的每一种状态。这就像试图编写一本规则手册，涵盖棋手永远可能做出的每一个棋步。这极其困难、耗时，且往往需要人类发明巧妙的“辅助规则”（引理）才能使证明成立。

这篇论文提出了一个简单的问题：人工智能（特别是大型语言模型或 LLM）能否充当“采矿机器”，为我们寻找这些辅助规则？

以下是他们方法的分解，使用日常类比：

1. 问题：“比特级”壁垒

当前的计算机工具就像非常勤奋但目光短浅的会计师。它们逐个检查每一个数据位（0 和 1）。如果机器非常庞大，会计师就会不堪重负并放弃。
然而，人类专家以“高层概念”思考。他们不数每一粒沙子，而是看到海滩的形状。作者希望看看人工智能能否学会像人类专家那样思考，并生成那些高层辅助规则。

2. 解决方案：“神经符号”团队

作者并没有仅仅要求人工智能“猜测”答案。他们组建了一个拥有两个不同角色的团队，就像一位创意作家和一位严格编辑。

创意作家（LLM）： 这就是人工智能。它的工作是头脑风暴。它查看硬件设计和安全规则，然后吐出一系列潜在的辅助规则（引理）。
- 局限性： 人工智能富有创造力但不可靠。有时它会写出精彩的规则；其他时候则会写出胡言乱语、毫无意义的规则或数学上错误的规则。它会“产生幻觉”。
严格编辑（形式化工具）： 这是一个传统的、僵化的计算机程序。它不在乎创造力，只在乎真实性。它接收人工智能生成的规则列表并进行严格检查。如果规则哪怕有一点点错误，编辑就会拒绝它。如果规则有效，编辑就会保留它。

3. 两种策略

团队尝试了两种不同的方式来组织这种作家与编辑的关系：

策略 A：“批量”方法（非智能体）
想象一下，你一次性问人工智能：“给我 50 个辅助规则的想法。”人工智能写出 50 份草稿。然后编辑审查这一堆草稿，扔掉坏的那些，保留好的，看看它们是否能解决问题。
策略 B：“对话”方法（智能体）
这更像是一场真正的对话。人工智能提出一个规则。编辑检查后说：“不，那个规则是错的，因为 X。”人工智能阅读反馈，从错误中学习，然后再次尝试。他们不断来回循环，直到找到一个有效的规则。论文发现，这种“对话”风格通常更高效。

4. 结果：淘金

团队在110 种不同的硬件设计（从简单的计数器到复杂的存储系统）上测试了这个系统。

成功率： 对于**84%**的问题，他们的系统成功找到了一组辅助规则，证明了硬件是安全的。
“幻觉”问题： 人工智能生成了数千条规则。其中许多是垃圾（语法错误、逻辑谬误）。但由于有“严格编辑”负责过滤，这些垃圾无关紧要。系统只保留了黄金。
超越专家： 他们在世界上最难的难题上测试了他们的系统，即使是全球最好的商业验证工具（“超级会计师”）也无法解决这些问题。他们的人工智能辅助方法成功解决了一些这些“不可能”的案例。

5. 这意味着什么（以及不意味着什么）

它的作用： 它自动化了辅助规则的“开采”。它将构思数学引理的繁重工作从人类工程师手中接管过来。
它的作用： 它并没有完全取代人类工程师。人类仍然需要设置系统并解释结果。此外，该系统目前需要特定格式（SystemVerilog）的硬件代码；它无法使用某些旧工具所用的原始“蓝图”（网表）。

简而言之： 作者构建了一个系统，其中人工智能充当混乱的头脑风暴伙伴，而严格的计算机程序充当质量控制过滤器。 Together，它们可以自动生成确保硬件安全所需的数学证明，解决那些以前标准工具单独处理起来过于困难的问题。

以下是论文《大引理挖掘者：大型语言模型能否为硬件执行归纳证明？》的详细技术总结：

1. 问题陈述

**形式验证（FV）**对于确保硬件设计（RTL）的正确性至关重要。然而，由于大多数模型检查工具具有“位级”特性，验证复杂的工业级设计仍然是一个瓶颈。这些工具难以构建复杂属性所需的高层、与位无关的数学证明。

解决这一问题的标准方法是归纳证明，这需要辅助引理（归纳强化）来证明某个属性。目前，生成这些引理是一项由专家级形式验证工程师执行的、耗时的手工任务。本文探讨的问题是：大型语言模型（LLM）能否自动化挖掘这些辅助引理，从而为硬件验证构建有效的归纳论证？

2. 方法论：神经符号方法

作者提出了一种神经符号框架，将 LLM 的生成能力与形式符号工具的严谨性相结合。该系统不仅仅依赖 LLM 的输出，而是利用 LLM 生成候选引理，并利用形式求解器对其进行验证和过滤。

A. 核心组件

LLM 提示框架：采用两种不同的策略来生成候选引理：
- 非代理（单次提示）：使用包含 $k$ 个（RTL 设计、属性、归纳引理）三元组示例的**少样本（Few-Shot）**提示。这些示例通过语义相似度（使用句子转换器）从预先构建的思维链（CoT）池中进行选择。LLM 使用相同的提示被采样 $n$ 次，以收集多样化的候选项。
- 代理（迭代交互）：将引理生成构建为一个循环。LLM 提出引理，由形式工具进行检查。如果检查失败，工具会提供反馈（指出哪些引理失败及原因）以及“修复”消息。LLM 随后在后续回合中（最多 5 次迭代） refine 其建议。
形式推理算法（FINDINDSTRENGTH）：
- 该算法接收 LLM 生成的候选引理集合，并尝试找到一个子集，使其构成有效的归纳强化。
- 归纳强化：一组引理 $L$ ，使得 $L \land \text{属性}$ 构成一个归纳不变式（满足初始化和递推性）。
- 过程：
  1. 过滤：检查单个引理是否为归纳不变式（使用 1-归纳）或在有界深度内成立（使用有界模型检查，BMC）。
  2. 排序：优先排列已知为归纳不变式的引理，而非仅在界限内成立的引理。
  3. 子集搜索：遍历排序列表的前缀，寻找最小的子集，使其与目标属性结合后构成有效的归纳不变式。
- 工具：使用 EBMC（一种形式验证工具）配合 $k$ -归纳和 BMC 实现。

B. 数据集

该框架在 110 个验证任务上进行了评估，包括：

58 个 SystemVerilog 设计（来源包括 VCEGAR、VIS、v2c 以及自定义的 FIFO/仲裁器/CAM 设计）。
47 个 C 程序衍生示例：将 C 代码转换为 SystemVerilog 有限状态机（FSM），以测试泛化能力。
CoT 池：一组用于少样本提示的手写示例。

3. 主要贡献

神经符号引理生成：展示了首次将 LLM 专门用于挖掘辅助引理，以构建硬件验证中的形式证明。
双重提示框架：实现并比较了静态少样本方法与迭代代理方法，表明后者能够将 LLM 从错误路径中引导出来。
实证评估：对 110 个任务进行了全面研究，突显 LLM 能够成功为中等规模的开源 RTL 设计生成非平凡的归纳论证。
处理幻觉：证明了虽然 LLM 会产生幻觉（生成语法无效或逻辑错误的引理），但形式过滤层可以有效地从噪声中提取出正确的证明。

4. 实验结果

实验在 Amazon EC2 实例上进行，使用了六种最先进的 LLM（GPT-5、Claude 3.7、Claude 4 Sonnet、Claude 4.5 Sonnet、Claude 4.5 Haiku、Claude 4.5 Opus）。

成功率：该框架成功为 110 个验证任务中的 84% 生成了可证明正确的归纳论证。
- 代理设置：解决了 92/110 个示例（84% 成功率）。
- 非代理设置：解决了 84/110 个示例（76% 成功率）。
模型性能：Claude 4.5-Opus 表现最佳，在代理设置中解决了 88 个示例。
与最先进（SOTA）工具的对比：
- 作者确定了 31 个“具有挑战性”的基准，在这些基准上，最先进的工业工具（JasperGold、VC-Formal、rIC3）未能在 10 分钟超时内证明属性。
- 基于 LLM 的方法解决了这些 SOTA 工具无法解决的实例，特别是在需要复杂归纳强化的情况下（例如特定的 FIFO 和仲裁器设计）。
- 在某些 LLM 找到了正确引理但形式检查超时的情况下，结果仍被视为引理生成方面的成功，因为瓶颈在于验证工具的运行时间，而非 LLM 的推理能力。
错误分析：
- LLM 偶尔会幻觉 SVA 语法（例如，无效的操作符、未定义的变量）或使用非 ASCII 字符。
- 代理设置效率更高，通常通过迭代细化搜索空间，用更少的总引理找到解决方案。

5. 意义与影响

工业价值：这种方法有潜力显著减少形式验证工程师所需的手工劳动。通过自动化辅助引理的发现，降低了将形式方法应用于复杂硬件设计的门槛。
超越记忆：结果表明，LLM 正在进行真正的推理而非简单的记忆，因为它们成功泛化到了 C 程序衍生示例，并处理了参数实例化和寄存器命名的变化。
未来方向：作者计划扩展该框架以同时处理多个属性，扩展到更大的工业级设计，并在真实的工业环境中验证该方法。

结论：本文确立了，当 LLM 在神经符号循环中与形式验证工具结合时，它们是自动化硬件归纳证明中最困难部分（即辅助引理的发现）的一种可行且强大的方法。