大規模言語モデルの手掛かりでハードウェア形式検証を支援
Enhancing Word-Level Property Directed Reachability with LLM-Driven Semantic Guidance
この論文をやさしく読む
ひとことで言うと
ハードウェアの正しさを証明する探索に、言語モデルが作る候補の関係式や補助条件を使います。
何に役立つ？
データ処理が多い回路で、形式検証が証明に必要な関係を見つける手助けになります。
この研究の面白いところ
言語モデルの候補をそのまま信じず形式的に検証し、算術問題では33件中28件を解いて通常のPonoの13件を上回りました。
どこまで分かった？
HWMCCでの効果は問題ごとに異なります。提案法の改善は列挙されたベンチマークに対する評価結果です。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
Property Directed Reachability（PDR）はハードウェアの形式検証で重要なアルゴリズムである。しかし、ビット単位のPDRでは高水準の意味がビット展開によって見えにくくなり、データ処理部分の多い設計で苦戦する。ワード単位のPDRはビットベクトルと配列の理論で推論してこの問題に対処するが、証明に関係するワード単位の関係を発見することが性能上の障害となる。本研究は、大規模言語モデル（LLM）でワード単位のPDR探索を導くLLM4PDRを提案する。仕組みは3つある。述語生成では帰納的一般化の途中で状態間の関係を候補述語として抽出する。節生成では、形式的に検証した後に収束を速めるフレームの補題候補を作る。アサーション生成では、反例に基づく修正を通じ、対象の性質を強める補助アサーションを合成する。LLM4PDRをPonoモデルチェッカーに実装し、算術の小規模ベンチマーク、HLSで生成したパイプライン、公開RTL部品、ハードウェアモデル検査競技（HWMCC）の問題で評価した。結果は、LLMによる手掛かりが、データ処理中心の設計および制御とデータ処理を併せ持つ設計で、解ける問題数と実行時間の両方を改善することを示す。最も強い設定は算術ベンチマーク33件中28件を解き、通常のPonoは13件、AVRは11件だった。HLSパイプラインと公開RTLでは、方法ごとに補完的な高速化が得られた。節による指針は深いパイプライン、述語による指針はバスやメモリー制御器の設計で有効だった。HWMCC問題での効果は個々の問題に依存したが、難しい例では顕著な高速化や時間切れの回避が見られた。LLMが作り検証器が確認する意味的な手掛かりは、従来のワード単位PDRを補う実用的な方法となり得る。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-24（UTC）
- 最新改訂
- 2026-09-24 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-24 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
Property Directed Reachability (PDR) is a prominent algorithm for hardware formal verification. However, bit-level PDR often struggles with datapath-heavy designs because bit-blasting obscures high-level semantics. While word-level PDR addresses this by reasoning over bit-vector and array theories, its performance remains bottlenecked by discovering proof-relevant word-level relations. We propose LLM4PDR, a framework leveraging Large Language Models (LLMs) to guide word-level PDR search through three mechanisms: (1) Predicate Generation, extracting state relationships as candidate predicates during inductive generalization; (2) Clause Generation, producing candidate frame lemmas to accelerate convergence after formal validation; and (3) Assertion Generation, synthesizing helper assertions that strengthen the target property under counterexample-guided refinement. We implement LLM4PDR in the Pono model checker and evaluate it on arithmetic micro-benchmarks, HLS-generated pipelines, open-source RTL components, and hardware model checking competition (HWMCC) instances. Results show LLM-generated guidance improves both solved instances and runtime on datapath-heavy and control-plus-datapath designs. The strongest configuration solves 28 of 33 arithmetic benchmarks, compared to 13 for vanilla Pono and 11 for AVR. On HLS pipelines and open-source RTL, different modes provide complementary speedups: clause guidance is effective for deep pipelines and predicate guidance for bus and memory-controller designs. On HWMCC benchmarks, benefits are instance-dependent, demonstrating notable speedups and timeout avoidance on hard cases. These results suggest that LLM-generated, verifier-checked semantic hints can serve as a practical complement to conventional word-level PDR.
著者のコメント
14 pages, 8 figures
arXiv ID: 2609.30131 ／ 要約の誤りについて