Evaluating LLM-Generated ACSL Annotations for Formal Verification

Titolo

Valutazione delle Annotazioni ACSL Generate da LLM per la Verifica Formale

1. Il Problema

La specifica formale è fondamentale per costruire sistemi software verificabili e affidabili, ma generare specifiche accurate e verificabili per programmi C reali rimane una sfida significativa. Sebbene l'Intelligenza Artificiale (in particolare i Large Language Models o LLM) abbia fatto progressi enormi, la loro applicazione in domini ad alta garanzia (high-assurance) è ostacolata dalla mancanza di garanzie intrinseche di sicurezza e correttezza.
Il problema centrale affrontato è la capacità degli strumenti di analisi formale di generare e verificare automaticamente specifiche ACSL (ANSI/ISO C Specification Language) per programmi C senza alcun intervento umano o ausilio basato sull'apprendimento. Esiste un divario tra la capacità degli LLM di produrre codice sintatticamente corretto e la loro capacità di generare contratti semantici robusti sufficienti per la prova automatica di correttezza.

2. Metodologia

Gli autori hanno condotto uno studio empirico controllato su un dataset recente e pubblico, distinguendosi da lavori precedenti basati su sondaggi o flussi di lavoro interattivi.

• Dataset: Utilizzo di CASP (un dataset curato di 506 programmi C con specifiche ACSL verificate, pubblicato nel novembre 2025). Dopo la pulizia (rimozione di file vuoti o incompleti), lo studio si è focalizzato su 355 file C puri.
• Ambiente di Sperimentazione: Piattaforma Frama-C su Linux (WSL 2).
• Sistemi di Generazione ACSL Confrontati:
  1. Script Python basato su regole: Un approccio deterministico e rule-based.
  2. Plugin RTE di Frama-C: Generazione di contratti basati sul rilevamento di errori a runtime (Runtime Error Detection).
  3. Tre Large Language Models (LLM):
     • DeepSeek-V3.2 (riferito come DeepSeek).
     • GPT-5.2 (riferito come GPT-5).
     • OLMo 3.1 32B Instruct (riferito come OLMo3).
• Processo di Verifica: Tutte le specifiche generate sono state verificate in condizioni identiche utilizzando il plugin WP (Weakest Precondition) di Frama-C, supportato da quattro diversi solver SMT: Alt-Ergo, CVC4, CVC5 e Z3.
• Metriche Valutate:
  • Tasso di successo delle prove (Proof Success Rate).
  • Numero di timeout dei solver.
  • Tempo di esecuzione della prova ( Qed time).
  • Variabilità e stabilità delle prestazioni dei solver.

3. Contributi Chiave

• Valutazione Empirica Diretta: Fornisce una delle prime valutazioni comparative dirette tra generatori di specifiche basati su regole, plugin statici e LLM avanzati su un dataset moderno e omogeneo.
• Analisi della Stabilità dei Solver: Non si limita al tasso di successo, ma analizza approfonditamente la robustezza dei solver (frequenza di timeout e dispersione dei tempi di esecuzione) in risposta a diverse qualità di specifiche.
• Nuova Evidenza Empirica: Completa il lavoro precedente degli autori (basato su sondaggi) fornendo dati quantitativi reali sulle capacità e i limiti attuali degli LLM nella sintesi di specifiche formali per il C.

4. Risultati Principali

A. Prestazioni dei Generatori di Specifiche

• Strumenti Tradizionali (Script Python e RTE): Hanno ottenuto i risultati migliori.
  • RTE ha raggiunto un tasso di successo medio delle prove vicino al 99% con un numero estremamente basso di timeout. Le specifiche sono conservative ma altamente stabili e verificabili.
  • Lo Script Python ha mostrato buone prestazioni (circa 72% di successo medio), ma con tempi di esecuzione molto rapidi e bassa variabilità.
• LLM: Le prestazioni variano significativamente in base al modello:
  • DeepSeek: Ha mostrato le prestazioni migliori tra gli LLM, avvicinandosi alle metriche di RTE (successo medio ~94-95%), con una variabilità moderata.
  • OLMo3: Ha mostrato una stabilità sorprendente, con un successo medio dell'83% e una dispersione dei tempi di esecuzione molto bassa, simile agli strumenti tradizionali.
  • GPT-5: Ha ottenuto risultati inferiori (successo medio ~81%) e ha generato il maggior numero di timeout, specialmente con il solver Alt-Ergo, indicando specifiche semanticamente deboli o ambigue che aumentano lo spazio di ricerca del solver.

B. Comportamento dei Solver

• CVC4 e CVC5: Hanno mostrato la maggiore stabilità e consistenza across tutti i generatori, con tempi di esecuzione prevedibili e pochi timeout.
• Z3: Ha mostrato una variabilità centrale più bassa ma fluttuazioni più ampie su input complessi (LLM).
• Alt-Ergo: Ha sofferto di tassi di timeout significativamente più alti, specialmente quando le specifiche erano generate da LLM (es. GPT-5), suggerendo una minore robustezza contro specifiche ambigue.

C. Trade-off Espressività vs. Stabilità

Lo studio rivela un trade-off fondamentale:

• Le tecniche guidate da regole e strumenti (RTE) producono specifiche strutturate e prevedibili, garantendo una verifica rapida e stabile, ma con un'espressività limitata.
• Gli LLM (specialmente DeepSeek e GPT-5) generano specifiche più eterogenee ed espressive, ma questo si traduce in una maggiore dispersione nei tempi di verifica e in una minore stabilità dei solver.
• OLMo3 rappresenta una via di mezzo, offrendo specifiche più ricche mantenendo una stabilità di verifica accettabile.

5. Significato e Conclusioni

Il paper conclude che, sebbene gli approcci automatizzati (inclusi gli LLM) siano in grado di produrre specifiche verificabili, esistono limitazioni ricorrenti legate alla completezza delle annotazioni e alla sensibilità dei solver.

• Implicazioni Pratiche: Per la verifica su larga scala, la qualità della specifica non è misurabile solo dal successo della prova, ma anche dalla stabilità del solver. Specifiche generate da LLM, sebbene promettenti, richiedono ancora affinamento per garantire consistenza e compatibilità con diversi backend di verifica.
• Futuro della Ricerca: I risultati suggeriscono che l'integrazione di tecniche ibride (che combinano la ricchezza semantica degli LLM con la stabilità degli strumenti basati su regole) è la direzione più promettente. Inoltre, i generatori basati su regole tradizionali stanno iniziando a essere sfidati dagli LLM, ma non ancora superati in termini di affidabilità di verifica.

In sintesi, lo studio fornisce una base di riferimento concreta per la sintesi assistita dall'apprendimento nelle specifiche formali, evidenziando che l'automazione completa richiede un equilibrio tra ricchezza espressiva e controllo della variabilità per garantire prestazioni prevedibili dei solver.