$\partial$CBDs: Differentiable Causal Block Diagrams

Riassunto Tecnico: $\partial$CBDs (Causal Block Diagrams Differenziabili)

1. Il Problema: La Triade in Conflitto nei Sistemi Cyber-Fisici (CPS)

La progettazione moderna dei sistemi cyber-fisici (CPS) richiede l'integrazione di modelli fisici, calcolo computazionale e apprendimento automatico (machine learning). Tuttavia, gli approcci attuali faticano a conciliare tre obiettivi fondamentali che spesso operano in isolamento:

• Componibilità (Compositionality): La capacità di costruire sistemi complessi assemblando moduli (supportata dai Causal Block Diagrams - CBD), ma che spesso mancano di strutture per l'ottimizzazione.
• Apprendibilità (Learnability): La capacità di ottimizzare parametri tramite gradienti (supportata dalla Differentiable Programming - DP), ma che spesso manca di garanzie formali di correttezza.
• Verificabilità (Verifiability): La capacità di garantire sicurezza e prestazioni tramite contratti formali (Assume-Guarantee contracts), che però sono solitamente scollegati dai processi di apprendimento basati sui dati.

Il problema centrale è la mancanza di un framework unificato che permetta di progettare sistemi che siano contemporaneamente modulari, addestrabili e certificabili.

2. Metodologia: Il Framework $\partial$CBD

Gli autori introducono i $\partial$CBDs, un formalismo che integra la struttura dei diagrammi a blocchi con la programmazione differenziabile e la teoria dei contratti. La metodologia si articola su cinque livelli di astrazione:

1. Livello Strutturale: Ogni blocco è definito come una tupla che include variabili di input ($U$), stato interno ($X$), output ($Y$), semantica temporale ($T$), funzioni di transizione di stato ($F$), funzione di output ($g$), condizioni iniziali ($Init$) e un insieme di contratti ($C$).
2. Livello Semantico: Definisce le regole di composizione (parallela, seriale e a feedback) che permettono di "appiattire" (flatten) un diagramma complesso in un unico blocco equivalente.
3. Livello dei Contratti: Vengono introdotti due tipi di contratti:
   • Contratti Assume-Guarantee (A–G): Forniscono specifiche normative per la correttezza composizionale (se l'input soddisfa l'assunzione $A$, l'output garantisce $G$).
   • Contratti basati sui Residui (Residual-based): Forniscono certificati quantitativi e differenziabili lungo le traiettorie eseguite, permettendo di trasformare i requisiti di sicurezza in funzioni di penalità o vincoli per l'ottimizzazione.
4. Livello Differenziabile: Il framework garantisce che ogni blocco sia (quasi ovunque) differenziabile. Attraverso tecniche come il rate lifting (sincronizzazione dei tempi), l'unrolling dei loop di feedback e l'uso di metodi di sensibilità (per ODE/DAE), il CBD viene ridotto a un Grafo Aciclico Diretto (DAG) eseguibile da motori di Automatic Differentiation (AD) come PyTorch o JAX.
5. Livello di Ottimizzazione: Il problema di progettazione viene formulato come un problema di ottimizzazione vincolata dove l'obiettivo è minimizzare una funzione di costo $J$ soggetta alla dinamica del sistema e al soddisfacimento dei residui dei contratti.

3. Contributi Chiave

• Unificazione Formale: Il primo framework che integra CBD, contratti A–G e programmazione differenziabile in un unico pipeline di modellazione.
• Contratti come Certificati Differenziabili: La trasformazione di specifiche di sicurezza (es. passività, stabilità di Lyapunov) in residui differenziabili che guidano l'apprendimento tramite gradienti.
• Riduzione a DAG Differenziabile: Un metodo sistematico per convertire diagrammi a blocchi causali e multi-rate in grafi pronti per l'addestramento tramite AD, preservando la causalità e la struttura fisica.

4. Risultati e Casi di Studio

Gli autori validano il framework attraverso tre esempi pratici:

1. Tuning di un Guadagno di Feedback: Dimostrano come regolare un guadagno $\kappa$ per garantire la stabilità di un sistema scalare, utilizzando un contratto di stabilità che agisce come vincolo durante l'ottimizzazione.
2. Apprendimento Congiunto di Policy Neurale e Certificato di Lyapunov: Utilizzando un oscillatore di Van der Pol, il framework apprende simultaneamente una rete neurale per il controllo e una funzione di Lyapunov (tramite ICNN) che certifica la stabilità della traiettoria.
3. Deep Koopman Operator con Certificato di Stabilità: Il framework viene utilizzato per identificare un modello lineare in uno spazio latente (Koopman) garantendo, tramite un contratto sul raggio spettrale, che la dinamica appresa sia intrinsecamente stabile.

5. Significato e Impatto

Il lavoro di Beckers et al. rappresenta un passo fondamentale verso l'AI Agente Sicura e l'Intelligenza Ibrida. Fornendo un ponte tra le librerie di differenziazione automatica (utilizzate nel deep learning) e i tool di verifica formale (utilizzati nell'ingegneria dei sistemi), $\partial$CBDs permette di progettare sistemi autonomi che non sono solo performanti, ma che portano con sé garanzie matematiche di sicurezza e correttezza fisica, integrabili direttamente nel processo di addestramento.