FVRuleLearner：演算子レベル推論ツリー（OP-Tree）に基づくルール学習による形式検証

要旨: 大規模言語モデル（LLM）による注目すべき推論およびコード生成能力により、形式的検証（FV）を自動化することへの関心が近年高まっています。形式的検証は、数学的に厳密な主張によってハードウェアの正しさを保証するプロセスですが、特に自然言語をSystemVerilog Assertions（NL-to-SVA）へ翻訳する作業を通じて、依然として非常に労力がかかります。しかし、LLMは訓練データの不足や、FVオペレータの本質的な複雑さのために、SVA生成が依然として難しい状況です。その結果、機能的に正しいアサーションを生成するためには、正しいSVAオペレータ選択を確実にする、より効率的で堅牢な手法が不可欠です。
これらの課題に対処するために、本研究では、Operator-Level Rule（Op-Rule）学習フレームワークであるFVRuleLearnerを導入します。このフレームワークは、新規のOperator Reasoning Tree（OP-Tree）に基づいており、SVA生成を構造化され、解釈可能な推論としてモデル化します。FVRuleLearnerは、補完的な2つのフェーズで動作します。（1）訓練：NL-to-SVA整合を、オペレータを意識した細粒度の質問へ分解するOP-Treeを構築し、正しいアサーションへ至る推論経路を組み合わせます。（2）テスト：学習したOP-Treeから、オペレータに整合した検索を行って関連する推論トレースを取得し、未見の仕様に対して新しいルールを生成します。包括的な研究の結果、提案したFVRuleLearnerは、構文正しさにおいて最先端のベースラインを平均で3.95%上回り、機能的正しさにおいては31.17%上回りました。さらに、FVRuleLearnerは、機能タクソノミ分析を通じて、多様なオペレータカテゴリにわたるSVAの機能的失敗の平均70.33%を首尾よく低減し、未見のNL-to-SVAタスクに対して学習したOP-TreeをOp-Rule生成に適用することの有効性を示しました。これらの結果により、FVRuleLearnerは、形式的検証におけるドメイン特化の推論とルール学習の新たなパラダイムとして確立されます。