[2026年7月29日提出]

PDFを表示 HTML（実験的）

要旨：現代の集積回路（IC）はますます複雑化しており、機能検証が主要なボトルネックとなっている。主流のハードウェア形式検証手法であるモデル検査は、各設計インスタンスを個別に検証し、合格/不合格の結果のみを示すため、証明の根拠がソルバーのヒューリスティクスの中に閉じ込められ、関連する設計間で繰り返し再構築される。対話型定理証明は代わりに明示的で再利用可能な証明成果物をもたらすが、ハードウェアへの適用は依然として手作業が中心であり、形式化、不変量の発見、および証明開発に専門家の労力を必要とする。本論文では、証明蓄積とパラメータ化検証をサポートする、Lean 4ベースのエージェント型検証フレームワークであるCircuitProverを提案する。CircuitProverは、パラメータ化されたハードウェア設計とその自然言語仕様を自動的に実行可能なLean 4モデルに変換する。その後、Leanのフィードバックを通じて機械検証可能な証明を反復的に構築し、ハードウェアコードが仕様に準拠していることを証明する。証明トレースと検証済みの定理は再利用可能なライブラリに蒸留され、証明戦略は将来のエージェント推論を導き、検証済みの補題は関連するハードウェア検証タスク間の形式証明の再利用を支援する。さらに、多様なパラメータ化ハードウェア設計、仕様、証明タスク、および評価指標をカバーする、エージェント型ハードウェア定理証明評価のための初のベンチマークスイートを導入する。63タスク全体で、CircuitProverは全ベンチマークの証明に成功した一方、バニラエージェントは92.1%を解決し、平均で2倍の証明ラウンドを必要とした。アブレーション研究は、蓄積された証明知識が関連する検証タスク間の冗長な証明構築を削減し、証明長を16.3%、検証時間を23.2%短縮することを示している。

投稿履歴

投稿者: Ziyi Yang [メールを表示]
[v1] 2026年7月29日 水曜日 03:25:07 UTC (1,235 KB)