Formal verification of tree-based machine learning models for lateral spreading

Titolo: Verifica Formale di Modelli di Machine Learning Basati su Alberi per la Liquefazione e lo Spostamento Laterale (Lateral Spreading)

1. Il Problema

I modelli di Machine Learning (ML) applicati alla previsione di rischi geotecnici, come la liquefazione e lo spostamento laterale del suolo durante i terremoti, possono raggiungere alte accuratezze predittive. Tuttavia, quando addestrati su dati sparsi o distorti, questi modelli tendono a imparare relazioni fisicamente inconsistenti che rimangono invisibili fino al momento del dispiegamento operativo.
Un esempio critico citato nel paper è un modello XGBoost addestrato sui dati del terremoto di Christchurch del 2011, che prevedeva erroneamente una diminuzione della probabilità di spostamento laterale all'aumentare dell'accelerazione massima del suolo (PGA) in alcune regioni. Questo comportamento non fisico era confinato in aree con pochi dati di addestramento, ma rappresentava un rischio grave per la sicurezza.
I metodi attuali di mitigazione presentano limiti significativi:

• Spiegabilità post-hoc (SHAP, LIME): Forniscono solo diagnosi approssimative su singoli punti e non possono garantire l'assenza di violazioni in tutto il dominio di input.
• Vincoli durante l'addestramento (es. monotonia): Migliorano la coerenza fisica ma operano solo su singole feature, non possono esprimere condizioni composte (es. "se la distanza è grande E l'accelerazione è bassa, allora rischio nullo") e non offrono garanzie esaustive su tutto il dominio.

2. Metodologia

Il paper introduce un approccio di verifica formale utilizzando i Satisfiability Modulo Theories (SMT) solver (in particolare Z3) per validare modelli ML basati su alberi decisionali (XGBoost e Explainable Boosting Machines - EBM).

• Codifica Logica: Gli ensemble di alberi addestrati vengono codificati come formule logiche in un solver SMT. Poiché gli alberi partizionano lo spazio degli input in regioni iperrettangolari con output costanti, la funzione del modello può essere rappresentata come una somma di espressioni If-Then-Else (ITE) su numeri reali.
• Verifica delle Specifiche: Vengono definite quattro specifiche geotecniche come formule logiche decidable:
  1. Profondità della falda (Spec A): Se la falda è profonda (>5m), non deve essere previsto spostamento.
  2. Monotonia PGA (Spec B): All'aumentare della PGA, il rischio non deve diminuire.
  3. Sicurezza della distanza (Spec C): Se la distanza dalla faccia libera è grande (>2.5km) E l'accelerazione è bassa (<0.35g), non deve essere previsto spostamento.
  4. Sicurezza del terreno piano (Spec D): Condizione simile alla C ma con pendenza quasi nulla (<0.1%).
• Processo di Verifica: Per verificare una specifica, il solver nega la formula e chiede se esiste un input che soddisfa la negazione (controesempio).
  • Se il solver restituisce SAT, è stato trovato un controesempio concreto (violazione).
  • Se restituisce UNSAT, la specifica è provata valida per tutti gli input possibili nel dominio.
• Loop "Verify-Fix-Verify": Il metodo propone un ciclo iterativo: addestramento -> verifica formale -> analisi dei controesempi -> applicazione di vincoli mirati -> re-verifica.

3. Contributi Chiave

1. Prima applicazione SMT al ML geotecnico: Dimostrazione che ensemble XGBoost ed EBM possono essere codificati e verificati formalmente contro specifiche di dominio.
2. Formalizzazione di specifiche complesse: Traduzione di regole ingegneristiche (soglie, monotonia, condizioni composte multi-feature) in query di soddisfacibilità logica (QF_LRA).
3. Ciclo di ingegneria sistematico: Introduzione di un workflow che utilizza i controesempi SMT per guidare l'applicazione di vincoli, superando i limiti dei vincoli a priori.
4. Analisi del trade-off: Quantificazione precisa del costo in termini di accuratezza necessario per ottenere la coerenza fisica completa.

4. Risultati

Lo studio è stato condotto su 33 varianti di modelli addestrati sul dataset di Christchurch (7.291 siti).

• Modelli Non Vincolati:
  • XGBoost (82.5% accuratezza) e EBM (80.1% accuratezza) violano tutte e quattro le specifiche.
  • La verifica formale ha identificato controesempi concreti in regioni a dati sparsi dove i modelli prevedono spostamenti in condizioni fisicamente impossibili.
• Modelli con Vincoli di Monotonia:
  • L'applicazione di vincoli di monotonia (es. solo sulla PGA) risolve la specifica B (monotonia), ma fallisce nel soddisfare le specifiche composte (C, D) e di soglia (A).
  • L'accuratezza scende significativamente (es. XGBoost da 82.5% a 69.3%).
• Modelli EBM Completamente Vincolati:
  • Un modello EBM con vincoli di monotonia su tutte e quattro le feature soddisfa 3 delle 4 specifiche (B, C, D).
  • La specifica A (profondità falda) viene violata per un margine sottile (probabilità 50.3% a 5.003m di profondità), dimostrando che la monotonia non garantisce automaticamente il rispetto di soglie assolute.
  • L'accuratezza finale è del 67.2%.
• Frontiera di Pareto: L'analisi rivela un trade-off persistente. Nessun modello studiato riesce a raggiungere sia un'accuratezza >80% sia la piena conformità alle specifiche. C'è un "costo" di 10-15 punti percentuali di accuratezza per garantire la coerenza fisica.
• Confronto SHAP vs Verifica Formale: L'analisi SHAP dei controesempi mostra che la feature che causa la violazione (es. profondità della falda) può essere classificata come l'ultima in termini di importanza (SHAP value basso), rendendo le spiegazioni post-hoc inaffidabili per rilevare violazioni sistemiche. La verifica formale, invece, individua automaticamente la violazione.

5. Significato e Implicazioni

Questo lavoro stabilisce un nuovo paradigma per l'adozione sicura del ML in applicazioni geotecniche critiche:

• Garanzie Deterministiche: A differenza del testing empirico (che può perdere violazioni in regioni rare), la verifica SMT offre una garanzia matematica che un modello rispetta le regole fisiche su tutto il dominio continuo.
• Supplemento ai Vincoli: La verifica formale non sostituisce i vincoli di addestramento, ma li completa, rivelando quando i vincoli sono insufficienti per garantire la sicurezza.
• Certificazione: Fornisce una base metodologica per la certificazione formale dei modelli ML prima del dispiegamento sul campo, trasformando la coerenza fisica da un'assunzione a una proprietà verificata.
• Scalabilità: Sebbene la verifica di modelli complessi richieda risorse computazionali, l'uso di tecniche di decomposizione (es. verifica per singolo albero per la monotonia) rende il processo praticabile per ensemble di dimensioni reali.

In sintesi, il paper dimostra che la verifica formale è essenziale per identificare e correggere le inconsistenze fisiche nei modelli ML, offrendo un percorso verso modelli di intelligenza artificiale affidabili e certificabili per la gestione dei rischi naturali.