IC3-Evolve：面向 IC3 硬件模型检查的经证明/反例门控的离线 LLM 驱动启发式演化

IC3，亦称性质导向可达性（PDR），是硬件安全模型检查的常用算法。它检查状态转移系统是否满足给定的安全性质。IC3 要么返回 UNSAFE（表示性质违反）并附反例轨迹，要么返回 SAFE 并附可检验的归纳不变量作为安全性证明。在实践中，IC3 的性能由大量相互作用的启发式与实现选择主导，使人工调优成本高、脆弱且难以复现。本文提出 IC3-Evolve，一个自动化的离线代码演化框架，利用 LLM 向 IC3 实现提出小的、受槽位约束且可审计的补丁。关键在于，每个候选补丁都必须通过证明/反例门控验证才能被采纳：SAFE 运行必须产出可独立检验的证书，UNSAFE 运行必须产出可重放的反例轨迹，从而防止不健全的编辑被部署。由于 LLM 仅在离线使用，部署产物是一个独立的演化后检查器，零 ML/LLM 推理开销且无运行时模型依赖。我们在公开的硬件模型检查竞赛（HWMCC）基准上演化，并在未见过的公开与工业模型检查基准上评估泛化性，结果表明 IC3-Evolve 能够在严格正确性门控下可靠地发现实用的启发式改进。