Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Krishna Kumar

Abstract

Machine learning models for geotechnical hazard prediction can achieve high accuracy while learning physically inconsistent relationships from sparse or biased training data. Current remedies (post-hoc explainability, such as SHAP and LIME, and training-time constraints) either diagnose individual predictions approximately or restrict model capacity without providing exhaustive guarantees. This paper encodes trained tree ensembles as logical formulas in a Satisfiability Modulo Theories (SMT) solver and checks physical specifications across the entire input domain, not just sampled points. Four geotechnical specifications (water table depth, PGA monotonicity, distance safety, and flat-ground safety) are formalized as decidable logical formulas and verified via SMT against both XGBoost ensembles and Explainable Boosting Machines (EBMs) trained on the 2011 Christchurch earthquake lateral spreading dataset (7,291 sites, four features). The SMT solver either produces a concrete counterexample where a specification fails or proves that no violation exists. The unconstrained EBM (80.1% accuracy) violates all four specifications. A fully constrained EBM (67.2%) satisfies three of four specifications, demonstrating that iterative constraint application guided by verification can progressively improve physical consistency. A Pareto analysis of 33 model variants reveals a persistent trade-off, as none of the variants studied achieve both greater than 80% accuracy and full compliance with the specified set. SHAP analysis of specification counterexamples shows that the offending feature can rank last, demonstrating that post-hoc explanations do not substitute for formal verification. These results establish a verify-fix-verify engineering loop and a formal certification for deploying physically consistent ML models in safety-critical geotechnical applications.

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

Abstract

Machine learning models for geotechnical hazard prediction can achieve high accuracy while learning physically inconsistent relationships from sparse or biased training data. Current remedies (post-hoc explainability, such as SHAP and LIME, and training-time constraints) either diagnose individual predictions approximately or restrict model capacity without providing exhaustive guarantees. This paper encodes trained tree ensembles as logical formulas in a Satisfiability Modulo Theories (SMT) solver and checks physical specifications across the entire input domain, not just sampled points. Four geotechnical specifications (water table depth, PGA monotonicity, distance safety, and flat-ground safety) are formalized as decidable logical formulas and verified via SMT against both XGBoost ensembles and Explainable Boosting Machines (EBMs) trained on the 2011 Christchurch earthquake lateral spreading dataset (7,291 sites, four features). The SMT solver either produces a concrete counterexample where a specification fails or proves that no violation exists. The unconstrained EBM (80.1% accuracy) violates all four specifications. A fully constrained EBM (67.2%) satisfies three of four specifications, demonstrating that iterative constraint application guided by verification can progressively improve physical consistency. A Pareto analysis of 33 model variants reveals a persistent trade-off, as none of the variants studied achieve both greater than 80% accuracy and full compliance with the specified set. SHAP analysis of specification counterexamples shows that the offending feature can rank last, demonstrating that post-hoc explanations do not substitute for formal verification. These results establish a verify-fix-verify engineering loop and a formal certification for deploying physically consistent ML models in safety-critical geotechnical applications.
Paper Structure (43 sections, 1 theorem, 14 equations, 8 figures, 8 tables, 1 algorithm)

This paper contains 43 sections, 1 theorem, 14 equations, 8 figures, 8 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background and related work
  3. Machine learning for lateral spreading
  4. Embedding physical knowledge in ML models
  5. Hard monotone constraints
  6. Post-hoc shape function editing
  7. Formal verification of ML models
  8. SMT solvers
  9. Tree ensemble verification
  10. Positioning: formal verification as complement to constraints
  11. Problem formulation
  12. Dataset
  13. Physical specifications as logical formulas
  14. Specification A (Water table depth)
  15. Specification B (PGA monotonicity)
  16. ...and 28 more sections

Key Result

Proposition 1

Let $f(\mathbf{x}) = \beta_0 + \sum_{m=1}^{M} g_m(\mathbf{x})$ be an additive model. If each component $g_m$ is monotonically non-decreasing in feature $x_j$, then $f$ is monotonically non-decreasing in $x_j$.

Figures (8)

  • Figure 1: SMT encoding of an XGBoost gradient-boosted ensemble. Each of the 100 trees (a) is encoded as a nested If-Then-Else expression over real-valued leaf weights; the ensemble sum of all trees partitions the input space into regions of constant predicted probability (b).
  • Figure 2: Global feature importance. Left: SHAP beeswarm plot for unconstrained XGBoost. Each dot represents a test sample; color indicates feature value (red = high, blue = low). PGA shows both positive and negative SHAP values, indicating non-monotonic behavior. Right: EBM feature importance measured by shape function range (maximum minus minimum log-odds contribution).
  • Figure 3: EBM shape functions for all four features. Top row: unconstrained EBM. Bottom row: PGA-monotone EBM. The PGA shape function (rightmost column) shows non-physical behavior in the unconstrained model, specifically a dip near 0.42 g where increasing PGA decreases predicted log-odds. The monotone constraint eliminates this artifact.
  • Figure 4: Specification violation diagnostics for unconstrained XGBoost. Left: PGA monotonicity (Specification B) for three soil profiles; red dots mark non-monotone regions. Center: contour of predicted spreading probability over distance ($L$) and PGA, with Specification C safe region marked. Right: predicted probability versus groundwater depth for several PGA levels, with Specification A threshold at 5 m.
  • Figure 5: Schematic of two failure modes in a two-dimensional feature subspace defined by bounds $\mathit{lb}$ and $\mathit{ub}$. (a) No training data fall in the green region; the model interpolates without empirical support. (b) Training observations exist in the red region but are exclusively negative-class ($\circ$), yet the model predicts $y = 1$ at the SMT counterexample ($\times$). Specification D violations correspond to case (b).
  • ...and 3 more figures

Theorems & Definitions (2)

  • Proposition 1: Additive decomposition for monotonicity
  • proof