横方向拡がりに対する木構造ベースの機械学習モデルの形式的検証

要旨: 地盤工学的ハザード予測の機械学習モデルは、まばらで偏った訓練データから物理的に一貫しない関係を学習しつつ、高い精度を達成することができる。
現在の対処法（SHAPやLIMEなどの事後説明可能性と、学習時の制約）は、個々の予測を近似的に診断するか、網羅的な保証を提供せずにモデル容量を制限する。
本論文は、学習済みの木のアンサンブルを充足可能性理論（SMT）ソルバーの論理式としてエンコードし、サンプル点だけでなく入力全体の領域に対して物理的仕様を検証する。
4つの地盤工学的仕様（地下水位の深さ、PGAの単調性、距離安全性、および平坦地の安全性）は、決定可能な論理式として形式化され、SMTを介して、XGBoostのアンサンブルとExplainable Boosting Machines（EBMs）の両方に対して検証される。これらは、2011年のクライストチャーチ地震の横方向の拡がりデータセット（7,291地点、4つの特徴量）で訓練されたものである。
SMTソルバーは、仕様が不適合となる具体的な反例を生成するか、違反が存在しないことを証明する。
制約のないEBM（80.1%の精度）は、4つの仕様すべてに違反する。
完全に制約されたEBM（67.2%）は、4つの仕様のうち3つを満たし、検証に導かれた反復的な制約適用が物理的整合性を段階的に向上させることを示している。
33種類のモデル変種のパレート分析は、80%以上の精度と指定された集合への完全な適合の両方を同時に達成した変異が一つもなく、持続的なトレードオフを明らかにしている。
仕様の反例に対するSHAP分析は、問題を引き起こす特徴量が最後に順位付けされる可能性があることを示しており、事後説明は形式的検証の代替にはならないことを示している。
これらの結果は、検証-修正-再検証のエンジニアリングループと、安全性が極めて重要な地盤工学的応用分野において物理的に一貫したMLモデルを展開するための正式な認証を確立する。