IC3-Evolve：基于证明/见证门控的离线LLM驱动启发式进化，用于IC3硬件模型检查
在硬件安全验证领域，IC3（Property-Directed Reachability，属性导向可达性）算法是模型检查的核心工具之一。它通过分析状态转移系统，判断是否满足给定的安全属性，并输出UNSAFE（违反属性，附带反例轨迹）或SAFE（安全，附带可检查的归纳不变量作为证明）。然而，IC3的实际性能高度依赖于大量相互作用的启发式策略和实现选择，这使得手动调优成本高昂、脆弱且难以复现。
IC3-Evolve 的提出，正是为了解决这一痛点。这是一个自动化的离线代码进化框架，利用大型语言模型（LLM）为IC3实现提出小型、槽位受限且可审计的补丁。其核心创新在于引入了证明/见证门控验证机制：
- 对于输出SAFE的运行，必须生成一个可被独立检查的证书。
- 对于输出UNSAFE的运行，必须生成一个可复现的反例轨迹。
这一机制严格防止了不健全的代码编辑被部署，确保了进化过程的可靠性。
离线进化与零推理开销
IC3-Evolve的一个关键设计是完全离线使用LLM。这意味着LLM仅在训练/进化阶段参与，用于生成和评估候选补丁。一旦进化完成，部署的最终产物是一个独立的、进化后的检查器。这个检查器在运行时没有任何机器学习或LLM推理开销，也不依赖任何运行时模型。这消除了将LLM集成到关键安全验证工具链中可能带来的性能、可靠性和复杂性顾虑，使得成果更易于在实际工业环境中落地。
评估与通用性验证
研究团队在公开的硬件模型检查竞赛（HWMCC）基准测试集上进行了进化训练，并在未见过的公开及工业模型检查基准上评估了其通用性。实验结果表明，在严格的正确性门控下，IC3-Evolve能够可靠地发现具有实用价值的启发式改进。这证明了该方法不仅能够自动化地优化IC3性能，还能将改进泛化到新的、复杂的验证问题上。
AI赋能传统工程的范式意义
IC3-Evolve的工作代表了AI，特别是LLM，赋能传统硬核工程领域的一个精妙范例。它没有试图用“黑箱”模型替代经过数十年验证的形式化方法，而是将LLM定位为一个在严格约束下进行创造性探索的助手。通过“离线进化+门控验证”的模式，它既利用了LLM在代码生成和模式发现方面的潜力，又通过形式化验证的“金标准”牢牢守住了正确性的底线。
这种范式为将AI安全、可靠地引入芯片设计、航空航天软件验证等高可信领域提供了新思路。未来，类似的“AI驱动探索 + 形式化保证”框架，有望在更多需要复杂启发式调优的算法和工程问题上发挥作用，推动研发流程的自动化与智能化。