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

Dit paper introduceert IC3-Evolve, een automatisch framework dat een LLM gebruikt om offline, onder strikte correctheidsgaranties, heuristieken voor hardware-modelchecking te optimaliseren, wat resulteert in een zelfstandige, verbeterde checker zonder runtime-ML-overhead.

De kern

Stel je voor dat je een gigantische, ingewikkelde machine bouwt, zoals een moderne auto of een chip voor een smartphone. Voordat je deze machine in productie neemt, moet je er 100% zeker van zijn dat hij nooit in een "dodelijke" staat terechtkomt (bijvoorbeeld een rem die niet werkt).

Vroeger testten ingenieurs dit door de machine te laten rijden in miljoenen scenario's (simulatie). Maar moderne machines zijn zo complex dat je niet alle mogelijke scenario's kunt testen. Daarom gebruiken ze wiskundige bewijzen om te zeggen: "We hebben bewezen dat deze machine nooit in een slechte staat kan komen."

Het algoritme dat dit doet, heet IC3. Het is als een supersterke detective die een bewijsstuk zoekt.

Het Probleem: De Detective is Slim, maar Stug

Deze detective (IC3) werkt heel goed, maar hij heeft een probleem: hij is erg afhankelijk van "heuristieken". Dat zijn kleine, handmatige regels die de detective gebruikt om slim te zoeken.

• Vergelijking: Stel je voor dat de detective een enorme bibliotheek moet doorzoeken. De heuristieken zijn de regels die zeggen: "Zoek eerst in de rode boeken" of "Spring over de boeken met een blauwe kaft".
• Het probleem is dat ingenieurs deze regels met de hand moeten instellen. Als ze één regel veranderen, kan het zijn dat de detective sneller is op het ene boek, maar trager op het andere. Het is een lastig, tijdrovend en kwetsbaar proces om de perfecte combinatie van regels te vinden.

De Oplossing: IC3-Evolve (De Slimme Architect)

De auteurs van dit paper hebben IC3-Evolve bedacht. In plaats van dat mensen handmatig proberen de regels te verbeteren, laten ze een AI (een Large Language Model) de code van de detective herschrijven.

Maar hier is de magische truc: ze laten de AI niet zomaar doen wat hij wil. Ze gebruiken een streng controlesysteem.

1. De "Slot" Methode (De Bouwvakker)

Stel je voor dat de detective een huis is. De AI mag niet het hele huis slopen en herbouwen. De AI krijgt slechts één klein "slot" (een raam, een deur, een muur) om aan te werken.

• De AI zegt: "Ik ga dit ene raam (een regel in de code) iets anders maken om het huis veiliger of sneller te maken."
• Dit maakt het makkelijk om te controleren wat er precies verandert.

2. De "Bewijs- en Getuige" Poort (De Onverbiddelijke Keurmeester)

Dit is het belangrijkste deel. Elke keer als de AI een nieuwe versie van de detective voorstelt, moet deze versie bewijzen dat hij nog steeds correct werkt. Er zijn twee soorten tests:

• Als de detective zegt "VEILIG" (SAFE): Hij moet een certificaat tonen. Een onafhankelijke keurmeester kijkt dit certificaat na. Als het certificaat niet klopt, wordt de nieuwe versie direct afgekeurd.

• Als de detective zegt "ONVEILIG" (UNSAFE): Hij moet een spoor (een getuige) laten zien. Een simulator speelt dit spoor na. Als het spoor niet klopt, is de nieuwe versie afgekeurd.

• Analogie: Het is alsof je een nieuwe auto ontwerpt. Je mag hem alleen op de markt brengen als hij een onafhankelijke crash-test haalt én een onafhankelijke remtest. Als hij faalt, mag hij niet de fabriek uit, hoe snel hij ook is.

3. De Resultaten: Een Zelfstandige Super-Detective

De AI werkt alleen in de "achtergrond" (offline). Zodra de AI een verbetering heeft gevonden en deze is goedgekeurd door de keurmeesters, wordt de nieuwe code vastgezet.

• Het resultaat: Je krijgt een nieuwe, snellere detective.
• Het grote voordeel: De AI is niet meer nodig om de detective te laten werken. De nieuwe detective werkt volledig zelfstandig, zonder dat er een AI in de lucht moet hangen om te helpen. Dit maakt het snel, betrouwbaar en goedkoop voor gebruik in de echte industrie.

Wat hebben ze ontdekt?

Ze hebben getoond dat deze methode werkt. De nieuwe detective (IC3-Evolve) is veel sneller dan de oude versies en lost veel meer problemen op.

• Ze ontdekten ook dat je niet zomaar één ding kunt verbeteren. Je moet verschillende kleine onderdelen (ramen, deuren, muren) samen optimaliseren. Als je maar één ding aanpast, helpt het niet genoeg. De AI moet slim combineren.

Samenvatting in één zin

IC3-Evolve is een systeem waarbij een AI als een slimme architect kleine, gecontroleerde verbeteringen aanbrengt aan een bewijs-algoritme, maar elke verbetering wordt streng getoetst door onafhankelijke keurmeesters voordat hij mag worden gebruikt, zodat we aan het einde een snellere, betrouwbaardere en volledig zelfstandige "detective" hebben.

Technische samenvatting

Probleemstelling

Hardware veiligheidsmodelchecking is essentieel voor de verificatie van complexe geïntegreerde schakelingen. De IC3-algoritme (ook bekend als Property-Directed Reachability of PDR) is de de facto standaard voor dit doel. IC3 bepaalt of een systeem een veiligheids eigenschap schendt (UNSAFE) of niet (SAFE), en levert respectievelijk een reproduceerbare tegenvoorbeeldtrace of een controleerbare inductieve invariant als bewijs.

Hoewel IC3 een robuust algoritmisch raamwerk biedt, wordt de praktische prestatie gedomineerd door een complex web van heuristieken en implementatiekeuzes (zoals generalisatie, clausule-propagatie en interacties met SAT-oplossers). Het handmatig tunen van deze heuristieken is:

• Kostbaar en broos: Kleine wijzigingen vereisen het opnieuw draaien van grote benchmark suites en kunnen regressies op andere probleemklassen veroorzaken.
• Moeilijk te reproduceren: Het vereist diepgaande domeinkennis.
• Beperkt door ML-integratie: Bestaande "learning-augmented" benaderingen (zoals NeuroPDR) introduceren trainings- en inferentiekosten, wat leidt tot onvoorspelbare latentie en maakt ze minder geschikt voor industriële productieomgevingen.

Methodologie: IC3-Evolve

Het paper introduceert IC3-Evolve, een geautomatiseerd, offline framework dat Large Language Models (LLMs) gebruikt om de heuristieken van een IC3-implementatie te evolueren via code-aanpassingen. Het centrale idee is om LLM's te gebruiken voor code-evolutie in plaats van voor runtime-inferentie.

De kerncomponenten van de methodologie zijn:

1. Offline Code-Evolutie:

   • Het LLM (GPT-5-Codex) fungeert als een "programmer agent" die kleine, beperkte patches (aanpassingen) voorstelt voor een IC3-codebase.
   • De LLM wordt niet gebruikt tijdens de verificatie zelf. Het resultaat is een standalone checker zonder ML-afhankelijkheid of runtime-overhead.

2. Slot-Beperkte Patchruimte:

   • Om controleerbaarheid te garanderen, wordt de code opgedeeld in specifieke "slots" die corresponderen met de belangrijkste heuristische onderdelen van IC3 (bijv. BLOCKPROOFOBLIGATIONS, INDGEN, PREDGEN, PUSHCLAUSES).
   • Per iteratie wordt de agent beperkt tot het wijzigen van één of een klein aantal slots, wat de wijzigingen lokaal en interpreteerbaar houdt.

3. Compass & Jump Zoekstrategie:

   • Een zoekbeleid dat bepaalt welke slots worden aangepakt.
   • Compass: Richt zich op de beste enkele beweging (slot) gebaseerd op eerdere feedback.
   • Jump: Springt naar meerdere slots tegelijk om synergieën tussen verschillende heuristieken te ontdekken.

4. Proof-/Witness-Gated Validatie (Kerninnovatie):

   • Dit is het strengste veiligheidsmechanisme. Een voorgestelde patch wordt alleen geaccepteerd als hij door een "harde check" komt:
     • SAFE runs: Moeten een inductieve invariant (bewijs) genereren die onafhankelijk wordt geverifieerd door een tool zoals CERTIFAIGER.
     • UNSAFE runs: Moeten een reproduceerbare tegenvoorbeeldtrace genereren die wordt nagebootst door een simulator (bijv. AIGSIM).
   • Als een patch geen geldig bewijs of trace levert, wordt deze direct verworpen, ongeacht de prestatieverbetering. Dit garandeert dat de evolutie de geluidheid (soundness) van de IC3-algoritme nooit schendt.

5. Twee-Agent Cyclus:

   • Programmer Agent: Stelt een patch voor met een hypothese en een fallback-plan.
   • Evaluator Agent: Bouwt de challenger, voert de harde validatie uit, benchmarkt de prestaties (PAR2-score) en genereert een diagnose ("MoveSet") om de volgende iteratie te sturen.

Belangrijkste Bijdragen

• IC3-Evolve Framework: Een nieuw paradigma voor het automatisch verbeteren van modelcheckers via offline code-evolutie, waarbij de LLM alleen gebruikt wordt voor het genereren van patches, niet voor runtime-beslissingen.
• Gecertificeerde Evolutie: Het introduceren van een "proof-/witness-gated" validatielaag die onjuiste wijzigingen uitsluit voordat ze worden geïntegreerd.
• Zoekstrategie: De "Compass & Jump" methode om zowel lokale optimalisaties als cross-module synergieën te ontdekken binnen een beperkte code-ruimte.
• Empirisch Bewijs: Demonstratie dat dit framework praktische heuristische verbeteringen kan vinden die de prestaties aanzienlijk verhogen zonder de correctheid te compromitteren.

Resultaten

De auteurs evalueerden IC3-Evolve op de HWMCC (Hardware Model Checking Competition) benchmarks en industriële datasets.

• Prestatieverbetering:

  • Op de HWMCC benchmarks (Set A en Set B) verbeterde IC3-Evolve de PAR2-score (gewichtsd gemiddelde oplostijd) drastisch ten opzichte van de basislijn (IC3ref) en sterke concurrenten zoals rIC3 en ABC.
  • Voorbeeld: Op HWMCC Set B bereikte IC3-Evolve een PAR2 van 464.56s en loste 94/100 gevallen op, vergeleken met 639.61s en 86/100 voor de sterke baseline rIC3-CaDiCaL.
  • Op industriële benchmarks (302 instances) loste IC3-Evolve 225/302 gevallen op met een PAR2 van 1044.26s, wat significant beter is dan de concurrentie.

• Ablatie Studies:

  • Validatie is cruciaal: Een contrafactueel experiment toonde aan dat een patch die prestatieverbetering bood, werd afgewezen omdat het geen geldig bewijs leverde. Zonder deze "gate" zou een onjuiste oplossing de champion zijn geworden.
  • Synergie is noodzakelijk: Evolutie die beperkt bleef tot één enkele slot (bijv. alleen PUSHCLAUSES) leverde slechts marginale verbeteringen. De volledige kracht van IC3-Evolve kwam voort uit de gecoördineerde evolutie over meerdere slots, wat aantoont dat IC3-heuristieken sterk met elkaar verbonden zijn.

Betekenis en Conclusie

IC3-Evolve biedt een unieke oplossing voor het dilemma tussen geavanceerde AI en industriële betrouwbaarheid in de EDA (Electronic Design Automation).

• Betrouwbaarheid: Door de LLM offline te houden en streng te valideren via formele bewijzen, ontstaat er een product dat volledig betrouwbaar is en geen runtime-afhankelijkheid heeft van ML-modellen.
• Efficiëntie: Het framework slaagt erin om complexe, menselijke heuristische engineering te automatiseren en te verbeteren, wat leidt tot snellere en robuustere modelcheckers.
• Toekomstperspectief: Het paper suggereert dat bewijsproducerende verificatie een ideaal testbed is voor evaluator-gedreven LLM-code-evolutie, met potentie voor uitbreiding naar bredere code-ruimtes terwijl de auditbaarheid behouden blijft.

Kortom, IC3-Evolve bewijst dat LLM's effectief kunnen worden ingezet om de kernalgoritmen van hardwareverificatie te optimaliseren, zolang de validatie strikt gebaseerd blijft op formele correctheid en niet op statistische prestaties alleen.