IC3-Evolve: 用于IC3硬件模型检查的自动离线LLM驱动启发式进化
IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking
AI总结：
IC3-Evolve通过离线LLM提出小范围修正，实现IC3硬件模型检查的自动优化，确保正确性验证下的启发式改进。
摘要：
IC3，也称为属性导向可达性（PDR），是硬件安全模型检查中常用的算法。它检查状态转换系统是否符合给定的安全属性。IC3要么返回UNSAFE（指示属性违反）并伴随反例轨迹，要么返回SAFE并以可检查的归纳不变量作为安全性的证明。在实践中，IC3的性能主要由大量相互作用的启发式和实现选择决定，使手动调优成本高、脆弱且难以复现。本文提出了IC3-Evolve，一种自动离线代码进化框架，利用LLM提出小、槽位受限且可审计的修正。关键在于每个候选修正必须通过证明/见证门验证：SAFE运行必须发出可独立检查的证书，UNSAFE运行必须发出可回放的反例轨迹，防止不正确的编辑部署。由于LLM仅用于离线，部署的成果是独立的进化检查器，无ML/LLM推理开销和无运行时模型依赖。我们在公开的硬件模型检查竞赛（HWMCC）基准上进化，并在未见过的公开和工业模型检查基准上评估泛化能力，显示IC3-Evolve能在严格正确性门下可靠地发现实用启发式改进。
英文摘要：
IC3, also known as property-directed reachability (PDR), is a commonly-used algorithm for hardware safety model checking. It checks if a state transition system complies with a given safety property. IC3 either returns UNSAFE (indicating property violation) with a counterexample trace, or SAFE with a checkable inductive invariant as the proof to safety. In practice, the performance of IC3 is dominated by a large web of interacting heuristics and implementation choices, making manual tuning costly, brittle, and hard to reproduce. This paper presents IC3-Evolve, an automated offline code-evolution framework that utilizes an LLM to propose small, slot-restricted and auditable patches to an IC3 implementation. Crucially, every candidate patch is admitted only through proof- /witness-gated validation: SAFE runs must emit a certificate that is independently checked, and UNSAFE runs must emit a replayable counterexample trace, preventing unsound edits from being deployed. Since the LLM is used only offline, the deployed artifact is a standalone evolved checker with zero ML/LLM inference overhead and no runtime model dependency. We evolve on the public hardware model checking competition (HWMCC) benchmark and evaluate the generalizability on unseen public and industrial model checking benchmarks, showing that IC3-Evolve can reliably discover practical heuristic improvements under strict correctness gates.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
