[Submitted on 29 Jul 2026]

View PDF HTML (experimental)

Abstract:現代積體電路（IC）日益複雜，使得功能驗證成為主要瓶頸。主流的硬體形式驗證方法——模型檢查——針對每個設計實例分別進行驗證，並僅提供通過／失敗結果，因此證明的背後推理被鎖在求解器啟發式中，且在相關設計中重複重建。互動式定理證明則能產生明確、可重用的證明產物，但將其應用於硬體仍主要依賴人工，需專家投入大量心力進行形式化、不變量發現與證明開發。本文提出 CircuitProver，一個基於代理式 Lean 4 的驗證框架，支援證明累積與參數化驗證。CircuitProver 能自動將參數化硬體設計及其自然語言規格轉譯為可執行的 Lean 4 模型，接著透過 Lean 回饋迭代建構機器可檢查的證明，以確立硬體程式碼符合規格。證明軌跡與已驗證定理會被提煉為可重用程式庫，其中證明策略可引導後續代理推理，已驗證引理則支援跨相關硬體驗證任務的形式證明重用。我們進一步提出首個用於評估代理式硬體定理證明的基準套件，涵蓋多樣的參數化硬體設計、規格、證明任務與評估指標。在 63 項任務中，CircuitProver 成功證明所有基準，而 vanilla 代理僅解出 92.1%，且平均需兩倍的證明回合。消融研究顯示，累積的證明知識可減少跨相關驗證任務的重複證明建構，將證明長度降低 16.3%，驗證時間減少 23.2%。

Submission history

From: Ziyi Yang [view email]
[v1] Wed, 29 Jul 2026 03:25:07 UTC (1,235 KB)