SHAP is the most popular explainability tool in machine learning. It assigns importance scores to features, telling practitioners which inputs matter most for a given prediction. Kumar shows that SHAP and formal verification can give actively contradictory conclusions about the same model failure.
The setting is geotechnical hazard prediction — specifically, lateral spreading during earthquakes, trained on 7,291 sites from the 2011 Christchurch earthquake. Four physical specifications are formalized as decidable logical formulas: water table depth, PGA monotonicity, distance safety, and flat-ground safety. Tree-ensemble models (XGBoost and Explainable Boosting Machines) are encoded as logical formulas in an SMT solver, which either proves no violation exists or produces a concrete counterexample.
The key finding: when the SMT solver identifies a counterexample — a specific input where the model violates physics — SHAP can rank the violating feature dead last in importance. The standard explainability pipeline would tell practitioners the model is fine precisely where it is most dangerously wrong. This is not a corner case; it reflects a structural mismatch. SHAP computes local gradients (how much does perturbing this feature change this prediction?), while SMT checks global logical formulas (does this constraint hold across all inputs?). These are different mathematical objects operating on different spaces.
A persistent Pareto frontier emerges across 33 model variants: no architecture achieves both greater than 80% accuracy and full physical compliance. The tension between data-fitting and physical consistency is quantitative, not resolvable by architecture tricks.
Explainability methods and formal verification are not aligned tools at different granularities — they operate on fundamentally different mathematical objects and can reach opposite conclusions about the same failure.