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

Die Arbeit stellt IC3-Evolve vor, ein automatisiertes Offline-Framework, das mittels eines LLMs überprüfbare Heuristik-Verbesserungen für den IC3-Hardware-Modellprüfer entwickelt, indem es jeden Kandidatenpatch strikt durch proof- und witness-gated Validierung sichert, um ein fehlerfreies, lauffähiges Ergebnis ohne Laufzeit-ML-Abhängigkeit zu gewährleisten.

Das Wesentliche

Stell dir vor, du hast einen extrem intelligenten, aber manchmal etwas sturen Wächter (einen Computer-Algorithmus namens IC3). Seine Aufgabe ist es, sicherzustellen, dass eine komplexe Maschine (wie ein neuer Computerchip) niemals in einen katastrophalen Zustand gerät – zum Beispiel, dass sie sich selbst zerstört oder Daten verliert.

Der Wächter prüft jede mögliche Bewegung der Maschine. Wenn er einen Fehler findet, sagt er: „Achtung, hier ist ein Unfall!" (UNSAFE). Wenn er alles geprüft hat und keine Gefahr sieht, sagt er: „Alles sicher!" (SAFE) und liefert einen unanfechtbaren Beweis dafür.

Das Problem ist: Dieser Wächter ist zwar schlau, aber er ist nicht perfekt. Er hat viele kleine „Knöpfe" und „Hebel" (Heuristiken), die bestimmen, wie er sucht. Wenn man diese Knöpfe falsch stellt, wird er langsam oder findet Fehler nicht. Bisher mussten menschliche Experten diese Knöpfe mühsam per Hand justieren – ein Prozess, der Jahre dauert und bei dem man leicht einen anderen Hebel versehentlich kaputt macht.

Die Lösung: IC3-Evolve (Der KI-Handwerker)

Die Forscher haben IC3-Evolve entwickelt. Stell dir das wie einen automatisierten Handwerker, der den Wächter verbessert, aber mit einer sehr strengen Sicherheitsregel.

Hier ist die einfache Erklärung, wie das funktioniert, mit ein paar Analogien:

1. Der Handwerker und die „Slot"-Regel

Stell dir den Code des Wächters als ein riesiges Haus vor. Normalerweise würde ein Handwerker versuchen, das ganze Haus auf einmal umzubauen. Das ist gefährlich und chaotisch.
IC3-Evolve nutzt eine KI (ein Large Language Model), die wie ein sehr geschickter Architekt ist. Aber dieser Architekt darf nicht das ganze Haus neu bauen. Er darf nur ein oder zwei kleine Räume (die sogenannten „Slots") gleichzeitig renovieren.

• Beispiel: Er darf nur die Küche (die „Küche" ist ein Teil des Programms, der prüft, ob ein Fehler vorhergesagt werden kann) oder nur das Treppenhaus (der Teil, der neue Informationen weitergibt) anpassen.

2. Die „Proof-/Witness"-Tür (Der strenge Türsteher)

Das ist der wichtigste Teil. Wenn der KI-Architekt einen neuen Entwurf für die Küche macht, darf er ihn nicht einfach sofort einbauen.
Er muss den Entwurf durch eine magische Tür schicken, die nur zwei Dinge akzeptiert:

• Wenn der Wächter sagt „Sicher": Er muss einen Beweis (eine Art Bauplan) liefern, der von einem anderen, völlig unabhängigen Prüfer bestätigt wird. Wenn der Plan nicht stimmt, wird der Entwurf sofort verworfen.
• Wenn der Wächter sagt „Gefahr": Er muss eine Reisekarte (eine Spur) liefern, die zeigt, wie man genau zu dem Fehler gelangt ist. Man muss diese Karte nachspielen können, um zu sehen, ob sie wirklich stimmt.

Die Analogie: Stell dir vor, du baust ein neues Auto. Bevor du es auf die Straße bringst, musst du beweisen, dass es bei einem Crashtest nicht explodiert (Beweis) ODER du musst zeigen, genau wie man in den Graben fährt, wenn man den Bremshebel falsch zieht (Reisekarte). Wenn du das nicht kannst, darfst du das Auto nicht bauen. Das verhindert, dass die KI „schlechte" Ideen einbaut, die nur schnell aussehen, aber unsicher sind.

3. Offline-Training (Keine KI im Auto)

Sobald die KI einen guten Entwurf gefunden und durch die Tür bestanden hat, wird er in den Code des Wächters eingebaut.
Wichtig: Die KI verschwindet danach wieder. Das fertige Produkt ist ein eigenständiger, super-schneller Wächter, der keine KI mehr braucht, um zu arbeiten. Er ist wie ein Sportwagen, der im Training von einem Trainer (der KI) optimiert wurde, aber beim Rennen fährt er ganz allein, ohne dass der Trainer im Beifahrersitz sitzt. Das macht ihn extrem schnell und zuverlässig.

Was hat das gebracht?

Die Forscher haben diesen Prozess auf öffentlichen und industriellen Testaufgaben laufen lassen.

• Das Ergebnis: Der so verbesserte Wächter war deutlich schneller und fand mehr Fehler als die besten menschlich optimierten Versionen.
• Die Lektion: Es reichte nicht, nur einen Knopf zu drücken. Die KI musste lernen, wie verschiedene Räume des Hauses zusammenarbeiten (z. B. wie die Küche mit dem Treppenhaus interagiert). Wenn man nur isoliert an einem Teil schraubt, bringt das wenig. Erst die Kombination aus vielen kleinen, geprüften Verbesserungen macht den Wächter zum Champion.

Zusammenfassung in einem Satz

IC3-Evolve ist wie ein KI-Architekt, der nachts an einem Sicherheitswächter arbeitet, aber nur kleine, getestete Änderungen vornimmt und jede Änderung erst dann einbaut, wenn ein unabhängiger Prüfer garantiert hat, dass sie sicher ist – am Ende bleibt ein schneller, KI-freier Wächter übrig, der alles perfekt macht.

Technische Zusammenfassung

1. Problemstellung

Das Hardware-Sicherheits-Modell-Checking (Formal Verification) ist ein Eckpfeiler der modernen Hardware-Verifikation, da Simulationen bei komplexen integrierten Schaltungen oft nicht ausreichen, um tiefgreifende Randfälle zu testen. Der IC3-Algorithmus (auch bekannt als Property-Directed Reachability, PDR) ist der aktuelle Standard für diese Aufgabe. Er entscheidet, ob ein System eine Sicherheitseigenschaft erfüllt, und liefert entweder einen UNSAFE-Beweis (mit einem replizierbaren Gegenbeispiel) oder einen SAFE-Beweis (mit einer überprüfbaren induktiven Invariante).

Das Hauptproblem liegt jedoch in der praktischen Leistungsfähigkeit von IC3-Implementierungen. Diese hängt nicht primär vom Kernalgorithmus ab, sondern von einem komplexen Netz aus Heuristiken und Implementierungsentscheidungen (z. B. Generalisierung, Klausel-Propagation, Interaktion mit SAT-Solvern).

• Manuelle Optimierung ist kostspielig und fragil: Kleine Änderungen erfordern das Neudurchlaufen großer Benchmark-Suiten. Verbesserungen in einem Bereich führen oft zu Regressionen in anderen.
• Limitationen bestehender ML-Ansätze: Lernbasierte Ansätze (z. B. NeuroPDR, DeepIC3) oder LLMs, die zur Laufzeit Hinweise geben, führen zu Laufzeit-Overhead, Latenz und Problemen mit der Reproduzierbarkeit. Zudem sind sie oft nicht robust genug für industrielle Workloads.

2. Methodik: IC3-Evolve

Das Paper stellt IC3-Evolve vor, ein offline arbeitendes Framework, das Large Language Models (LLMs) nutzt, um den IC3-Code durch kontrollierte Evolution zu verbessern, ohne die Laufzeitabhängigkeit von ML-Modellen.

Kernprinzipien

1. Offline Code-Evolution: Das LLM wird nur während des Trainingsprozesses (Offline) verwendet, um Patches vorzuschlagen. Das resultierende Werkzeug ist ein eigenständiger, optimierter Checker ohne ML-Overhead zur Laufzeit.
2. Slot-Restriktierte Patches: Der Code wird nicht willkürlich geändert. Stattdessen werden spezifische „Slots" (Heuristik-Parameterbereiche) definiert, die den wichtigsten IC3-Subroutinen entsprechen (z. B. BLOCKPROOFOBLIGATIONS, INDGEN, PREDGEN, PUSHCLAUSES). Das LLM darf nur innerhalb dieser Slots Änderungen vorschlagen, was die Änderungen interpretierbar und auditierbar macht.
3. Proof-/Witness-Gated Validation (Der entscheidende Sicherheitsmechanismus):
   • Jeder vorgeschlagene Patch (Challenger) wird nur dann akzeptiert, wenn er strenge Korrektheitsprüfungen besteht.
   • SAFE-Läufe: Müssen eine überprüfbare induktive Invariante (Proof) ausgeben, die unabhängig verifiziert wird (z. B. mit CERTIFAIGER).
   • UNSAFE-Läufe: Müssen einen replizierbaren Gegenbeispiel-Trace (Witness) ausgeben, der durch Simulation bestätigt wird (z. B. mit AIGSIM).
   • Fällt ein Lauf durch diese „Tore" (Gates), wird der Patch verworfen, unabhängig von seiner Geschwindigkeit. Dies verhindert das Deployen unsounder (fehlerhafter) Änderungen.

Der Evolutions-Workflow (Compass & Jump)

Das System nutzt einen Zwei-Agenten-Ansatz (Programmierer-Agent und Evaluierer-Agent) in einer geschlossenen Schleife:

• Compass-Modus: Wählt den besten einzelnen Heuristik-Slot basierend auf Feedback aus.
• Jump-Modus: Erlaubt Änderungen in mehreren Slots gleichzeitig, um Synergien zu entdecken.
• Der Evaluierer generiert ein MoveSet (eine priorisierte Liste von Empfehlungen), das den Programmier-Agenten für die nächste Iteration steuert.

3. Hauptbeiträge

1. IC3-Evolve Framework: Ein automatisiertes, offline arbeitendes System zur Evolution von IC3-Heuristiken durch slot-restriktierte, auditierbare Code-Patches.
2. Proof-/Witness-Gated Validierung: Ein strikter Mechanismus, der sicherstellt, dass nur korrekte Änderungen in den Champion-Code übernommen werden, was die Zuverlässigkeit der Evolution garantiert.
3. Suchstrategie (Compass & Jump): Eine leichte Suchpolitik, die zwischen lokalen Verfeinerungen und cross-modularen Änderungen balanciert, um komplexe Heuristik-Kombinationen zu finden.
4. Nachweis praktischer Verbesserungen: Die Evolution führt zu einem eigenständigen Checker, der auf öffentlichen und industriellen Benchmarks signifikante Leistungssteigerungen erzielt, ohne ML-Abhängigkeit zur Laufzeit.

4. Ergebnisse

Die Evaluation erfolgte auf dem HWMCC (Hardware Model Checking Competition) Benchmark und industriellen Datensätzen.

• Leistungssteigerung: IC3-Evolve übertrifft starke Baselines (einschließlich IC3ref, ABC und dem aktuellen Gewinner rIC3) deutlich.
  • Auf dem HWMCC-Set B (ungesehen während des Trainings) löste IC3-Evolve 94 von 100 Instanzen mit einem PAR2-Wert von 464,56 s.
  • Zum Vergleich: Der starke Baseline rIC3-CaDiCaL löste 89 Instanzen mit einem PAR2 von 524,35 s.
  • Auf industriellen Benchmarks löste IC3-Evolve 225 von 302 Instanzen (PAR2: 1044,26 s), während rIC3-CaDiCaL nur 182 löste (PAR2: 1449,78 s).
• Ablationsstudien:
  • Notwendigkeit der Gates: Ohne die Proof-/Witness-Gates wären unsounde „Verbesserungen" akzeptiert worden, die die Korrektheit des Systems gefährdet hätten.
  • Komplexität der Heuristiken: Isolierte Optimierung einzelner Slots (z. B. nur PUSHCLAUSES) führte zu marginalen oder instabilen Gewinnen. Die Kombination von Änderungen über mehrere Slots hinweg (Cross-Slot-Evolution) war entscheidend für den großen Erfolg. Dies zeigt, dass IC3-Heuristiken stark gekoppelt sind und koordinierte Anpassungen erfordern.

5. Bedeutung und Ausblick

Das Paper demonstriert, dass LLM-gesteuerte Code-Evolution in Kombination mit formalen Korrektheitsgarantien ein vielversprechender Weg zur Automatisierung von Heuristik-Engineering ist.

• Paradigmenwechsel: Statt ML-Modelle in die Laufzeit-Schleife zu integrieren (was Latenz und Variabilität erhöht), wird das LLM genutzt, um einen besseren, statischen Algorithmus zu „erfinden".
• Vertrauenswürdigkeit: Durch die Proof-/Witness-Gates wird sichergestellt, dass das Ergebnis mathematisch verifizierbar und sicher ist.
• Industrielle Relevanz: Die Ergebnisse zeigen, dass diese Methode nicht nur auf akademischen Benchmarks, sondern auch auf realen industriellen Problemen signifikante Verbesserungen bringt.

Zukünftige Arbeiten könnten den Suchraum erweitern, während die Auditierbarkeit und die Kontrolle über Regressionen beibehalten werden. IC3-Evolve etabliert somit einen neuen Standard für die sichere und effektive Automatisierung von Formal-Verification-Tools.