Sintesi Neuro-Simbolica di Modelli di Utilizzo di Markov Formalmente Verificati

1. Definizione del Problema

Il collo di bottiglia principale che impedisce l'adozione diffusa del Model-Based Statistical Testing (MBST) oltre le nicchie critiche per la sicurezza è la costruzione manuale dei modelli di utilizzo di catene di Markov. Questi modelli sono essenziali per spostare gli obiettivi di testing dalla copertura del codice assoluta all'inferenza statistica riguardante la qualità attesa sul campo. Tuttavia, tradurre requisiti in linguaggio naturale ambigui e non strutturati in topologie di transizione di stato e matrici di probabilità matematicamente coerenti richiede una significativa competenza nei metodi formali.

Sebbene i Large Language Models (LLM) abbiano dimostrato capacità di estrazione sintattica, gli approcci puramente neurali soffrono di quattro criticità fondamentali quando applicati all'MBST:

1. Volatilità Stocastica e Allucinazione: Gli LLM possono omettere casi limite critici, costruire transizioni impossibili o violare gli invarianti di sistema, portando a casi di test invalidi.
2. Fallimento della Calibrazione: Gli LLM faticano con il ragionamento numerico preciso, fallendo spesso nel soddisfare i vincoli rigorosi di stocasticità per riga ($\sum_j p_{ij} = 1$) e i complessi vincoli multi-variabile richiesti per catene di Markov valide.
3. Esplosione dello Spazio degli Stati: Gli LLM che operano entro finestre di contesto finite non possono tracciare o generare efficacemente modelli di transizione altamente concorrenti e multi-stream senza perdere coerenza strutturale.
4. Divergenza tra Semantica e Fattibilità: Gli LLM eccellono nel progresso semantico ma violano frequentemente i vincoli di fattibilità fisica e logica (ad esempio, eseguire una transizione di checkout con un carrello vuoto), generando percorsi che sono semanticamente logici ma fisicamente ineseguibili.

La letteratura esistente manca di una valutazione end-to-end sulla capacità della costruzione automatizzata del modello di preservare le proprietà strutturali e probabilistiche necessarie per le garanzie di rilevamento dei guasti dell'MBST.

2. Metodologia: Il Framework NeSy-MBST

Il documento introduce il Neuro-Symbolic Model-Based Statistical Testing (NeSy-MBST), un framework ibrido che disaccoppia il parsing semantico dalla risoluzione dei vincoli matematici. L'architettura integra cinque fasi strettamente accoppiate:

A. Architettura a Doppia Memoria Progresso-Fattibilità

Il sistema partiziona la costruzione del modello in due sistemi di memoria complementari:

• Memoria Neurale del Progresso: Un LLM sottoposto a fine-tuning analizza i requisiti in linguaggio naturale per bozzare un grafo di flusso semantico (il "cosa"), catturando le topologie comportamentali intese.
• Memoria Simbolica della Fattibilità: Un motore basato su regole impone rigidi invarianti logici, precondizioni e guardie di transizione (il "come"), validando ogni transizione candidata prima dell'ammissione.

B. Apprendimento di Automi Attivo tramite $L^*$ con Oracoli LLM

Il framework impiega una variante specializzata dell'algoritmo di apprendimento attivo di automi $L^*$ per scoprire lo spazio degli stati.

• Query di Appartenenza (Membership Queries): L'algoritmo interroga un oracolo LLM vincolato dalla grammatica (limitato agli output: Sì, No, Non sicuro) per determinare se una sequenza di input candidata è accettata.
• Query di Equivalenza: L'automa ipotetico corrente viene testato contro il Sistema Sotto Test (SUT) effettivo. Le divergenze generano controesempi utilizzati per raffinare l'ipotesi.
• Escalation: Se l'LLM restituisce "Non sicuro", la query viene scalata verso esperti umani o l'esecuzione del runtime del SUT, garantendo che il ciclo di apprendimento non incorpori mai informazioni non verificate.

C. Modellazione Gerarchica Dipendente dal Percorso

Per affrontare la dipendenza dal percorso senza esplosione combinatoria, NeSy-MBST utilizza una gerarchia a due livelli:

1. Struttura ad Albero Superiore: Le sequenze frequenti e dipendenti dal percorso sono modellate come una catena di Markov di ordine superiore incorporata in un albero.
2. Modello di Markov Inferiore: I percorsi di eccezione o meno frequenti sono modellati utilizzando catene di Markov standard di primo ordine.

D. Ottimizzazione dei Vincoli Matematici

Inveve di chiedere all'LLM di generare direttamente le probabilità numeriche, il framework delega questo compito a un solver simbolico:

1. Estrazione dei Vincoli: L'LLM estrae relazioni comparative (ad esempio, $P(\text{checkout}|\text{carrello}) > P(\text{navigazione}|\text{carrello})$) dai requisiti.
2. Ottimizzazione Convessa: Un motore di programmazione convessa (SLSQP) risolve la matrice di probabilità di transizione $P$ che soddisfi tutti i vincoli estratti, la stocasticità per riga e i limiti specifici del dominio, massimizzando al contempo l'entropia per evitare bias ingiustificati.

E. Adattamento del Modello a Ciclo Chiuso

Il framework tratta il modello di utilizzo come un artefatto vivo. La telemetria a runtime (log di esecuzione, metriche di copertura, dati sui guasti) viene riportata al motore di modellazione. L'LLM analizza le divergenze tra il comportamento previsto e quello osservato, e il solver simbolico ricalibra le probabilità, assicurando che il modello converga verso i pattern di utilizzo del mondo reale.

3. Contributi Chiave

• Framework NeSy-MBST: Un'architettura innovativa che combina l'apprendimento attivo $L^*$, oracoli LLM vincolati dalla grammatica, solver simbolici e feedback a ciclo chiuso per automatizzare la sintesi dei modelli di utilizzo.
• Verifica Formale dell'Output LLM: L'introduzione di un ciclo di verifica simbolica che rileva violazioni strutturali (stati irraggiungibili, mancanza di auto-loop) e innesca il re-prompting mirato, convertendo un problema di generazione limitato dal richiamo in un problema di completamento guidato dalla verifica.
• Decomposizione Ortogonale degli Errori: Il documento stabilisce che la completezza strutturale (topologia) e la calibrazione probabilistica (pesi) sono proprietà ortogonali, affrontate separatamente rispettivamente dal ciclo simbolico e dall'ottimizzatore convesso.
• Validazione Empirica: Una valutazione completa su un benchmark di Sistemi Cyber-Fisici (CPS) per Veicoli Autonomi (AV) e due specifiche di e-commerce, confrontando NeSy-MBST con baseline puramente neurali e approcci manuali tradizionali.

4. Risultati Sperimentali

Valutato su un benchmark CPS per veicoli autonomi (9 stati, 13 transizioni) e modelli di e-commerce (fino a 42 stati, 218 transizioni), NeSy-MBST ha ottenuto i seguenti risultati:

• Accuratezza dell'Estrazione (RQ1): Ha raggiunto un F1 score di sistema di 0,9125, superando la soglia di sicurezza critica di 0,90. Ciò rappresenta un miglioramento del 39,1% rispetto alla migliore baseline GPT-4o (Hybrid SMF) e un miglioramento del 14,8% rispetto alla più forte baseline a singolo modello (Claude 3.5 Sonnet).
• Copertura del Rilevamento Guasti (RQ2): Ha raggiunto l'85,7% di copertura delle transizioni, un guadagno di 5 l' 35,7 punti percentuali rispetto alla baseline puramente neurale (50%). Ciò suggerisce un aumento significativo della diversità dei percorsi che rivelano guasti.
• Calibrazione Probabilistica (RQ3): Ha raggiunto una Divergenza di Jensen–Shannon (JSD) di 0,012 (rispetto allo 0,157 della baseline puramente neurale), confermando che l'ottimizzatore convesso preserva la fedeltà dell'allocazione dei test operativi. La distanza di Frobenius normalizzata era 0,0654, indicando un'alta somiglianza strutturale con la distribuzione di riferimento.
• Efficienza: Ha generato suite di test con copertura completa del modello in meno di sei minuti per modelli con fino a 42 stati.
• Studio di Ablazione (RQ4):
  • Il Ciclo Simbolico è stato identificato come il driver primario per la completezza strutturale (aumentando l'F1 delle transizioni da 0,78 a 0,96).
  • L'Ottimizzatore Convesso ha dimostrato di governare la calibrazione probabilistica senza alterare le metriche strutturali.
  • Il Feedback a ciclo chiuso ha fornito miglioramenti marginali nella fedeltà distributiva, preziosi principalmente per campagne di test a lungo termine.

5. Significatività e Rivendicazioni

Il documento sostiene che NeSy-MBST elimina il collo di bottiglia della modellazione manuale senza compromettere il rigore statistico richiesto dai sistemi cyber-fisici (CPS) critici per la sicurezza.

• Colmare il Divario: I risultati dimostrano che l'integrazione neuro-simbolica può raggiungere la fedeltà strutturale (F1 $\ge$ 0,90) e la calibrazione probabilistica richieste dall'MBST, che gli approcci puramente neurali non riescono a garantire.
• Proxy del Rilevamento Guasti: Sebbene lo studio non abbia misurato i tassi diretti di rilevamento dei difetti contro un corpus di guasti inseriti, il documento argomenta che l'osservato aumento del 35,7% nella copertura delle transizioni è un forte proxy per il rilevamento dei guasti, coerente con i miglioramenti del 25–40% riportati nella letteratura di deployment industriale dell'MBT.
• Standard Ingegneristico: Gli autori propongono che l'aumento degli LLM nella generazione di modelli di test formali debba passare da curiosità di ricerca a pratica ingegneristica standard, a condizione che vengano soddisfatte due condizioni: (1) gli LLM operino sotto vincoli strutturali (output vincolato dalla grammatica, verifica simbolica) per prevenire le allucinazioni, e (2) i parametri numerici siano assegnati da solver certificati, non direttamente dall'LLM.

Il documento conclude che questo approccio rende il testing statistico rigoroso accessibile a pratiche di sviluppo software più ampie, portandolo oltre i team specialisti della sicurezza, pur riconoscendo che sono necessari ulteriori lavori per validare questi risultati su sistemi industriali di scala maggiore e con stili di requisiti diversificati.