IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking

This paper presents IC3-Evolve, an automated offline framework that leverages an LLM to iteratively evolve IC3 hardware model checking heuristics through strictly proof- and witness-gated validation, resulting in a standalone, high-performance checker with zero runtime ML overhead that reliably discovers practical improvements on standard benchmarks.

The Gist

Imagine you are trying to solve a massive, incredibly complex maze. This maze represents a piece of computer hardware (like a microchip). Your goal is to prove that there is no path through the maze that leads to a "trap" (a safety failure). If you find a path to the trap, you need to show exactly how to get there so engineers can fix it.

This is the job of a Model Checker, and the most famous algorithm for doing this is called IC3.

The Problem: The "Tuning" Nightmare

Think of IC3 as a very smart, but slightly stubborn, robot. It knows the rules of the maze, but it has to decide how to explore it. Should it check the left path first? Should it guess? Should it forget old paths to save memory?

These decisions are called heuristics. Currently, human experts have to manually tweak these settings. It's like trying to tune a race car engine by turning tiny screws with a screwdriver while the car is moving. It's slow, expensive, and if you turn one screw too far, the car might crash (the software stops working correctly).

The Solution: IC3-Evolve

The paper introduces IC3-Evolve, a new way to fix this robot. Instead of a human turning the screws, they use an AI (a Large Language Model) to write code patches.

But here is the catch: AI can be hallucinatory or make mistakes. If you just let an AI rewrite the robot's brain, it might break the rules of logic, and the robot might say "I'm safe!" when it's actually in a trap. That would be disastrous for hardware safety.

The Secret Sauce: The "Proof Gate"

This is where the paper gets clever. They don't just let the AI edit the code and hope for the best. They use a Proof-and-Witness Gate.

Think of the AI as a Chef trying to improve a recipe for a cake.

1. The Proposal: The Chef (the AI) suggests a small change: "Let's add a pinch of salt to the frosting."
2. The Gatekeeper: Before anyone eats the cake, a strict Taste-Tester (the Gate) checks two things:
   • If the cake is supposed to be "Safe" (no traps): The Chef must provide a Certificate (a mathematical proof) that the cake is definitely safe. The Gate checks this certificate with a different, independent tool. If the proof doesn't hold up, the cake is thrown away.
   • If the cake is supposed to be "Unsafe" (a trap exists): The Chef must provide a Replayable Trace (a video showing exactly how to get to the trap). The Gate watches the video to make sure the trap is real. If the video is fake or the trap isn't there, the cake is thrown away.

Crucially: The AI is only used in the kitchen (offline) to write the recipe. Once the recipe is approved and the cake is baked, the final product is just a regular cake. You don't need the AI or the Gate to eat it later. This means the final software is fast, cheap, and doesn't need an internet connection or a supercomputer to run.

How They Do It: The "Slot" System

To keep the AI from getting confused, they don't let it rewrite the whole code at once. They use a "Slot-Restricted" approach.

Imagine the robot's brain is a giant control panel with 100 different dials.

• Compass Mode: The AI is only allowed to turn one dial at a time (e.g., "How fast should I check the left path?").
• Jump Mode: If the AI gets stuck, it's allowed to turn two or three dials at once to see if they work better together.

After every change, the Gate checks if the robot still works correctly. If it does, and it's faster, the new setting is kept. If not, it's reverted.

The Results

They tested this on a huge collection of standard hardware puzzles (the HWMCC benchmarks).

• The Result: The AI-evolved robot solved significantly more puzzles and did them much faster than the best human-tuned robots.
• The Surprise: They found that you can't just fix one dial at a time and expect a miracle. The dials are all connected. The AI had to learn how to tweak multiple dials together to get the best performance.

Why This Matters

1. Safety First: Because of the "Proof Gate," we know for a fact the new software is mathematically correct. No "AI hallucinations" allowed.
2. No Runtime Cost: The final software doesn't need the AI running in the background. It's a standalone, super-fast tool.
3. Automation: It automates the tedious job of tuning complex algorithms, freeing up human experts to do more creative work.

In a nutshell: IC3-Evolve is like having an AI mechanic who suggests tiny, specific tweaks to a race car engine. But before any tweak is installed, a strict inspector verifies that the car still follows the laws of physics and can prove it. Once verified, the car runs faster than ever, without needing the mechanic or the inspector to be present during the race.

Technical Summary

1. Problem Statement

Hardware safety model checking is critical for verifying integrated circuits, with IC3 (Property-Directed Reachability, PDR) being the state-of-the-art algorithm. While IC3 is theoretically sound, its practical performance relies heavily on a complex web of heuristics and engineering choices (e.g., clause propagation, generalization strategies, SAT engine interactions).

• The Challenge: Manually tuning these heuristics is costly, brittle, and requires deep domain expertise. Small changes often lead to regressions in other areas, making it difficult to find robust heuristic combinations.
• Limitations of Existing ML Approaches:
  • Learning-Augmented Solvers: Methods like NeuroPDR introduce ML models into the runtime loop, adding inference latency, training costs, and unpredictability, which hinders industrial deployment.
  • LLM-in-the-Loop: Using LLMs to provide hints during verification introduces latency and reproducibility issues.
• The Goal: To automate the discovery of heuristic improvements without compromising the soundness of the checker or introducing runtime ML dependencies.

2. Methodology: IC3-Evolve

The paper proposes IC3-Evolve, an offline framework that treats heuristic engineering as a controlled code evolution process. The core philosophy is to use LLMs only for proposing code changes, while relying on formal verification to validate them.

A. Core Architecture

The system operates as a two-agent closed-loop:

1. Programmer Agent: Proposes small, slot-restricted patches to the IC3 codebase. It is guided by a "knowledge pack" specific to the chosen heuristic slot (e.g., PREDGEN, INDGEN, PUSHCLAUSES).
2. Evaluator Agent: Builds the modified solver, runs benchmarks, and performs rigorous validation.

B. Key Mechanisms

• Slot-Restricted Patch Space: To ensure edits are auditable and interpretable, the LLM is restricted to modifying specific "slots" (subroutines) at a time. This prevents the LLM from making arbitrary, large-scale changes that could break the solver's logic.
• Compass & Jump Search Policy: A lightweight strategy to navigate the search space:
  • Compass Mode: Focuses on the single best-performing heuristic slot based on feedback.
  • Jump Mode: Occasionally explores edits across multiple distinct slots (2–3) to discover synergistic improvements.
• Proof-/Witness-Gated Validation (The "Hard Gate"): This is the most critical contribution. A proposed patch is only accepted if it passes strict soundness checks:
  • SAFE Runs: Must emit a checkable inductive invariant (certificate), verified by an independent tool (CERTIFAIGER).
  • UNSAFE Runs: Must emit a replayable counterexample trace, verified by a simulator (AIGSIM).
  • Result: Any patch that fails these checks is rejected immediately, regardless of performance gains. This ensures the final artifact is sound and standalone.

C. Workflow

1. Select a modification slot (or set) via Compass & Jump.
2. LLM proposes a patch with a hypothesis and fallback plan.
3. Evaluator builds the challenger and runs the Hard Gate (independent proof/witness validation).
4. If sound, the challenger is benchmarked (PAR2, solved count).
5. If it improves performance without regressions, it becomes the new "Champion"; otherwise, the system rolls back and uses the diagnosis to guide the next iteration.

3. Key Contributions

1. Offline LLM-Driven Evolution: A framework that evolves IC3 heuristics via code patches, resulting in a standalone checker with zero runtime ML/LLM overhead.
2. Soundness-Guaranteed via Hard Gates: Introduction of a proof-/witness-gated validation protocol that prevents unsound edits from ever being deployed, solving the reliability issues of previous ML-based approaches.
3. Slot-Restricted Search: A methodology that constrains LLM edits to specific heuristic subroutines, making the evolution process interpretable, auditable, and easier to revert.
4. Compass & Jump Strategy: A search policy that balances local refinement (Compass) with cross-module synergy exploration (Jump).

4. Experimental Results

The framework was evaluated on the HWMCC (Hardware Model Checking Competition) benchmarks and unseen industrial benchmarks.

• Performance Gains:
  • Starting from IC3ref (PAR2 ~1050s), IC3-Evolve achieved a PAR2 of 490.67s on the evolution set and 464.56s on unseen HWMCC Set B.
  • It solved 92/100 instances on Set A and 94/100 on Set B, significantly outperforming strong baselines like rIC3 (the recent HWMCC winner) and ABC.
  • On industrial benchmarks, it solved 225/302 instances with a PAR2 of 1044.26s, outperforming all baselines.
• Ablation Studies:
  • Necessity of Hard Gates: A counterfactual experiment showed that a patch improving performance by +9 solved instances was rejected because it failed witness validation. This proves the gate prevents "unsound improvements."
  • Cross-Slot Synergy: Single-slot evolution yielded marginal gains. Naively combining the best single-slot edits (Naive-Compose) still fell far short of the full IC3-Evolve champion. This demonstrates that IC3 heuristics are tightly coupled and require coordinated, feedback-driven evolution.

5. Significance

• Industrial Viability: Unlike learning-augmented solvers, IC3-Evolve produces a traditional C++ binary with no runtime dependencies on LLMs or GPUs, making it immediately deployable in production EDA flows.
• Reliability: By enforcing formal proof and witness checks, the framework guarantees that the evolved solver remains mathematically sound, addressing the "black box" fear associated with AI-driven code generation.
• New Paradigm for EDA: The paper demonstrates that "offline code evolution" guided by LLMs, but constrained by formal verification gates, is a viable and superior path for optimizing complex verification algorithms compared to online ML inference or manual tuning.

In summary, IC3-Evolve successfully bridges the gap between the adaptability of LLMs and the rigor of formal verification, delivering a high-performance, sound, and deployable hardware model checker.