侦探的困境：为什么我们需要更智能的硬件

想象一下，你正在建造一座巨大且极其复杂的乐高城市。每一块积木都是一个微小的电子开关，它们共同组成了一个计算机芯片，驱动着从你的手机到未来的自动驾驶汽车的一切事物。问题在于，这些城市变得如此庞大和复杂，以至于即使是最优秀的建筑师也无法检查每一块积木，以确保它们不会倒塌。如果有一个微小的开关放错了位置，整个城市都可能崩溃。

多年来，检查这些城市的标准方法一直是一种“黑盒”测试。你构建一个特定版本的城市（例如，有 8 层楼高的版本），运行一个超快速的机器人来查看它是否正常工作，然后它会给你一个简单的“通过”或“失败”的印章。如果失败了，机器人可能会向你展示一张损坏积木的照片。但问题在于：机器人并不会告诉你它为什么坏了，它也不会为下一个城市记住教训。如果你建造一个稍微大一点的、有 16 层楼高的城市，机器人必须从头开始，重新摸索出所有相同的规则，尽管其逻辑几乎是完全一样的。这就像是在解一道数学题，得到答案后就把过程扔掉，以便在处理下一个问题时不得不重新解一遍完全相同的题目。

这就是为什么会出现一个名为“形式化验证”（formal verification）的新领域。形式化验证不仅仅是进行测试，它试图编写一个数学证明来证明这座城市是完美的。但编写这些证明通常是一项极其艰巨的工作，需要人类天才来一步步引导计算机。现在，一组研究人员开发了一个工具，它就像一位超级聪明的侦探，不仅能解开谜题，还能为未来的侦探写下一份“小抄”，让这项工作变得越来越快、越来越容易。

CircuitProver：从每个案件中学习的侦探

这篇论文介绍了一种名为 CircuitProver 的新系统，旨在利用一种名为 Lean 4 的编程语言来检查硬件设计（即那些“城市”）。你可以把 Lean 4 想象成一位极其严厉的数学老师，绝不接受任何错误答案。CircuitProver 是一个“智能体”（agent），这只是一个高级词汇，指代一个可以与这位老师对话、尝试解决问题、听取老师的纠正并不断重试直到正确为止的 AI 机器人。

但真正的魔力不仅在于它能解决问题，更在于它解决问题之后所做的事情。

旧方式 vs. 新方式

在过去，验证硬件就像检查单扇门的单把锁。如果你有一扇门，它可以是 8 英寸宽、16 英寸宽或 100 英寸宽，你必须检查 8 英寸的版本，扔掉笔记，再检查 16 英寸的版本，再扔掉笔记，以此类推。论文指出，这种做法非常浪费。无论门的大小如何，锁的工作逻辑都是一样的。

CircuitProver 通过将门视为一种“参数化”设计改变了游戏规则。它会问道：“我们能否证明这把锁在任何尺寸下都能正常工作？”它不再是检查某一个特定尺寸的门，而是证明了一个涵盖所有可能尺寸的通用规则。

“小抄”库

这是最令人兴奋的部分：CircuitProverter 保留了一个可重用证明库（Reusable Proof Library）。想象一下，你是一名正在调查一系列入室盗窃案的侦探。

1. 第一个案件： 你解决了一起棘手的盗窃案。你进行了 13 轮调查。你发现小偷总是在窗台上留下一种特定类型的泥土。
2. 旧方式： 下次发生类似的盗窃案时，你忽略了之前的笔记。你再次进行了 13 轮调查，重新发现了泥土这个线索。
3. CircuitProver 方式： 在解决第一个案件后，你写下了一份“证明策略”笔记：“如果你看到窗台上有泥土，请立即检查阁楼。” 你还保存了“经机器校验的事实”（即证明了泥土意味着小偷曾出现在那里的逻辑）。
4. 下一个案件： 当新的盗窃案发生时，你的机器人侦探查看了库。它看到了泥土线索，抓取了“检查阁楼”的策略，仅用了 6 轮就解决了案件。

论文显示，通过使用这个库，该系统不仅变得更快，而且变得更聪明了。它能够解决那些标准机器人（没有库的机器人）根本无法解决的问题。

数据说明

研究人员在 63 个不同的硬件任务上测试了 CircuitProver，范围从简单的数学电路到复杂的存储系统。

• 成功率： 一个标准的机器人（被称为“原生智能体/vanilla agent”）成功解决了 92.1% 的任务。而拥有库和智能策略的 CircuitProver 解决了 100%（全部 63 个任务）。
• 速度： 标准机器人在尝试并失败以获得证明的过程中，平均需要 9.2 轮。CircuitProver 仅需 4.6 轮——它的速度快了一倍。
• 时间： 验证设计所需的总时间下降了 23.2%。
• 复杂度： 证明过程本身缩短了 16.3%，这意味着逻辑更加简洁易读。

论文还在巨大的处理器级设计（如真实计算机的大脑）上进行了测试。在这里，收益甚至更大。与标准机器人相比，CircuitProver 将时间和精力减少了 50% 以上。这表明，随着硬件变得越来越复杂，“小抄”库的价值会越来越高，能让研究人员免于每次都重新发明轮子。

它是如何工作的（魔术表演）

CircuitProver 的工作分为三个步骤：

1. 翻译： 它将硬件设计（使用一种称为 Chisel 的语言编写）转换为 Lean 4 的严格数学语言。它还将人类对硬件应该实现的功能的描述也转换为数学问题。
2. 侦探工作： AI 智能体尝试证明该数学问题。如果卡住了，它会向 Lean 4 老师寻求帮助。老师会说：“不，这一步错了，”然后智能体会尝试另一条路径。
3. 库更新： 一旦证明完成，系统并不仅仅是将其存档。它会分析自己是如何解决问题的。它会提取出那些“顿悟”时刻（例如“针对进位使用这种特定的数学技巧”），并将它们添加到库中。下次，智能体可以直接抓取这个技巧，而不是从头开始摸索。

为什么这很重要

论文指出，这种方法是硬件验证领域的一个重大进步。通过积累知识，我们不再将每一个新的芯片设计视为一个全新的谜团。相反，我们建立了一个不断增长的已解谜题库，使得验证未来更复杂的芯片变得更快、更可靠。

研究人员承认，他们的系统目前最适用于特定类型的硬件设计，并且依赖于强大的 AI 模型（他们测试了不同版本的 AI 叫做 Claude，发现 AI 越聪明，结果就越好）。然而，其核心思想——即我们可以教计算机从自身的证明中学习并分享这些知识——是一个强大的新方向。它将硬件验证从一种重复性的、手动的苦差事转变为一种智能的、自我改进的过程。

简而言之，CircuitProver 就像是给侦探配备了记忆和笔记本。它不仅能破案，还能记住自己是如何破案的，这样下次类似的罪案发生时，城市能更快地恢复安全。