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.
Figures & tables
Feature
Description
Range
Unit
GWD
Groundwater depth
0.37–6.05
m
L
Distance to nearest free-face
0–3.29
km
Slope
Ground surface slope
0–10.92
%
PGA
Peak ground acceleration
0.33–0.57
g
Table 1: Input features for lateral spreading classification.
Symbol
Meaning
x=(g,ℓ,s,p)
Input vector (GWD, distance, slope, PGA)
X⊆R4
Bounded input domain
f(x)
Model logit (log-odds) output
y^(x)
Predicted class: 1[f(x)>0]
∀
Universal quantification (“for all”)
∃
Existential quantification (“there exists”)
Table 2: Notation and logical symbols.
Spec.
Name
Type
Monotone constraint sufficient?
A
Water table depth
Single-feature threshold
No
B
PGA monotonicity
Single-feature monotonicity
Yes
C
Distance safety
Compound multi-feature
No
D
Flat-ground safety
Compound multi-feature
No
Table 3: Specification taxonomy. Training-time monotone constraints can directly enforce only the monotonicity class (B). Threshold (A) and compound (C, D) specifications require formal verification to check.
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.
Model
A (Water table)
B (PGA mono.)
C (Distance)
D (Flat-ground)
Test Acc.
XGBoost (unconstrained)
✗
✗
✗
✗
82.5%
XGBoost (monotone)
✗
✓
✗
✗
69.3%
EBM (unconstrained)
✗
✗
✗
✗
80.1%
EBM (PGA monotone)
✗
✓
✗
✗
70.5%
EBM (fully constrained)
✗
✓
✓
✓
67.2%
Table 4: Specification verification results. XGBoost results are full SMT proofs (Z3). EBM results use SMT for Specifications A, C, and D; Specification B uses per-term score-array decomposition ( Proposition 1 ). The solver checks the negation of each specification: if satisfiable, a counterexample exists and the specification is violated (✗); if unsatisfiable, no counterexample exists and the specification is proven (✓). All counterexamples are validated against the actual model.
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 lb and 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 ( ∘ ), yet the model predicts y=1 at the SMT counterexample ( × ). Specification D violations correspond to case (b).
Figure 6: PGA monotonicity comparison across model families for a fixed soil profile (GWD = 1.5 m, L = 0.5 km, Slope = 2.0%). Red dots mark non-monotone regions where increasing PGA decreases predicted probability. Unconstrained XGBoost and EBM exhibit violations; monotone-constrained variants do not.
Figure 7: Accuracy versus physical consistency (Specification B compliance) for 33 model variants. Unconstrained models cluster at high accuracy with zero compliance (upper-left); constrained models cluster at lower accuracy with full compliance (lower-right). The fully constrained EBM (lowest green diamond, 67.2%) achieves full Specification B compliance and proves 3 of 4 specifications via SMT. No model occupies the ideal top-right region.
Model family
Variants
Acc. range
B violations
B compliance
XGBoost (unconstrained)
12
74.0–84.2%
120/120
0%
XGBoost (monotone)
12
68.3–70.0%
0/120 ✓
100% ✓
EBM (unconstrained)
4
74.6–80.1%
116/120
3.3%
EBM (monotone)
4
67.9–70.5%
0/120 ✓
100% ✓
EBM (fully constrained)
1
67.2%
0/120 ✓
100% ✓
Table 5: Summary statistics for the Pareto frontier, aggregated across hyperparameter variants. Violations and compliance refer to Specification B (PGA monotonicity) only, measured on 120 empirically sampled PGA-sweep profiles. Full specification verification results (Specifications A–D) are in Table 4 .
Figure 8: SHAP analysis of specification violations (unconstrained XGBoost). (a) Waterfall at a Specification A counterexample (GWD =5.65 m, predicted 91% spreading). Red bars push toward spreading, blue bars push against it. GWD is the feature that violates Specification A, yet SHAP ranks it last (#4) with the smallest magnitude ( −0.12 ). (b) SHAP dependence plot for PGA. Each dot is one test sample; color indicates the SHAP value (red = pushes toward spreading, blue = pushes against). The black line (binned mean) should increase monotonically if the model respects Specification B; instead, it drops sharply between 0.42–0.52 g (shaded region, red arrows), confirming the non-monotonicity that formal verification detects.
Spec.
GWD (m)
L (km)
Slope (%)
PGA (g)
Logit
Probability
A (water table)
5.001
1.35
1.58
0.37
+0.065
52%
C (distance safety)
1.73
2.501
0.05
0.33
+0.169
54%
D (flat-ground)
1.72
2.501
0.05
0.33
+0.169
54%
Table 6: Representative counterexamples from SMT verification of unconstrained XGBoost. A positive logit (probability >50 %) means the model predicts spreading, violating the specification. All counterexamples were validated against the actual XGBoost model to machine precision.
Method
Points eval.
Premise (C)
Premise (D)
Time
Violated?
Grid ( n=30 )
810,000
18,900
630
< 0.1 s
None found
Grid ( n=50 )
6,250,000
150,000
3,000
0.1 s
None found
Grid ( n=100 )
100,000,000
2,160,000
21,600
1.7 s
None found
Grid ( n=150 )
506,250,000
10,530,000
140,400
17 s
None found
Grid ( n=200 )
1,600,000,000
32,640,000
326,400
184 s
None found
SMT (C)
entire continuous domain
0.19 s
Yes
Table 7: Grid search versus SMT verification for Specifications C and D (unconstrained XGBoost). Grid search evaluates the model on n4 uniformly spaced points over X . The SMT solver encodes the model symbolically and reasons over the entire continuous domain. Specification D adds a Slope <0.1 % constraint, which further reduces the number of grid points in the premise region.
GWD threshold (m)
Result
Counterexample logit
3.0
Violated
+0.131
3.5
Violated
+1.405
4.0
Violated
+0.062
4.5
Violated
+0.366
5.0
Violated
+1.405
5.5
Violated
+1.405
Table 8: Threshold sensitivity for Specification A (water table depth) against unconstrained XGBoost. The model violates Specification A at every GWD threshold.
Explainable Boosting Machines (EBMs) provide transparent predictions through additive shape functions, enabling direct inspection of feature contributions. However, EBMs can learn non-physical relationships that reduce their reliability in natural hazard applications. This study presents a domain-informed framework to improve the physical consistency of EBMs for lateral spreading prediction. Our approach modifies learned shape functions based on domain knowledge. These modifications correct non-physical behavior while maintaining data-driven patterns. We apply the method to the 2011 Christchurch earthquake dataset and correct non-physical trends observed in the original EBM. The resulting model produces more physically consistent global and local explanations, with an acceptable tradeoff in accuracy (4--5%).
Tree ensembles (TEs) find a multitude of practical applications. They represent one of the most general and accurate classes of machine learning methods. While they are typically quite concise in representation, their operation remains inscrutable to human decision makers. One solution to build trust in the operation of TEs is to automatically identify explanations for the predictions made. Evidently, we can only achieve trust using explanations, if those explanations are rigorous, that is truly reflect properties of the underlying predictor they explain This paper investigates the computation of rigorously-defined, logically-sound explanations for the concrete case of two well-known examples of tree ensembles, namely random forests and boosted trees.
Yacine Izza, Alexey Ignatiev, Xuanxiang Huang +2
National University of Singapore, Singapore · Monash University, Australia · Nanyang Technological University, Singapore +1
We introduce Sequent-Prover, a family of verifier-using language-model agents, and the post-training framework that produces them. Agents reason in an executable SMT-LIB scratchpad: they write complete SMT-LIB programs, query Z3 across turns, inspect solver feedback, repair formalizations, and terminate with an explicit answer. Our recipe, verifier-conditioned trajectory distillation, bootstraps from a noisy teacher proposal policy by sampling multi-turn trajectories, retaining the successful tail that is correct, non-trivial, grounded, and executable, then applying supervised fine-tuning and trajectory-level preference optimization. Because solver success alone does not guarantee semantic faithfulness, we evaluate task accuracy, k-sample reliability, and SMT program quality. Across 37 benchmarks and 7,254 problems per model family, post-training raises the 4B model's per-attempt accuracy from 85.6% to 97.0% and four-sample all-correct reliability (pass^4}) from 64.1% to 91.7%. It also reduces average SMT calls from 4.10 to 2.52 and tokens per attempt from 18.97k to 12.72k. Sequent-Prover agents give answers backed by executable formal artifacts.
Debargha Ganguly, Weicong Chen, Mohsen Hariri +13
Case Western Reserve University · UT Austin · Microsoft Research