Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?

1. Enunciato del Problema

La Verifica Formale (FV) è fondamentale per garantire la correttezza dei progetti hardware (RTL). Tuttavia, la verifica di progetti industriali complessi rimane un collo di bottiglia a causa della natura "a livello di bit" della maggior parte degli strumenti di model checking. Questi strumenti faticano a costruire prove matematiche di alto livello, indipendenti dai bit, necessarie per proprietà complesse.

L'approccio standard per risolvere questo problema è la Dimostrazione per Induzione, che richiede lemma ausiliari (rafforzamenti induttivi) per dimostrare una proprietà. Attualmente, la generazione di questi lemma è un compito manuale e laborioso svolto da ingegneri esperti in FV. Il paper affronta la domanda: I Large Language Models (LLM) possono automatizzare l'estrazione di questi lemma ausiliari per costruire argomenti induttivi validi per la verifica hardware?

2. Metodologia: Un Approccio Neusimbolico

Gli autori propongono un framework neusimbolico che combina le capacità generative degli LLM con il rigore degli strumenti simbolici formali. Il sistema non si basa esclusivamente sull'output dell'LLM; invece, utilizza l'LLM per generare candidati e un solver formale per verificarli e filtrarli.

A. Componenti Principali

1. Framework di Prompting per LLM: Vengono utilizzate due strategie distinte per generare lemma candidati:

   • Non-Agentic (Singolo Prompt): Utilizza un prompt Few-Shot contenente $k$ esempi di triple (Design RTL, Proprietà, Lemma Induttivi). Gli esempi sono selezionati tramite similarità semantica (utilizzando sentence transformers) da un pool pre-costruito di Catena di Pensiero (CoT). L'LLM viene campionato $n$ volte con lo stesso prompt per raccogliere candidati diversificati.
   • Agentic (Interazione Iterativa): Inquadra la generazione dei lemma come un ciclo. L'LLM propone lemma, che vengono verificati dallo strumento formale. Se la verifica fallisce, lo strumento fornisce feedback (indicando quali lemma hanno fallito e perché) e un messaggio di "riparazione". L'LLM affina quindi i suoi suggerimenti nei turni successivi (fino a 5 iterazioni).

2. Algoritmo di Ragionamento Formale (FINDINDSTRENGTH):

   • Questo algoritmo prende l'insieme dei lemma candidati generati dall'LLM e tenta di trovare un sottoinsieme che formi un valido Rafforzamento Induttivo.
   • Rafforzamento Induttivo: Un insieme di lemma $L$ tale che $L \land \text{Proprietà}$ sia un invariante induttivo (soddisfa l'inizializzazione e la consecuzione).
   • Processo:
     1. Filtraggio: Verifica se i singoli lemma sono invarianti induttivi (utilizzando 1-induzione) o valgono fino a una profondità limitata (utilizzando Bounded Model Checking, BMC).
     2. Ordinamento: Prioritizza i lemma noti come invarianti induttivi rispetto a quelli che valgono solo entro un limite.
     3. Ricerca di Sottoinsieme: Itera attraverso i prefissi della lista ordinata per trovare il sottoinsieme più piccolo che, quando congiunto alla proprietà target, formi un invariante induttivo valido.
   • Strumentazione: Implementato utilizzando EBMC (uno strumento di verifica formale) con $k$-induzione e BMC.

B. Dataset

Il framework è stato valutato su 110 compiti di verifica comprendenti:

• 58 progetti SystemVerilog (da fonti come VCEGAR, VIS, v2c e progetti FIFO/Arbiter/CAM personalizzati).
• 47 esempi derivati da programmi C: Codice C tradotto in Macchine a Stati Finiti (FSM) SystemVerilog per testare la generalizzazione.
• Pool CoT: Un piccolo insieme di esempi scritti manualmente utilizzati per il prompting few-shot.

3. Contributi Chiave

1. Generazione Neusimbolica di Lemma: Dimostra il primo caso d'uso di LLM specificamente per l'estrazione di lemma ausiliari per la costruzione di prove formali nella verifica hardware.
2. Framework di Prompting Duale: Implementa e confronta un approccio statico Few-Shot con un approccio Agentic iterativo, mostrando che quest'ultimo può guidare l'LLM lontano da percorsi errati.
3. Valutazione Empirica: Fornisce uno studio completo su 110 compiti, evidenziando che gli LLM possono generare con successo argomenti induttivi non banali per progetti RTL open-source di medie dimensioni.
4. Gestione delle Allucinazioni: Dimostra che, sebbene gli LLM allucinino (producendo lemma sintatticamente invalidi o logicamente errati), un livello di filtraggio formale può estrarre efficacemente le prove corrette dal rumore.

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su istanze Amazon EC2 utilizzando sei LLM all'avanguardia (GPT-5, Claude 3.7, Claude 4 Sonnet, Claude 4.5 Sonnet, Claude 4.5 Haiku, Claude 4.5 Opus).

• Tasso di Successo: Il framework ha generato con successo argomenti induttivi provabilmente corretti per l'84% dei 110 compiti di verifica.
  • Configurazione Agentic: Ha risolto 92/110 esempi (84% di tasso di successo).
  • Configurazione Non-Agentic: Ha risolto 84/110 esempi (76% di tasso di successo).
• Prestazioni del Modello: Claude 4.5-Opus ha ottenuto i migliori risultati, risolvendo 88 esempi nella configurazione Agentic.
• Confronto con Strumenti SOTA:
  • Gli autori hanno identificato 31 benchmark "sfidanti" dove strumenti industriali all'avanguardia (JasperGold, VC-Formal, rIC3) non sono riusciti a dimostrare la proprietà entro un timeout di 10 minuti.
  • L'approccio basato su LLM ha risolto istanze che questi strumenti SOTA non potevano, in particolare nei casi che richiedevano rafforzamenti induttivi complessi (ad esempio, progetti specifici di FIFO e Arbiter).
  • In alcuni casi in cui l'LLM ha trovato il lemma corretto ma la verifica formale ha superato il timeout, il risultato è stato comunque considerato un successo in termini di generazione di lemma, poiché il collo di bottiglia era il tempo di esecuzione dello strumento di verifica, non il ragionamento dell'LLM.
• Analisi degli Errori:
  • Gli LLM hanno occasionalmente allucinato sintassi SVA (ad esempio, operatori non validi, variabili non definite) o utilizzato caratteri non ASCII.
  • La configurazione Agentic è stata più efficiente, trovando spesso soluzioni con un numero totale inferiore di lemma affinando iterativamente lo spazio di ricerca.

5. Significato e Impatto

• Valore Industriale: Questo approccio ha il potenziale per ridurre significativamente lo sforzo manuale richiesto dagli ingegneri di Verifica Formale. Automatizzando la scoperta di lemma ausiliari, abbassa la barriera all'applicazione dei metodi formali a progetti hardware complessi.
• Oltre la Memorizzazione: I risultati suggeriscono che gli LLM stanno eseguendo un ragionamento genuino piuttosto che una semplice memorizzazione, poiché sono riusciti a generalizzare agli esempi derivati da C e a gestire variazioni nell'istanziazione dei parametri e nella denominazione dei registri.
• Direzioni Future: Gli autori intendono estendere il framework per gestire più proprietà simultaneamente, scalare a progetti industriali più grandi e validare l'approccio in un contesto industriale reale.

Conclusione: Il paper stabilisce che gli LLM, quando accoppiati a strumenti di verifica formale in un ciclo neusimbolico, sono un metodo valido e potente per automatizzare la parte più difficile delle prove di induzione hardware: la scoperta di lemma ausiliari.