Counterfactual Explanations (CEs) have emerged as a major paradigm in
explainable AI research, providing recourse recommendations for users affected
by the decisions of machine learning models. However, when slight changes occur
in the parameters of the underlying model, CEs found by existing methods often
become invalid for the updated models. The literature lacks a way to certify
deterministic robustness guarantees for CEs under model changes, in that
existing methods to improve CEs' robustness are heuristic, and the robustness
performances are evaluated empirically using only a limited number of retrained
models. To bridge this gap, we propose a novel interval abstraction technique
for parametric machine learning models, which allows us to obtain provable
robustness guarantees of CEs under the possibly infinite set of plausible model
changes $\Delta$. We formalise our robustness notion as the $\Delta$-robustness
for CEs, in both binary and multi-class classification settings. We formulate
procedures to verify $\Delta$-robustness based on Mixed Integer Linear
Programming, using which we further propose two algorithms to generate CEs that
are $\Delta$-robust. In an extensive empirical study, we demonstrate how our
approach can be used in practice by discussing two strategies for determining
the appropriate hyperparameter in our method, and we quantitatively benchmark
the CEs generated by eleven methods, highlighting the effectiveness of our
algorithms in finding robust CEs.

为了解决因模型变动导致已有方法无效的问题，我们提出了一种用于参数化机器学习模型的新颖区间抽象技术，能够获得可靠的对抗模型变动的证明，进而提供具备可证明健壮性的反事实解释。通过基于混合整数线性规划的验证程序，我们进一步提出了两种算法，生成具备对抗模型变动健壮性的反事实解释，并通过对比实证研究表明，我们的算法在寻找具备健壮性的反事实解释方面具有很好的效果。