arXiv cs.AI· Wenji Fang, Yuchao Wu, Jing Wang, Zhiyao Xie·· 10 小时前AI 评分31
智能体 AI 遇上形式化验证：面向智能体硬件开发时代
Agentic AI Meets Formal Verification in the Era of Agentic Hardware Development
AI 导读
一篇 ASP-DAC'27 受邀论文综述了 AI 时代硬件形式化验证的方法与应用。文章从规格、证明构造和推理引擎三个层面分析智能体 AI 如何推进硬件形式化方法，并讨论形式化方法如何通过 RTL 生成、调试和保持正确性的优化来支撑可靠的 AI 驱动硬件开发。文章还展望了形式化推理成为自主硬件设计固有组成部分的“证明原生”硬件开发方向。
正文 · AI 翻译
摘要：随着 AI 智能体在生成和优化硬件电路方面的能力日益增强，确保 AI 生成设计的正确性变得更加重要。与此同时，AI 的进步降低了开发和应用形式化方法的门槛，为自动化并改进硬件验证创造了新的机遇。本特邀论文概述了 AI 时代硬件形式化方法的方法论与应用。首先，我们从规范、证明构造和推理引擎三个层面考察智能体 AI 如何推动硬件形式化方法的发展。其次，我们讨论形式化方法如何通过 RTL 生成、调试和保持正确性的优化来支持可靠的 AI 驱动硬件开发。我们回顾了代表性研究以及我们近期的贡献，重点介绍关键技术进展和实验结果带来的洞见。最后，我们讨论面向证明原生硬件开发的未来研究机遇，即形式化推理有望成为自主硬件设计的组成部分。
| 评论： | ASP-DAC'27 特邀论文 |
| 主题： | 人工智能（cs.AI）；硬件架构（cs.AR） |
| 引用为： | arXiv:2611.13705 [cs.AI] |
| （或 arXiv:2611.13705v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2611.13705 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Wenji Fang [查看邮箱]
[v1]
2026年11月10日星期二 07:57:20 UTC（7,242 KB）
来源：arXiv cs.AI · arxiv.org