Formale Verifikation von Baum-basierten ML-Modellen für seitliches Ausbreiten

Maschinelles Lernen wird zunehmend zur Vorhersage geotechnischer Gefahren eingesetzt. Trotz hoher Genauigkeit können Modelle jedoch physikalisch inkonsistente Zusammenhänge aus unvollständigen oder voreingenommenen Trainingsdaten lernen. Traditionelle Ansätze wie SHAP, LIME oder Trainingszeitbeschränkungen liefern lediglich ungefähre Diagnosen oder reduzieren die Modellkapazität, ohne umfassende Garantien zu bieten.

In dieser Arbeit wird ein neuer Ansatz vorgestellt: trainierte Baum-Ensembles werden als logische Formeln in einen Satisfiability Modulo Theories (SMT)-Solver übersetzt. Der Solver prüft vier geotechnische Spezifikationen – Wasserstand, Monotonie der PGA, Distanzsicherheit und Flächensicherheit – über den gesamten Eingabebereich und nicht nur über Stichproben. Dabei werden sowohl XGBoost- als auch Explainable Boosting Machine (EBM)-Modelle auf dem 2011er Christchurch-Erdbeben-Datensatz (7 291 Standorte, vier Merkmale) getestet.

Der SMT-Solver liefert entweder einen konkreten Gegenbeweis oder beweist die Einhaltung der Spezifikation. Das unbeschränkte EBM mit 80,1 % Genauigkeit verletzt alle vier Spezifikationen, während ein vollständig konstrahiertes EBM mit 67,2 % Genauigkeit drei von vier Spezifikationen erfüllt. Eine Pareto-Analyse von 33 Modellvarianten zeigt, dass keine Variante gleichzeitig mehr als 80 % Genauigkeit und vollständige Konformität erreicht – ein klarer Kompromiss zwischen Genauigkeit und physikalischer Konsistenz.

Die Ergebnisse demonstrieren, dass die iterative Anwendung von Constraints, unterstützt durch formale Verifikation, die physikalische Konsistenz von ML-Modellen systematisch verbessern kann. Dieser Ansatz bietet einen vielversprechenden Weg, um zuverlässigere und sicherere Vorhersagen in der Geotechnik zu ermöglichen.