面向横向扩散的基于树的机器学习模型形式化验证

用于地质灾害预测的机器学习模型可实现高准确率，同时从稀疏或偏斜的训练数据中学习出物理不一致的关系。当前的补救措施（如 SHAP 和 LIME 等后置可解释性，以及训练时约束）要么对单个预测进行近似诊断，要么限制模型容量而不提供穷尽性保证。本文将训练好的树集成模型编码为 SMT (Satisfiability Modulo Theories) 求解器中的逻辑公式，并在整个输入域上检查物理规格，而不仅仅是抽样点。将四个地质规格（地下水位深度、PGA 单调性、距离安全、平地安全）形式化为可判定的逻辑公式，并通过 SMT 对基于 2011 年新西兰喀纳斯地震横向扩散数据集（7,291 个场地，四个特征）训练的 XGBoost 集成模型和 Explainable Boosting Machines (EBMs) 进行验证。SMT 求解器要么生成一个具体的反例表明规格失效，要么证明不存在违规情况。未受约束的 EBM（80.1% 准确率）违反所有四个规格。一个完全受约束的 EBM（67.2%）满足三个规格，表明在验证引导下进行迭代约束应用可逐步改善物理一致性。对 33 个模型变体的帕累托分析揭示，存在持久的准确率与规格合规之间的权衡，因为研究的任何变体都未实现同时超过 80% 的准确率和完全符合指定规格集合。SHAP 分析显示，反例的冒犯特征可排在最后，表明后置解释并不足以替代形式化验证。这些结果建立了一个 verify-fix-verify 工程循环，为在安全关键的地质应用中部署物理一致的 ML 模型提供形式化认证。