面向多项式形式验证中基于 LLM 的人类可读证明生成

Rolf Drechsler

面向多项式形式验证中基于 LLM 的人类可读证明生成

计算机科学中的逻辑 2025-05-30 v1 硬件体系结构符号计算

作者: Rolf Drechsler

摘要

验证是电路与系统设计的核心任务之一。尽管仿真与模拟被广泛使用，但只有基于形式化证明技术才能确保完全的正确性。然而，这些方法通常具有极高的运行时间和内存需求。近期，多项式形式验证 (PFV) 被提出，表明对于许多具有实际相关性的实例，可以给出所需资源上限的界限。但所提供的证明必须是人类可读的。在此，我们研究如何利用基于大型语言模型 (LLMs) 的人工智能 (AI) 现代方法来生成证明，并随后通过推理引擎对这些证明进行验证。我们给出了展示 LLMs 如何与证明引擎交互的示例，并概述了未来工作的方向。

关键词

多项式形式验证大型语言模型人类可读证明电路验证推理引擎

引用

@article{arxiv.2505.23311,
  title  = {Towards LLM-based Generation of Human-Readable Proofs in Polynomial Formal Verification},
  author = {Rolf Drechsler},
  journal= {arXiv preprint arXiv:2505.23311},
  year   = {2025}
}

备注

4 pages; keynote given at 7th International Symposium on Devices, Circuits and Systems (ISDCS 2025), May 27-30, 2025, IIEST Shibpur, Kolkata, India

面向多项式形式验证中基于 LLM 的人类可读证明生成

摘要

关键词

引用

备注

相关论文