Designing FSMs Specifications from Requirements with GPT 4.0

1. Il Problema

La progettazione di specifiche formali per sistemi reattivi (come le Macchine a Stati Finiti - FSM o Macchine di Mealy) è un compito fondamentale nell'ingegneria dei sistemi basata su modelli (MDE), utilizzato per l'analisi, la generazione di codice e il testing automatizzato. Tuttavia, queste specifiche sono spesso derivate da requisiti scritti in linguaggio naturale, un processo che, se eseguito manualmente, è lungo e soggetto a errori.

La qualità della specifica FSM è critica: una specifica di bassa qualità porta a un numero maggiore di difetti che sopravvivono alla fase di testing, aumentando il rischio di fallimento del sistema in produzione. L'obiettivo della ricerca è automatizzare la trasformazione di descrizioni testuali in linguaggio naturale in specifiche FSM rigorose (deterministiche) utilizzando i recenti progressi dei Modelli Linguistici di Grande Dimensione (LLM), in particolare GPT-4, e sviluppare metodi per correggere gli errori generati.

2. Metodologia

L'approccio proposto si articola in due fasi principali: la generazione delle specifiche tramite LLM e la loro riparazione (repair) tramite metodi semi-automatizzati.

A. Generazione delle FSM

• Input: Descrizioni testuali sintetiche (generate automaticamente) di FSM, che descrivono stati, ingressi, uscite e transizioni.
• Strumento: Utilizzo di GPT-4 (specificamente GPT-4o) tramite tecniche di prompt engineering.
• Processo: Vengono creati prompt strutturati che definiscono un ruolo (ingegnere software) e richiedono l'output in un formato CSV specifico (Stato, Ingresso, Uscita, Stato Successivo).
• Valutazione: Poiché non è possibile affidarsi esclusivamente a esperti umani per ogni valutazione, l'autore utilizza "Oracoli" (FSM di riferimento generate casualmente) per confrontare la FSM generata dall'LLM con quella attesa.

B. Metodi di Riparazione (Repair)

Il paper propone quattro approcci distinti per correggere le FSM difettose generate dall'LLM:

1. Riparazione basata su Errori Sintattici:

   • Confronta direttamente la FSM generata con l'oracolo.
   • Identifica errori specifici (transizioni mancanti, transizioni aggiuntive, errori di output, errori di trasferimento).
   • Genera un nuovo prompt che elenca esplicitamente le transizioni da aggiungere o rimuovere, chiedendo all'LLM di correggere il modello.
   • Nota: Questo metodo assume la disponibilità dell'oracolo completo, il che è irrealistico nella pratica, ma serve come baseline teorica.

2. Riparazione basata su Sequenze di Distinzione (Distinguishing Sequences):

   • Utilizza sequenze di input/output che distinguono il comportamento della FSM generata da quello dell'oracolo.
   • Il prompt viene arricchito con queste sequenze per guidare l'LLM verso il comportamento corretto.
   • Svantaggio: L'LLM fatica a gestire grandi quantità di informazioni comportamentali (sequenze lunghe), portando a risultati meno efficaci rispetto al metodo sintattico.

3. Riparazione basata su Sequenze di Controllo (Checking Sequences):

   • Approccio più realistico dove un esperto (o un oracolo) fornisce solo l'output atteso per una specifica sequenza di controllo, senza conoscere la struttura interna completa della FSM.
   • L'LLM viene interrogato iterativamente con queste sequenze per raffinare la specifica.
   • Svantaggio: Il calcolo delle sequenze di controllo è computazionalmente costoso (NP-completo) e i risultati sperimentali mostrano un tasso di successo inferiore rispetto ad altri metodi.

4. Riparazione basata su Modelli di Difetto (Fault Models) e Mutazione:

   • Sfrutta la conoscenza a priori dei tipi di errori più comuni commessi da GPT-4 (es. errori di output, transizioni mancanti).
   • Costruisce una "Macchina di Mutazione" che definisce uno spazio di riparazione contenente tutte le FSM plausibili ottenute applicando patch (patch di transizione) alla FSM generata.
   • Utilizza un algoritmo di estrazione (mining) basato su SAT e interazioni con un esperto per selezionare la FSM corretta all'interno di questo dominio, senza richiedere all'LLM di riscrivere il prompt per ogni errore.

3. Contributi Chiave

• Generazione di Dati Simulati: Creazione di un dataset sintetico composto da FSM oracle casuali e relative descrizioni in linguaggio naturale per valutare l'approccio.
• Framework di Prompt Engineering: Sviluppo di prompt specifici per la generazione di FSM in formato CSV da descrizioni testuali.
• Quattro Strategie di Riparazione: Proposta e valutazione comparativa di quattro metodi di riparazione, che spaziano dalla correzione sintattica diretta all'uso di modelli di mutazione e domini di riparazione.
• Analisi delle Capacità dell'LLM: Valutazione empirica della capacità di GPT-4 di comprendere requisiti complessi e di applicare correzioni basate su feedback iterativi.

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su FSM con 5, 10 e 25 stati.

• Generazione Iniziale: GPT-4 genera FSM corrette per macchine piccole, ma il tasso di errore aumenta con la complessità (numero di stati e transizioni). Gli errori più frequenti sono errori di output e transizioni mancanti.
• Efficacia della Riparazione:
  • Metodo Sintattico: Ha ottenuto un tasso di successo del 100% nella riparazione delle FSM difettose (quando l'oracolo è disponibile). Dimostra che fornire all'LLM un elenco esplicito di errori da correggere è molto efficace.
  • Metodo delle Sequenze di Distinzione: Ha mostrato risultati inferiori (0% di successo per macchine da 10 stati in alcuni test). L'LLM fatica a elaborare e integrare molte sequenze input/output nel prompt contemporaneamente.
  • Metodo delle Sequenze di Controllo: Ha ottenuto risultati modesti (40% per macchine da 5 stati), limitati dalla complessità computazionale e dalla lunghezza delle sequenze.
  • Metodo dei Modelli di Difetto: Ha ottenuto il 100% di successo sia per macchine da 5 che da 10 stati. Questo approccio, che non richiede all'LLM di "pensare" alla correzione ma di selezionare una soluzione da un dominio pre-calcolato, si è rivelato il più robusto e promettente.

5. Significato e Conclusioni

Il paper dimostra che, sebbene gli LLM come GPT-4 siano capaci di generare specifiche FSM da requisiti testuali, tendono a commettere errori che aumentano con la complessità del sistema. L'automazione completa non è ancora affidabile senza un intervento di riparazione.

La conclusione principale è che l'approccio più efficace non è chiedere all'LLM di correggere se stesso basandosi su lunghe liste di comportamenti attesi (che sovraccaricano il meccanismo di attenzione del modello), ma piuttosto:

1. Utilizzare metodi formali (come i modelli di mutazione) per delimitare lo spazio delle soluzioni possibili.
2. Integrare l'LLM in un ciclo semi-automatizzato dove un esperto valida solo le risposte necessarie per restringere lo spazio di ricerca.

Questo lavoro apre la strada a nuove visioni sull'uso degli LLM nell'ingegneria dei sistemi basata su modelli (MDE), suggerendo che il futuro risiede nell'ibridazione tra la capacità generativa degli LLM e la rigore dei metodi formali per la verifica e la riparazione delle specifiche.