Sintesi Tecnica: Analisi della Robustezza Neurosimbolica per Sistemi Discreti rispetto alle Deviazioni di Transizione

Definizione del Problema

Nel controllo supervisionato di sistemi a eventi discreti (DES), i controllori vengono sintetizzati per imporre specifiche su un modello di impianto (plant). Sebbene i metodi classici forniscano garanzie di tipo "corretto per costruzione" (correct-by-construction), tali garanzie dipendono strettamente dall'accuratezza del modello dell'impianto. Nella pratica, i disallineamenti derivanti da dinamiche non modellate, rumore dei sensori o errori di astrazione causano deviazioni del sistema reale rispetto al modello nominale, compromettendo potenzialmente la sicurezza.

Studi recenti hanno affrontato questo problema definendo la robustezza discreta come l'insieme di tutte le possibili deviazioni di transizione (transizioni aggiuntive aggiunte al plant nominale) contro le quali un supervisore mantiene la sicurezza. Tuttavia, questo approccio basato sulle transizioni presenta due criticità fondamentali:

1. Scalabilità: Lo spazio delle possibili deviazioni cresce esponenzialmente con gli spazi di stato e di azione, rendendo l'enumerazione esaustiva computazionalmente intrattabile per tutti i sistemi tranne quelli estremamente piccoli.
2. Conservatività: La stragrande maggioranza delle deviazioni matematicamente possibili sono fisicamente non fattibili (ad esempio, una macchina che produce spontaneamente un pezzo senza input). L'inclusione di queste deviazioni non fattibili gonfia lo spazio di ricerca e produce risultati di robustezza che non riflettono accuratamente il comportamento reale del sistema.

I tentativi esistenti di filtrare le deviazioni non fattibili utilizzando vincoli formali di sistema ($P_{sys}$) richiedono agli esperti di dominio di codificare manualmente le leggi fisiche in specifiche formali, creando un carico significativo e aggiungendo overhead alla pipeline di analisi.

Metodologia

Il documento propone un framework di calcolo neurosimbolico per affrontare queste sfide di scalabilità e fattibilità. L'approccio scinde il ragionamento sulla fattibilità fisica dalla computazione formale delle garanzie di robustezza, utilizzando un processo in due fasi:

1. Filtraggio della Fattibilità Neurale (Livello LLM)

La prima fase sfrutta i Large Language Models (LLM) per inferire un sottoinsieme di transizioni di deviazione fisicamente fattibili ($D$).

• Input: Il framework riceve modelli LTS formali del plant e del supervisore, descrizioni in linguaggio naturale degli stati e degli eventi del sistema, specifiche di sicurezza e conoscenza del dominio riguardante le leggi fisiche (ad esempio, "un pezzo non può trovarsi in due posti contemporaneamente").
• Processo: Un template di prompt strutturato guida l'LLM nel ragionare su questi input. L'LLM ha il compito di identificare transizioni che rappresentino guasti o deviazioni realistiche coerenti con la semantica del sistema e i vincoli fisici.
• Output: Un set ridotto di deviazioni fattibili $D \subseteq (Q_E \times Act_E \times Q_E) \setminus R_E$, significativamente più piccolo rispetto allo spazio di transizione completo.

2. Verifica della Robustezza Simbolica (Livello Simbolico)

La seconda fase esegue la verifica formale sul set ridotto $D$.

• Processo: Un algoritmo brute-force (Algoritmo 1) itera attraverso tutti i sottoinsiemi delle deviazioni fattibili $D$. Per ogni insieme di deviazioni candidato $d$, utilizza il model checking standard per verificare se il sistema deviato $E_d$ controllato dal supervisore $S$ soddisfa la proprietà di sicurezza $P$ (ovvero, $E_d/S \models P$).
• Raffinamento: L'algoritmo estrae solo le deviazioni di robustezza massimali (quelle non contenute in altre deviazioni robuste) per formare l'insieme finale di robustezza $\Delta_f$.
• Garanzia: Poiché la verifica viene eseguita simbolicamente su un sistema di transizione formalmente definito, le garanzie di robustezza risultanti rimangono matematicamente corrette rispetto all'insieme inferito $D$.

Contributi Chiave

Il documento delinea due contributi primari:

1. Un Framework Neurosimbolico: Un'architettura innovativa che combina gli LLM per l'inferenza di modelli di deviazione fisicamente fattibili con metodi simbolici per il calcolo delle garanzie di robustezza. Questo approccio automatizza l'estrazione dei vincoli fisici da descrizioni in linguaggio naturale e conoscenza del dominio, eliminando la necessità di una codifica formale manuale di $P_{sys}$.
2. Prototipo e Valutazione: L'implementazione di uno strumento prototipo e la sua valutazione sperimentale su tre distinti casi di studio: un sistema manifatturiero, l'interfaccia della terapia radiante Therac-25 e il protocollo Alternate Bit (ABP).

Risultati Sperimentali

Il framework è stato valutato su tre casi di studio utilizzando LLM (GPT-5.2 e Claude 3.5 Sonnet) per il filtraggio della fattibilità e un verificatore simbolico basato su Python.

• Sistema Manifatturiero: L'LLM ha identificato 18 deviazioni fattibili (su uno spazio teorico di 108). Lo strato simbolico ha trovato un insieme di deviazioni robuste massimali, confermando che il sistema è robusto contro 15 transizioni specifiche ma vulnerabile a specifici guasti di scarico del buffer.
• Therac-25: L'analisi ha identificato 9 deviazioni fattibili. Il sistema è stato trovato robusto contro pressioni ripetute del tasto "enter" dell'operatore, ma vulnerabile alla specifica condizione di race condition riguardante la selezione della terapia elettronica, catturando accuratamente il difetto di progettazione storico.
• Protocollo ABP: L'LLM ha identificato 16 deviazioni fattibili. L'analisi ha confermato la robustezza contro la perdita, la duplicazione e la corruzione dei messaggi, allineandosi con l'intento di progettazione del protocollo.

Risultati Quantitativi:

• Riduzione della Fattibilità: Gli LLM hanno ridotto significativamente lo spazio di ricerca. La riduzione è variata dal 67% (Therac-25) al 99% (ABP) rispetto al pieno spazio di transizione.
• Accuratezza della Fattibilità: Per l'esempio manifatturiero, l'89% delle transizioni generate da GPT era fisicamente fattibile, rispetto al 54% di Claude. Su sistemi più complessi come l'ABP, i tassi di fattibilità sono diminuiti per entrambi i modelli (rispettivamente 63% e 36%), indicando la necessità di un miglioramento del prompt engineering o delle ontologie di dominio.
• Equivalenza della Robustezza: Nonostante l'operare su un set ridotto di deviazioni, il framework ha prodotto garanzie di robustezza comparabili a quelle ottenute tramite l'analisi completa basata sulle transizioni nei casi valutati.

Significato e Rivendicazioni

Il documento sostiene che questo approccio neurosimbolico affronta con successo il compromesso tra scalabilità e l'inclusione di deviazioni non fattibili nell'analisi della robustezza discreta. Utilizzando gli LLM per filtrare lo spazio delle soluzioni basandosi sulla comprensione semantica e fisica, il metodo rende trattabile l'analisi della robustezza per sistemi dove l'enumerazione esaustiva è impossibile.

Gli autori sottolineano che, sebbene la componente LLM introduca un elemento probabilistico nell'identificazione delle deviazioni fattibili, la successiva verifica simbolica assicura che le garanzie di robustezza finali siano formalmente corrette rispetto al set inferito. Il lavoro dimostra che è possibile recuperare analisi di robustezza comparabili ai metodi a spazio completo operando su un sottoinsieme di deviazioni drasticamente più piccolo e fisicamente significativo.

Il documento conclude con modestia, osservando che l'attuale implementazione dell'algoritmo brute-force richiede ottimizzazione per sistemi più grandi e che il lavoro futuro si concentrerà sul miglioramento del prompt engineering, sull'integrazione di ontologie di dominio per aumentare l'accuratezza degli LLM e sull'investigazione di loop di raffinamento interattivi in cui i risultati simbolici guidano le query degli LLM.