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

Titre de l'article

Vérification formelle des modèles d'apprentissage automatique basés sur les arbres pour le phénomène de liquéfaction latérale (lateral spreading)

1. Problématique

Les modèles d'apprentissage automatique (ML) utilisés pour prédire les risques géotechniques, tels que la liquéfaction et le glissement latéral, peuvent atteindre une grande précision tout en apprenant des relations physiquement incohérentes à partir de données d'entraînement clairsemées ou biaisées.

• Le problème de l'opacité : Les modèles ensemblistes (comme XGBoost) capturent des interactions complexes mais masquent la logique de décision. Cela permet l'émergence de comportements non physiques (par exemple, prédire une diminution du risque de glissement lorsque l'accélération sismique augmente) dans des régions de l'espace d'entrée peu représentées dans les données.
• Limites des solutions actuelles :
  • Explicabilité post-hoc (SHAP, LIME) : Ces méthodes sont approximatives. Elles peuvent suggérer la présence d'une erreur sur un échantillon spécifique mais ne peuvent pas certifier l'absence d'erreurs sur l'ensemble du domaine d'entrée. De plus, elles peuvent attribuer une importance faible à une caractéristique critique (comme la profondeur de la nappe phréatique) même lorsque celle-ci est la cause d'une violation de spécification.
  • Contraintes à l'entraînement (Monotonie) : Bien qu'elles améliorent la cohérence physique sur des caractéristiques individuelles, elles ne peuvent pas exprimer de conditions composées (impliquant plusieurs caractéristiques simultanément) et ne garantissent pas que le modèle respecte les spécifications sur tout son domaine.

L'absence d'outils d'assurance modèle exhaustifs capables de déterminer si un modèle entraîné satisfait des conditions de cohérence physiques spécifiques constitue un vide critique pour le déploiement en sécurité.

2. Méthodologie

L'article propose l'application de la vérification formelle via des solveurs SMT (Satisfiability Modulo Theories) aux modèles d'ensembles d'arbres en géotechnique.

• Encodage Logique : Les ensembles d'arbres entraînés (XGBoost et Explainable Boosting Machines - EBM) sont encodés sous forme de formules logiques dans un solveur SMT (Z3). Chaque arbre est représenté comme une expression imbriquée "Si-Alors-Sinon" (ITE) sur des réels.
• Formalisation des Spécifications : Quatre spécifications géotechniques sont définies comme des formules logiques décidables dans l'arithmétique réelle linéaire sans quantificateurs (QF_LRA) :
  1. Spécification A (Profondeur de la nappe phréatique) : Si la profondeur > 5 m, le risque ne doit pas être prédit.
  2. Spécification B (Monotonie du PGA) : L'augmentation de l'accélération sismique (PGA) ne doit jamais diminuer le risque prédit.
  3. Spécification C (Sécurité de la distance) : Si la distance à la face libre est grande (> 2,5 km) et le PGA faible (< 0,35 g), le risque ne doit pas être prédit.
  4. Spécification D (Sécurité du terrain plat) : Une version plus stricte de C, ajoutant une pente de terrain très faible (< 0,1 %).
• Processus de Vérification : Au lieu de tester des points échantillonnés, le solveur vérifie la négation de la spécification sur l'ensemble du domaine continu.
  • Si le solveur retourne SAT (satisfaisable), il fournit un contre-exemple concret (un vecteur d'entrée précis) où la spécification échoue.
  • Si le solveur retourne UNSAT (insatisfaisable), la spécification est prouvée vraie pour tout point du domaine.
• Boucle "Vérifier-Corriger-Vérifier" : Une approche itérative est proposée : entraîner un modèle, vérifier les spécifications, analyser les contre-exemples pour appliquer des contraintes ciblées (monotonie), puis ré-vérifier.

3. Contributions Clés

1. Première application de la vérification SMT aux modèles ML géotechniques, démontrant que les ensembles XGBoost et EBM peuvent être encodés et vérifiés formellement.
2. Formalisation de quatre spécifications couvrant des seuils simples, la monotonie et des conditions composées multi-caractéristiques, réduites à des requêtes de satisfiabilité QF_LRA.
3. Développement d'une boucle d'ingénierie permettant d'identifier les violations, d'appliquer des corrections ciblées et de prouver la conformité résiduelle.
4. Analyse de Pareto de 33 variantes de modèles quantifiant le compromis inévitable entre la précision (accuracy) et la conformité physique.

4. Résultats

L'étude a été menée sur le jeu de données du séisme de Christchurch (2011) comportant 7 291 sites.

• Modèles non contraints :
  • XGBoost (82,5 % de précision) : Violation des 4 spécifications. Le modèle prédit un glissement latéral même avec une nappe phréatique profonde ou une faible secousse lointaine.
  • EBM (80,1 % de précision) : Violation des 4 spécifications, malgré une structure additive plus interprétable.
• Modèles contraints (Monotonie) :
  • L'application de contraintes de monotonie sur le PGA (Spécification B) corrige cette violation spécifique mais ne suffit pas pour les spécifications A, C et D (conditions de seuil et composées).
  • La précision chute significativement (de ~82 % à ~69 % pour XGBoost contraint).
• Modèle EBM entièrement contraint :
  • En imposant des contraintes de monotonie sur les 4 caractéristiques, le modèle satisfait 3 spécifications sur 4 (B, C, D).
  • La Spécification A (nappe phréatique) reste violée de justesse (probabilité de 50,3 % à 5,003 m de profondeur), car la monotonie ne contrôle pas la valeur absolue de la sortie, seulement sa direction.
  • Précision finale : 67,2 %.
• Analyse du compromis (Pareto) : Aucun modèle étudié n'atteint à la fois >80 % de précision et une conformité totale aux spécifications. Le coût de la cohérence physique est d'environ 10 à 15 points de pourcentage de précision.
• Comparaison SHAP vs Vérification Formelle : L'analyse SHAP d'un contre-exemple (violation de la Spécification A) montre que la caractéristique violante (profondeur de la nappe) est classée dernière par SHAP, masquant ainsi la violation. La vérification formelle, elle, détecte automatiquement la violation et fournit le contre-exemple exact.

5. Signification et Conclusion

Ce travail établit un nouveau paradigme pour le déploiement de modèles ML en géotechnique, domaine critique pour la sécurité :

• Garantie Déterministe : Contrairement aux tests empiriques (qui peuvent manquer des violations rares dans des régions de données clairsemées), la vérification formelle offre une garantie mathématique que le modèle respecte les règles physiques sur tout le domaine d'entrée continu.
• Limites des Explicabilités Post-hoc : L'article démontre que SHAP et LIME ne remplacent pas la vérification formelle. Une explication locale peut sembler raisonnable alors que le modèle global viole des règles physiques fondamentales.
• Cadre de Certification : La boucle "Vérifier-Corriger-Vérifier" fournit une méthodologie systématique pour auditer et améliorer les modèles avant leur mise en œuvre sur le terrain.
• Implication Pratique : Bien que la contrainte physique réduise la précision statistique, elle est indispensable pour éviter des catastrophes dans des scénarios critiques où les données d'entraînement sont rares. La vérification formelle permet de quantifier ce coût et de certifier que les modèles restants sont physiquement cohérents.

En résumé, l'article prouve que la vérification formelle via SMT est un outil essentiel pour transformer les modèles d'apprentissage automatique de "boîtes noires" performantes en systèmes certifiés pour des applications géotechniques critiques.