Reward-Weighted On-Policy Distillation with an Open Property-Equivalence Verifier for NL-to-SVA Generation

技術概要：NL から SVA 生成のための報酬重み付きオンポリシー蒸留

問題定義
大規模言語モデル（LLM）を用いた自然言語（NL）仕様からのシステムベリロジックアサーション（SVA）生成は、性能の頭打ちに直面している。最も強力な専門モデル（例：CodeV-SVA-14B）であっても、NL2SVA-Human ベンチマークにおいて約 76% の精度しか達成できていない。しかし、この集計スコアは重要な「時間的ギャップ」を隠蔽している。モデルは組み合わせ論理（C1）では良好に機能するが、有界遅延（C2）および活性（C3）仕様では頻繁に失敗する。支配的な失敗モードは「テンプレートの崩壊」であり、モデルは仕様の具体的な時間的要請に関わらず、限られた数のインプリケーションテンプレート（例：|->）に依存してしまう。

特定された根本原因は、訓練目的にある。既存のシステムは、単一の参照アサーションのトークンレベルの模倣を最適化する NL/SVA 対に対する教師あり微調整（SFT）に依存している。このアプローチは、SVA の正しさの意味論的性質を捉え損なう。すなわち、2 つのアサーションは構文的に遠く離れていても意味的に同等であり得るか、あるいは構文的に類似していても意味的に相反し得る点である。さらに、検証器フィードバックを用いた標準的な強化学習（RL）はこの設定において効果的であることが証明されていない。スパースなロールアウトレベルの報酬は、限られた適応予算（LoRA）を持つ小規模パラメータモデル（7B）に対して十分なシグナルを提供できず、SFT ベースラインを上回ることは稀である。

手法：報酬重み付きオンポリシー蒸留（RWOPD）
本論文は、形式検証器を蒸留プロセスに統合し、学生モデルをプロパティ同等の動作へと誘導する手法である**報酬重み付きオンポリシー蒸留（RWOPD）**を提案する。パイプラインは以下の 4 つの主要コンポーネントで構成される。

1. 階層化カリキュラム SFT：蒸留に先立ち、7B の学生モデル（Qwen2.5-Coder-7B-Instruct）はカリキュラムベースの SFT を受ける。この段階では、リプレイバッファを用いて 3 つの段階（C1、C2、C3）で訓練を行うことで、より簡単な時間クラスへのバイアスを解消し、破滅的忘却を防ぐ。重要なのは、モデルがこれらのトークンの構造的な重要性を学習することを保証するために、時間演算子トークン（例：|->、s_eventually）を重み付けする演算子トークン重み付き交差エントロピー損失を採用している点である。

2. オープンプロパティ同等性チェッカー（PEC）：訓練中に Cadence JasperGold などの産業用ツールのコストやクローズドソース性を回避するため、著者はSymbiYosys と Z3に基づいたオープンソースの検証器を導入する。このチェッカーは、C1 および C2 フラグメントに対して有界モデル検査（BMC）を実行する。出力される判定には、EQUIVALENT、IMPLIES_REF_TO_LM、IMPLIES_LM_TO_REF、NOT_EQUIVALENT、または BMC 外の活性ケースに対するUNSUPPORTED がある。PEC は健全である。つまり、出力するEQUIVALENT 判定は常に正しいことが保証されるが、複雑な活性プロパティについては判断を保留することがある。

3. RWOPD 訓練ループ：

   • 学生モデルは、与えられたプロンプトに対して $K$ 個のロールアウトをサンプリングする。
   • オープン PEC はこれらのロールアウトをフィルタリングし、構文的に破損しているか意味的に誤っている（NOT_EQUIVALENT）ものを破棄する。
   • 残ったロールアウトには、PEC の判定に基づいて報酬重みが割り当てられる（例：EQUIVALENT の場合 1.0、片方向インプリケーションの場合 0.6/0.4）。
   • フリーズされた 14B の教師モデル（CodeV-SVA-14B）は、保持されたロールアウトに対して密なフォワード KL（カルバック・ライブライ）発散ターゲットを提供する。
   • 学生モデルは、これらの KL 損失の報酬重み付き平均を用いて更新される。これにより、監督はトークンレベルで密であると同時に、プロパティ同等の動作に基づいて接地されることを保証する。

4. 評価プロトコル：訓練はフィルタリングと報酬形状付けのためにオープン PEC に依存するが、最終評価は完全性と先行ベンチマークとの一貫性を確保するため、産業グレードの Cadence JasperGold prop_eq_checker を使用する。

主な貢献

1. RWOPD アルゴリズム：プロパティ同等性チェッカーを用いて教師の密な監督を制限し、報酬重み付けする新しい蒸留手法。これは、蒸留の密なトークンレベルシグナルと、形式検証による意味論的接地を組み合わせる。
2. オープン SymbiYosys+Z3 PEC：SVA の有界モデル検査フラグメントに対する、ライセンスフリーかつ健全な検証器。先行研究で使用されたクローズドソースのオラクルとは異なり、訓練時のフィルタリングのための再現性のある秒単位の検証シグナルを提供する。
3. 経験的 SOTA：本手法は NL2SVA-Human および NL2SVA-Machine ベンチマークにおいて新たな記録を樹立した。

結果
著者は、LoRA（学習可能パラメータ 0.53%）を適用した 7B 学生モデルを、専門的な 14B モデルおよび 671B の汎用ベースラインに対して評価した。

• 性能：RWOPD は、両方のベンチマークにおいて最高位の pass@1、pass@5、および pass@10 スコアを達成した。NL2SVA-Machine において、専門的な先行 SOTA（CodeV-SVA-14B）を pass@1 で 2〜4 パーセントポイント（pp）上回り、671B モデル（DeepSeek-R1、GPT-5）を pass@1 で 4〜7 pp 上回った。
• 時間的内訳：改善は時間的に非自明なスライスに集中していた。RWOPD は、14B 教師モデルに対して C2（有界遅延）を 7.5 pp、C3（活性）を 11.5 pp 改善した一方、C1 の性能は飽和状態にあった。
• アブレーション研究：
  • 蒸留対 RL：同じ PEC シグナルを用いたスパース報酬最適化（GRPO、IPO）は SFT ベースラインを上回ることができず、密な教師 KL が性能の主要な駆動力であることを確認した。
  • フィルタ対教師：教師なしのロールアウトフィルタリング（拒否サンプリング SFT）はわずかな改善（約 2.5 pp）しか提供せず、密な教師監督が支配的な付加価値であることを特定した。
  • フィルタ精度：EQUIVALENT のみで厳密にフィルタリングするよりも、RWOPD（EQUIVALENT および片方向インプリケーションの両方を使用）が、勾配の可用性と意味論的正確性のバランスを取りながら、より優れた性能を示した。

意義と主張
本論文は、LoRA 適応を伴う 7B モデルという特定の領域において、検証器は RL のための単独の報酬シグナルとしてではなく、密な教師監督のための報酬形状付けフィルタとして最も効果的であると主張する。著者らは、NL から SVA への生成における「隠れた時間的ギャップ」は、データ不足やモデルサイズの欠如によるものではなく、訓練目的（トークンの模倣対プロパティ同等性）の不一致によるものであると論じる。密な蒸留シグナルを形式プロパティ同等性に基づいて接地することで、RWOPD は、より小さく効率的なモデルが、より大きな専門モデルや巨大な汎用 LLM を凌駕し、意味的に正しいハードウェアアサーションを生成することを可能にする。

本研究は「領域声明」として提示されている。7B+LoRA スケールにおいて、健全なオープン検証器とオンポリシー蒸留による強力な教師の組み合わせは、スパースな強化学習よりも検証シグナルの有効利用である。著者らは、C3 学習における間接的なメカニズム（直接の検証器フィードバックではなくカリキュラムのシードに依存）や、活性プロパティにおけるオープン PEC の不完全さにより最終評価が JasperGold に依存する点など、限界を認めている。