IC3-Evolve：IC3ハードウェアモデル検査のための、オフラインLLM駆動ヒューリスティック進化（証明/証人ゲート付き）
arXiv cs.AI / 2026/4/7
📰 ニュースIdeas & Deep AnalysisTools & Practical UsageModels & Research
要点
- 本論文は、LLMを用いてIC3（PDR）ハードウェアモデルチェッカー実装に対し、小さく監査可能でスロット制限されたパッチを提案する、自動オフライン・コード進化フレームワークであるIC3-Evolveを紹介する。
- 証明/証人ゲート付きの検証によって正しさを担保し、SAFE結果には独立に検証可能な証明（証明書）を、UNSAFE結果には再生可能な反例トレースを要求することで、誤った変更を防ぐ。
- LLM推論はオフラインのパッチ探索時にのみ使用されるため、最終的にデプロイされる成果物は、単体で動作する進化済みチェッカーであり、実行時のML/LLM依存や推論オーバーヘッドは存在しない。
- HWMCCベンチマークでの実験により、このアプローチが実用的なヒューリスティック改善を確実に発見でき、厳格な正しさゲートのもとで、追加の未見の公開ベンチマークおよび産業用ベンチマークにも汎化できることを示す。
