Autoformalizing Memory Specifications with Agents

ICLR 2026 で発表された論文「Autoformalizing Memory Device Specifications with Agents」の詳細な技術的サマリーを以下に示す。

1. 問題定義

半導体チップ設計における設計検証（DV）フェーズは主要なボトルネックであり、設計ライフサイクルの 50% 以上を消費している。核心的な課題は、メモリチップの JEDEC 規格などの構造化されていない自然言語仕様を、検証に必要な形式的かつ実行可能なモデルへ変換することにある。

現在の AI アプローチは、通常、孤立した SystemVerilog アサーション（SVA）の生成に焦点を当てている。しかし、このアプローチには重大な限界がある：

• 不完全性: SVA は特定の性質を検査するが、完全な動作モデル、刺激ジェネレーター、または機能カバレッジ指標を生成するものではない。
• 曖昧性: 自然言語仕様には曖昧さが含まれることが多く、これにより LLM が構文的に無効またはプロトコルと整合しないアサーションを生成してしまう。
• 複雑性: 現代のメモリ規格（DDR5、HBM3、GDDR7）は、複雑なタイミング制約、複雑なコマンド相互作用、階層的構造を伴い、単純なプロンプトからコードへの生成では捉えきれない。

2. 手法

著者は、SVA を直接生成するのではなく、自然言語のメモリ仕様を構造化された実行可能中間表現であるDRAMPyMLに変換するエージェント型自動形式化フレームワークを提案する。

2.1 中間表現：DRAMPyML

アサーションへ直接飛ぶのではなく、システムはTimed Petri Netsに基づいて構築された Python ベースのモデリング言語であるDRAMPyMLをターゲットとする。

• 構造: メモリデバイスを、場所（バンク、ランク）、遷移（ACT、RD、WR などのコマンド）、およびアーク（通常、インヒビター、リセット、およびタイミング付き）のタプルとしてモデル化する。
• 利点: この表現は実行可能であり、コマンドトレース、刺激、およびタイミングチェックの生成を可能にする。また、下流で SVA、テストベンチ、およびカバレッジモデルを導出するための統一されたソースとして機能する。
• 形式的定義: 本論文は DRAM ペトリネットを数学的に定義し、トレース等価性の概念を導入する。また、対称性の性質により、小さな構成（例：1 または 2 バンク）と短いトレース長さ（$k=4$）に対するトレース等価性の検証が、完全で複雑なデバイス全体の等価性を証明するのに十分であると仮定（仮説 3.4）し、実証的に検証している。

2.2 自動形式化エージェント

システムは、ワンショット生成アプローチではなく、反復的なエージェントワークフロー（論文の図 2）を採用する：

1. 入力: エージェントは JEDEC PDF 仕様、ベンダーのデータシート、および DRAMPyML ライブラリを受け取る。
2. 反復ループ: エージェントはツール（MCP サーバー、LLM API）を使用して以下の操作を行う：
   • 仕様の特定セクションを読み取る。
   • ペトリネットグラフを構築するために Python コードを記述または編集する。
   • 自己検証: 内部検証テストを実行する（デッドロックや孤立ノードのチェック、および仕様とのクロスチェックを行うためのコマンドトレースの生成）。
3. 洗練: 検証フィードバックに基づき、構造的一貫性とタイミングの正確さが満たされるまで、エージェントはモデルを反復的に洗練させる。
4. プロンプト戦略: 本研究では、明示的な規約を含む単一プロンプトによるワンショットプロンプティングと、環境およびツールとの反復的相互作用によるエージェント型アプローチを比較する。

3. 主な貢献

1. DRAMBench: 13 の JEDEC 規格（DDR2-5、LPDDR2-5、GDDR5-7、HBM2-3 を網羅）のグランドトゥルース DRAMPyML 形式化を含む、ハードウェア自動形式化のための最初のオープンソースベンチマークの公開。
2. エージェント型フレームワーク: ツール拡張検証を用いた反復的エージェントが、特に複雑な仕様において、ワンショット生成を大幅に上回ることを実証。
3. 理論的および実証的検証:
   • DRAM ペトリネットおよびトレース等価性の形式的定義。
   • 最小構成（1-2 バンク）における短いトレース（$k \le 4$）のチェックが、生成されたモデルにおける意味的バグを検出するのに十分であり、状態空間爆発の問題を回避できるという実証的証明。
4. ベンチマーク結果: 最先端モデル（Sonnet 4.5、GPT-5.2、DeepSeek-v3p2）の包括的な評価により、トークンコストとパフォーマンスのトレードオフを示す。

4. 実験結果

著者は DRAMBench データセット上で、2 つの指標を用いてモデルを評価した：

• Jaccard Index: 生成されたモデルとグランドトゥルース間の合法的なコマンドトレースの重なりを測定。
• Timing Constraint Recall: 正しく回復されたグランドトゥルースのタイミング制約の割合を測定。

主要な知見:

• エージェント型 vs ワンショット: エージェント型アプローチは、特に複雑な規格（例：DDR5、HBM3）や例が提供されない場合、一貫して高いピークパフォーマンスを達成した。強い事前知識なしでは、ワンショット生成は不慣れな出力形式に苦戦した。
• 例の影響: 「厳選された」例を提供すること（例：DDR3 を用いて DDR4 の生成を支援）は、両方の手法のパフォーマンスを大幅に向上させ、時には単純なタスクにおいてワンショットモデルがエージェントを上回ることを可能にした。
• モデルのパフォーマンス:
  • DeepSeek-v3p2（オープンウェイト）は、クローズドソースモデル（Sonnet 4.5、GPT-5.2）と競争力のあるパフォーマンスを示し、エージェント型設定ではしばしばそれらを凌駕した。
  • Sonnet 4.5は、例が提供された場合、HBM2 や DDR2-4 などの規格において最も高い構造的完全性を達成した。
• 失敗モード: 複雑な失敗（例：DDR5）の分析により、エージェントが以下の点で苦戦することが明らかになった：
  • 正しいプリミティブの選択（例：誤ったプリチャージコマンド）。
  • メモリ階層のモデル化（例：バンクグループ）。
  • 適切な抽象化レベルでのタイミング制約の強制（座標の不一致によりタイミングアークが非活性化すること）。
• トークン効率: エージェントはより高い精度を達成するが、より多くのトークンを消費する。しかし、複雑な仕様の場合、「トークン対パフォーマンス」の曲線はエージェントを支持する。なぜなら、ワンショットモデルはトークン数に関係なく、正しい構造に収束できないためである。

5. 意義

この研究は、ハードウェア検証におけるパラダイムシフトを表している：

• アサーションからモデルへ: 孤立したアサーションの生成を超え、実行可能で構造化された動作モデルの作成へと移行する。これにより、検証の「シフトレフト」が可能となり、設計欠陥の早期検出や、刺激、カバレッジ、SVA などの多様な付随物の自動生成を可能にする。
• スケーラビリティ: DRAMPyML 中間表現とトレース等価性チェックを活用することで、以前は自動化された形式化には複雑すぎた、現代の高度に並列なメモリデバイスの検証へのスケーラブルな道筋を提供する。
• オープンサイエンス: DRAMBenchの公開は、AI for Hardware の文献から以前欠けていた、標準化されたプロフェッショナルグレードのベンチマークを提供し、コミュニティがハードウェア自動形式化の進捗を追跡することを可能にする。

結論として、本論文は、エージェントワークフローと構造化された中間表現（ペトリネット）の組み合わせが、現在の直接アサーション生成 LLM アプローチの限界を克服し、複雑な半導体規格の検証を自動化するための最も実現可能な道であることを実証している。