Sintesi Tecnica: Verifica del Software Neuro-Simbolica con VerIbmc

Definizione del Problema

La sintesi degli invarianti di ciclo rimane un collo di bottiglia centrale nella verifica formale del software. Sebbene esistano tecniche simboliche (ad esempio, interpretazione astratta, risoluzione di vincoli) e metodi basati sui dati "guess-and-check", esse spesso faticano con scalabilità, espressività o la diversità del codice reale. Recentemente, i Large Language Models (LLM) hanno mostrato una promettente capacità di generare candidati invarianti sfruttando pattern appresi da corpora di codice. Tuttavia, gli approoli neuro-simbolici esistenti si affidano tipicamente a modelli proprietari e chiusi, accessibili tramite API cloud esterne. Questa dipendenza introduce ostacoli significativi per l'implementazione industriale:

1. Privacy e Conformità: Il codice sorgente deve essere trasmesso a servizi terzi, sollevando preoccupazioni sulla riservatezza.
2. Riproducibilità: La dipendenza da fornitori esterni complica l'integrazione in pipeline di verifica controllate.
3. Costo e Sostenibilità: I modelli di grandi dimensioni sono computazionalmente costosi e intensivi dal punto di vista energetico, limitandone la praticità per flussi di lavoro di verifica continua.

Gli autori sostengono che queste sfide rendano necessario un passaggio verso modelli linguistici a pesi aperti (open-weight), distribuibili localmente, che possano operare interamente all'interno dell'infrastruttura di un'organizzazione senza esporre codice proprietario.

Metodologia: La Pipeline VerIbmc

Il documento presenta VerIbmc, una pipeline neuro-simbolica progettata per sintetizzare invarianti di ciclo per programmi C, accoppiando il ragionamento simbolico con LLM a pesi aperti ospitati localmente. Il sistema utilizza ESBMC (Efficient SMT-Based Context-Bounded Model Checker) come oracolo di verifica. La pipeline è progettata sul principio di "escalation solo quando necessario", dando priorità al ragionamento simbolico deterministico ed economico prima di invocare l'LLM.

Architettura Core

La pipeline opera in tre fasi distinte:

1. Fase 0 (Verifica Baseline): ESBMC verifica il programma non annotato. Se il programma è trivialmente sicuro o provabilmente insicuro, il processo termina immediatamente, evitando sforzi di sintesi non necessari.
2. Fase 1 (Generazione di Candidati Simbolici): Se la Fase 0 restituisce "Unknown", il sistema enumera simbolicamente atomi candidati invarianti tramite il confronto a coppie tra variabili di ingresso del ciclo e costanti. Questi atomi sono verificati per induttività tramite ESBMC. Il sistema mantiene tre store: Provabili ($P$), Disprovabili ($D$) e Sconosciuti ($U$). Se la congiunzione di tutti gli atomi provabili è sufficiente a dimostrare la post-condizione, la pipeline termina con successo senza alcuna chiamata all'LLM.
3. Fase 2 (Ciclo di Raffinamento LLM): Se la fase simbolica è insufficiente, la pipeline entra in un ciclo iterativo in cui un LLM viene istruito per generare nuovi invarianti.
   • Meccanismo di Feedback: L'LLM riceve il programma corrente, il contenuto degli store $P$, $D$ e $U$ come feedback strutturato, ed esempi few-shot.
   • Decomposizione e Ricombinazione: Quando un candidato generato dall'LLM fallisce la verifica, il sistema lo decompone in sotto-formule (atomi). Gli atomi vengono verificati individualmente e aggiunti allo store appropriato. La congiunzione di tutti gli atomi attualmente provabili viene poi riverificata. Ciò consente al sistema di recuperare componenti utili dalle proposte fallite dell'LLM.
   • Terminazione: Il ciclo continua finché non viene trovato un invariante valido, finché il budget di iterazione è esaurito o si verifica un timeout.

Strategie di Inferenza

Gli autori valutano quattro strategie di inferenza basate su due assi di progettazione:

1. Feedback del Verificatore (Prior Simbolico):
   • Basic: Esegue l'intera pipeline a tre fasi, utilizzando il prior simbolico della Fase 1 e il filtraggio a livello di atomo.
   • LLM-Only: Salta la Fase 1 e la decomposizione a livello di atomo, affidandosi esclusivamente all'LLM per generare invarianti induttivi come blocco unico. Questo funge da baseline di ablazione.
2. Struttura di Ragionamento:
   • Chain-of-Thought (CoT): Utilizza il prompting standard con esempi di ragionamento passo-passo (Induttivo, Logica di Hoare, Clausole di Horn o derivazione diretta).
   • Tree-of-Thoughts (ToT): Esplora più stili di derivazione in parallelo durante una fase di "scouting", li valuta in base al numero di atomi provabili generati e concentra il budget di iterazione rimanente sui due stili con le prestazioni migliori.

Contributi Chiave

1. Pipeline Neuro-Simbolica: Un sistema completo che integra LLM a pesi aperti serviti localmente con ESBMC per la sintesi automatizzata di invarianti di ciclo, operando interamente su infrastruttura interna.
2. Valutazione Sistematica delle Strategie: Un confronto esaustivo tra le varianti pure LLM, guidate dal simbolo e Tree-of-Thoughts (ToT), dimostrando l'impatto del feedback simbolico e delle strutture di ragionamento.
3. Guadagni dal Feedback Simbolico: Dimostrazione che fornire atomi di invariante provabili come contesto all'LLM produce guadagni costanti, in particolare per modelli più deboli (ad esempio, Llama-3.1-8B ottiene +35 benchmark risolti rispetto a una baseline pure-LLM).
4. Analisi del Prompt Engineering: Valutazione di diversi stili di prompting (CoT vs. ToT) e template di ragionamento (Induttivo, Logica di Hoare, Clausole di Horn) sulla sintesi degli invarianti.
5. Benchmarking su Larga Scala: Una valutazione estesa attraverso cinque famiglie di benchmark (520 problemi, 499 efficaci), totalizzando 10.400 esiti per problema, su cinque modelli a pesi aperti (da 7B a 120B parametri).

Risultati Sperimentali

La valutazione è stata condotta su un server con quattro GPU NVIDIA RTX A6000 utilizzando cinque modelli a pesi aperti: GPT-OSS-120B, GPT-OSS-20B, Qwen2.5-32B, Qwen2.5-7B e Llama-3.1-8B.

• Prestazioni Complessive: La migliore configurazione singola (GPT-OSS-120B con la strategia Basic) ha risolto 431 su 499 problemi (86,4%).
• Confronto con lo Stato dell'Arte (SOTA):
  • VerIbmc supera sostanzialmente gli strumenti puramente simbolici (CPA-Checker, 2ls, ESBMC-Kind) e quelli puramente neurali (Code2Inv) quando eseguiti sullo stesso hardware locale.
  • Su suite di benchmark condivise, VerIbmc è competitivo o leggermente inferiore ai più forti strumenti aumentati da LLM (Clause2Inv, LaM4Inv, LORIS) che si affidano a costose API esterne (es. GPT-4). Notevolmente, VerIbmc raggiunge questi risultati senza trasmettere codice al cloud.
  • VerIbmc scala unicamente all'intero set di benchmark SV-COMP (154 problemi), inclusi programmi con array, cicli annidati e puntatori, che molti strumenti concorrenti non riescono a esprimere a causa di limitazioni del frontend.
• Impatto della Fase Simbolica: La Fase 1 simbolica ha risolto 75 problemi senza alcuna chiamata all'LLM. Per i modelli più deboli, l'aumento simbolico ha fornito incrementi significativi (fino a +35 problemi risolti aggiuntivi per Llama-3.1-8B).
• ToT vs. CoT: Il prompting ToT ha mostrato un compromesso tra diversità e accuratezza. Sebbene abbia raggiunto coppie problema-modello uniche inaccessibili alla CoT, ha spesso comportato un overhead di tempo di esecuzione (wall-clock) e, per i modelli più deboli, ha causato una diminuzione netta dei problemi risolti a causa dell'esaurimento del budget di iterazione. Per i modelli più forti (GPT-OSS-120B), la differenza di prestazione tra CoT e ToT è stata trascurabile.
• Capacità del Modello: I risultati indicano che la capacità del modello è il driver primario dell'accuratezza. Il divario tra il modello più forte e quello più debole è stato significativamente più grande della varianza di prestazione introdotta dal cambio di strategia all'interno dello stesso modello.

Significato e Rivendicazioni

L'articolo sostiene che VerIbmc dimostri che un approccio neuro-simbolico basato su LLM può essere applicato efficacemente alla sintesi di invarianti in modo riservato alla privacy ed efficiente dal punto di vista energetico. Operando interamente su infrastruttura locale con modelli a pesi aperti, l'approccio elimina la necessità di costosi modelli proprietari di frontiera bloccati dietro API.

Gli autori sottolineano che il loro metodo è corretto per costruzione (sound by construction): ogni candidato invariante è convalidato da un verificatore formale (ESBC) prima dell'accettazione. Sebbene il sistema sia incompleto a causa dell'indecidibilità del problema, esso fornisce un percorso pratico, scalabile e riproducibile per la verifica assistita dall'IA del software di produzione. Il lavoro rappresenta un passo verso pipeline di verifica pronte per l'industria, dove la privacy dei dati e l'efficienza delle risorse sono requisiti critici.