CktFormalizer: Autoformalization of Natural Language into Circuit Representations
CktFormalizer 是一个利用 Lean 4 依赖类型硬件描述语言来引导大语言模型生成硬件描述的框架，所生成的描述在语法上保证正确、无综合破坏性缺陷，并通过机器验证的证明实现功能验证，从而达成近乎完美的后端可综合实现性，并支持安全、自动化的 PPA 优化。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正在请一位才华横溢但略显粗心的建筑师，根据口头描述绘制房屋蓝图。
在传统芯片设计领域，你会要求建筑师使用Verilog（一种用于描述计算机芯片的语言）编写指令。建筑师可能会写出优美的描述，但由于 Verilog 有点像一套松散的规则，建筑师可能会不小心写下“将一根 4 英寸的管道连接到一根 8 英寸的管道”，或者“创建一个循环回到自身的走廊”。
计算机检查语法后会说：“看起来不错！”但当房屋真正建成（芯片被制造）时，这些错误会导致管道爆裂或走廊困住人员。这些是昂贵且无声的故障，往往要数周后才会显现。
CKTFORMALIZER 是一个改变游戏规则的新框架。它不再让建筑师直接用松散的 Verilog 语言编写，而是强制他们使用一种名为Lean的严格数学语言来编写。
以下是其工作原理，使用一个简单的类比：
1. 严格编辑器（编译器）
将 Lean 想象为一位超级严格的编辑，他确切知道房屋必须如何建造。
- 旧方式：建筑师写下“将管道 A 连接到管道 B"。编辑不检查尺寸。稍后，施工队发现管道 A 太小。
- CKTFORMALIZER 方式：建筑师试图写下“将管道 A（尺寸 4）连接到管道 B（尺寸 8）”。编辑立即关门并说：“错误！你不能连接这些。现在修正它。”
- 结果：建筑师（人工智能）获得即时反馈。在尺寸完全匹配之前，他们无法继续前进。这会在铺设第一块砖之前就捕捉到“宽度不匹配”和“循环”问题。
2. 安全网（类型安全）
在旧系统中，你可能会不小心在房间里留一扇开着的门，导致房屋建成了一个通风不良、有缺陷的房间。而在 Lean 系统中，规则如此严格，以至于编写带有缺陷房间的蓝图在物理上是不可能的。
- 如果建筑师忘记描述开关翻转时会发生什么，编辑会说：“你漏掉了一种情况！你必须描述每一种可能性。”
- 这确保了设计是“通过构建实现正确”的。如果它能通过编译（通过编辑器的检查），就保证其在结构上是健全的。
3. 真理证明（形式验证）
通常，为了检查房屋设计是否可行，你会建造一个微型模型并进行测试。有时模型能工作，但真正的房屋却无法工作。
CKTFORMALIZER 使用数学证明。人工智能不仅仅是猜测；它会撰写一个数学证明，声称：“这个新的、更便宜的设计与原始完美设计在所有方面完全一致。”
- 这就像有一位数学家证明，你的新、更便宜的蓝图在功能上与原始设计 100% 相同，精确到最后一个原子，并且适用于每一个可能的场景，而不仅仅是你测试过的那些。
4. 优化循环（智能改造者）
一旦人工智能拥有了一个可行的设计，系统并不会停止。它就像一个智能改造者，看着蓝图说：“我们可以让这栋房子缩小 35%，并减少 30% 的能耗。”
- 人工智能尝试重新排列房间（电路逻辑）。
- 它构建一个新版本。
- 它立即再次运行“严格编辑器”，以确保新版本仍然完美工作。
- 然后，它运行物理模拟，以查看它节省了多少空间和电力。
- 如果新版本更好且仍被数学证明是正确的，系统就会保留它。否则，它会回滚。
结果
该论文在数百个设计问题（如构建计数器、存储单元和交通信号灯控制器）上测试了这种方法。
- 基线（旧方式）：当他们尝试制造芯片时，约**20%**在纸面上看起来正确的设计，在尝试制造时实际上失败了。
- CKTFORMALIZER（新方式）：**100%**通过严格编辑器的设计成功通过了整个制造流程（综合、布局和布线），未发生任何失败。
- 效率：该系统还成功缩小了设计并显著节省了功耗（面积减少高达 35%），同时证明它们仍然是完美的。
总结
CKTFORMALIZER 就像给一位人工智能建筑师一本魔法规则书，防止他们在开始绘图之前就犯下错误。它不再是在建造房屋后希望它不会倒塌，而是迫使建筑师在订购第一块砖之前就证明房屋是坚固的。这将芯片设计从“猜测与检查”的游戏转变为“证明与构建”的过程，从而产生更小、更高效且保证能工作的芯片。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。