[2026年7月29日提交]

查看 PDF HTML（实验性）

摘要：现代集成电路（ICs）日益复杂，使功能验证成为主要瓶颈。主流的硬件形式化验证方法——模型检查——分别验证每个设计实例，且仅输出通过/失败结果，因此证明背后的推理被锁定在求解器启发式中，并在相关设计间重复重建。交互式定理证明可产生显式、可重用的证明产物，但将其应用于硬件仍主要依赖人工，需要专家在形式化、不变量发现和证明开发上投入大量精力。本文提出 CircuitProver，一个基于 Lean 4 的代理式验证框架，支持证明累积和参数化验证。CircuitProver 自动将参数化硬件设计及其自然语言规范翻译为可执行的 Lean 4 模型，随后通过 Lean 反馈迭代构建机器可验证的证明，以确立硬件代码符合规范。证明轨迹与已验证定理被提炼为可重用库，其中的证明策略引导未来的代理推理，已验证引理则支持跨相关硬件验证任务的形式化证明重用。我们还引入了首个用于评估代理式硬件定理证明的基准套件，涵盖多样化的参数化硬件设计、规范、证明任务和评估指标。在 63 个任务上，CircuitProver 成功证明了全部基准，而基线代理仅解决了 92.1%，且平均需要两倍的证明轮次。消融研究表明，累积的证明知识减少了相关验证任务间的冗余证明构建，证明长度缩短 16.3%，验证时间减少 23.2%。

提交历史

来自：Ziyi Yang [查看邮箱]
[v1] 2026年7月29日，UTC 03:25:07 (1,235 KB)