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

Il paper presenta IC3-Evolve, un framework offline che utilizza un LLM per evolvere automaticamente e in modo sicuro le euristiche dell'algoritmo IC3 per la verifica di modelli hardware, garantendo la correttezza delle modifiche attraverso validazioni basate su certificati di sicurezza o tracce di controesempio, producendo così un verificatore autonomo e performante privo di dipendenze da modelli ML a runtime.

L'essenziale

Immagina di dover costruire un ponte che deve essere assolutamente sicuro. Non puoi permetterti nemmeno un singolo errore, perché se crolla, le conseguenze sono disastrose. Nel mondo dell'ingegneria dei computer, questo "ponte" è un circuito elettronico (come quello dentro il tuo smartphone o un'auto a guida autonoma), e il compito di verificarne la sicurezza spetta a un algoritmo chiamato IC3.

IC3 è come un ispettore di sicurezza super-preciso. Il suo lavoro è controllare se il ponte può mai crollare (stato "pericoloso"). Se trova un difetto, ti mostra esattamente come crollerebbe (un "esempio di errore"). Se non trova difetti, ti consegna un certificato matematico che dice: "È sicuro al 100%".

Il Problema: L'Ispettore è un po' "testardo"

Il problema è che IC3, anche se è un genio, ha bisogno di essere guidato da un capo cantiere (gli "euristici"). Questo capo decide come ispezionare il ponte: da dove iniziare, quanto velocemente muoversi, quali strumenti usare.
Attualmente, scegliere il capo cantiere perfetto è un incubo. Gli ingegneri umani devono provare migliaia di combinazioni diverse, e spesso un piccolo cambiamento che aiuta su un tipo di ponte ne rovina un altro. È come cercare di indovinare la ricetta perfetta per una torta provando ingredienti a caso: ci vuole tempo, costa molto e il risultato è fragile.

La Soluzione: IC3-Evolve (Il "Chef" Robot che non mangia mai)

Gli autori di questo paper hanno creato IC3-Evolve, un sistema che usa l'Intelligenza Artificiale (un LLM, come un modello linguistico avanzato) per diventare quel capo cantiere perfetto. Ma c'è un trucco fondamentale: l'AI lavora solo "fuori dal campo" (offline).

Ecco come funziona, con una metafora culinaria:

1. Il Laboratorio di Cucina (Offline):
   Immagina un cuoco robot (l'AI) che sta in una cucina segreta. Il suo compito è modificare leggermente la ricetta di base del nostro ispettore IC3. Il cuoco dice: "Proviamo a togliere un po' di sale" o "Aggiungiamo un pizzico di pepe".

   • La Regola d'Oro: Il cuoco non può toccare la struttura fondamentale della ricetta (la logica matematica deve rimanere intatta), può solo modificare piccoli dettagli (i "slot" o le manopole di controllo).

2. Il Controllo di Qualità (Il "Gated" o Cancello):
   Ogni volta che il cuoco propone una nuova versione della ricetta, questa viene portata in una stanza di prova separata. Qui, due guardie del corpo molto severe controllano tutto:

   • Se la ricetta dice "Il ponte è sicuro", deve produrre un certificato che un altro computer indipendente può verificare.
   • Se la ricetta dice "Il ponte è pericoloso", deve mostrare un video (traccia) che dimostra esattamente come crolla.
   • Se il certificato è falso o il video non torna? La ricetta viene buttata via immediatamente. Non importa se sembra più veloce o migliore: se non è sicura al 100%, non passa. Questo è il "Proof-/Witness-Gated" (Cancello basato su prove e testimonianze).

3. Il Risultato Finale (Il Piatto Pronto):
   Dopo centinaia di tentativi nel laboratorio segreto, il sistema trova la ricetta perfetta. Il risultato finale è un nuovo ispettore IC3 che è stato "allenato" dall'AI, ma che non ha più bisogno dell'AI per funzionare.

   • Quando questo nuovo ispettore va a lavorare sul ponte reale, è veloce, silenzioso e non consuma energia per pensare all'AI. È un software autonomo e perfetto.

Perché è rivoluzionario?

Prima, per usare l'AI in questo campo, bisognava farla lavorare mentre l'ispettore controllava il ponte. Era come avere un assistente che ti urlava le istruzioni mentre guidavi: lento, costoso e imprevedibile.
Con IC3-Evolve:

• Nessun costo extra: L'AI non è presente quando il software lavora.
• Sicurezza assoluta: Nessun cambiamento è stato accettato senza una prova matematica che non ha rotto nulla.
• Miglioramenti reali: Testato su circuiti industriali reali, questo nuovo ispettore ha risolto molti più problemi e molto più velocemente dei migliori ispettori esistenti, trovando combinazioni di "ingredienti" che nessun umano avrebbe mai osato provare.

In sintesi

IC3-Evolve è come un allenatore di calcio che studia le partite, prova migliaia di tattiche diverse in allenamento (offline), e quando trova quella vincente, la insegna alla squadra. La squadra poi scende in campo e gioca da sola, senza l'allenatore, ma con la tattica perfetta che ha imparato, garantendo che non commetteranno mai errori di regolamento (sicurezza) e che vinceranno più partite (prestazioni).

Sommario tecnico

1. Il Problema

Il Model Checking Hardware è fondamentale per la verifica formale dei circuiti integrati, ma la complessità crescente degli spazi degli stati rende l'analisi esaustiva difficile. L'algoritmo IC3 (noto anche come Property-Directed Reachability o PDR) è lo standard industriale per la verifica di sicurezza, in quanto è in grado di produrre prove formali (invarianti induttivi per "SAFE" o tracce di controesempio per "UNSAFE").

Tuttavia, le prestazioni pratiche di IC3 dipendono criticamente da una rete complessa di euristiche e scelte implementative (es. generalizzazione, propagazione delle clausole, interazione con i motori SAT).

• Limitazioni attuali: L'ottimizzazione manuale di queste euristiche è costosa, fragile e difficile da riprodurre. Piccoli cambiamenti possono migliorare le prestazioni su un insieme di istanze ma causare regressioni su altre.
• Sfide dell'IA: Gli approcci precedenti che integrano modelli di Machine Learning (ML) direttamente nel ciclo di esecuzione (runtime) introducono costi di inferenza, latenza e problemi di robustezza, rendendoli poco adatti ai flussi di produzione industriale. Inoltre, l'uso di LLM in tempo reale solleva preoccupazioni su latenza e riproducibilità.

2. Metodologia: IC3-Evolve

Il paper propone IC3-Evolve, un framework offline che utilizza un Large Language Model (LLM) per evolvere il codice sorgente di un solver IC3, garantendo la correttezza formale attraverso un rigoroso processo di validazione.

Architettura e Flusso di Lavoro

Il sistema opera in un ciclo chiuso a due agenti, orchestrato da una politica di ricerca chiamata Compass & Jump:

1. Agente Programmatore: Propone patch di codice limitate a "slot" specifici (es. gestione degli obblighi di prova, generalizzazione induttiva, propagazione). Ogni proposta include un'ipotesi sull'impatto e un piano di fallback.
2. Agente Valutatore: Compila il codice modificato, esegue i benchmark e, crucialmente, applica la validazione tramite Proof-/Witness-Gating.
3. Politica Compass & Jump: Guida la ricerca selezionando quali "slot" modificare. In modalità "Compass", si concentra sul singolo miglioramento migliore; in modalità "Jump", esplora sinergie tra più slot diversi.

Il Meccanismo Chiave: Proof-/Witness-Gated Validation

Questa è la componente più innovativa per garantire la sicurezza. Un candidato patch viene accettato solo se:

• Caso SAFE: Il solver produce un certificato (invariante induttivo) che viene verificato indipendentemente da un tool esterno (es. CERTIFAIGER).
• Caso UNSAFE: Il solver produce una traccia di controesempio che viene riprodotta e validata da un simulatore (es. AIGSIM).
• Rigetto: Se manca il certificato, la traccia non è riproducibile o c'è una discrepanza, la patch viene scartata immediatamente, indipendentemente dalle prestazioni di velocità. Questo impedisce l'adozione di modifiche "non sonore" (unsound).

Spazio di Ricerca Slot-Restricted

Per rendere l'evoluzione controllabile e auditabile, il codice IC3 è diviso in slot euristici (es. BLOCKPROOFOBLIGATIONS, INDGEN, PUSHCLAUSES). L'LLM può modificare solo un sottoinsieme ristretto di file/funzioni alla volta, riducendo il rumore di contesto e facilitando la reversibilità delle modifiche.

3. Contributi Chiave

1. Framework IC3-Evolve: Un sistema offline che evolve le euristiche IC3 tramite modifiche al codice auditable, producendo un solver standalone senza dipendenze da modelli ML a runtime.
2. Validazione Gated: Un protocollo di sicurezza che garantisce che ogni miglioramento sia formalmente corretto prima di essere promosso, eliminando il rischio di regressioni di correttezza.
3. Strategia Compass & Jump: Una politica di ricerca che bilancia l'ottimizzazione locale (un singolo slot) con l'esplorazione di sinergie cross-modulo.
4. Workflow di Evoluzione: Un processo iterativo che combina proposte di codice, validazione rigorosa e diagnosi guidata per guidare l'evoluzione successiva.

4. Risultati Sperimentali

Gli esperimenti sono stati condotti sul benchmark pubblico HWMCC (Hardware Model Checking Competition) e su un set di istanze industriali.

• Setup: Partendo da IC3ref (una versione base), il sistema ha eseguito 200 iterazioni di evoluzione offline.
• Prestazioni:
  • Su un set di test HWMCC non visto durante l'addestramento, IC3-Evolve ha risolto 94 istanze su 100, con un tempo PAR2 (metrica di performance) di 464.56s.
  • Confronto con i Baseline: Ha superato significativamente le versioni base di IC3ref, ABC e persino rIC3-CaDiCaL (l'attuale vincitore HWMCC'24/25), riducendo il PAR2 da ~524s a ~464s e aumentando il numero di istanze risolte.
  • Su benchmark industriali (302 istanze), ha risolto 225 istanze con un PAR2 di 1044.26s, superando tutti i baseline.
• Studi di Ablazione:
  • L'evoluzione su un singolo slot alla volta ha prodotto miglioramenti marginali e instabili.
  • La composizione "naive" delle migliori patch singole non ha raggiunto le prestazioni del sistema completo, dimostrando che le euristiche IC3 sono fortemente accoppiate e richiedono un'evoluzione coordinata e cross-slot.
  • Controfattuale: Un'ipotetica patch che avrebbe migliorato le prestazioni ma fallito la validazione del "witness" è stata correttamente rifiutata, dimostrando l'efficacia del gate di sicurezza.

5. Significato e Impatto

IC3-Evolve rappresenta un cambio di paradigma nella verifica formale assistita da AI:

• Sicurezza e Affidabilità: Dimostra che è possibile utilizzare LLM per l'ottimizzazione algoritmica senza compromettere la correttezza formale, grazie alla validazione offline rigorosa.
• Deploy Industriale: Il risultato finale è un solver C++ standalone. Non ci sono costi di inferenza ML a runtime, né dipendenze da modelli esterni, rendendo la soluzione immediatamente integrabile nei flussi di lavoro industriali esistenti.
• Scoperta di Euristica: Il sistema è riuscito a scoprire combinazioni di euristiche pratiche e robuste che sarebbero state difficili da trovare manualmente, superando i limiti dell'ottimizzazione umana e delle soluzioni ML runtime.

In sintesi, il paper dimostra che l'evoluzione del codice guidata da LLM, se vincolata da gate di validazione formale, può produrre strumenti di verifica hardware significativamente più potenti, mantenendo la garanzia di correttezza richiesta dall'industria dei semiconduttori.