Predictive models are being increasingly used to support consequential
decision making at the individual level in contexts such as pretrial bail and
loan approval. As a result, there is increasing social and legal pressure to
provide explanations that help the affected individuals not only to understand
why a prediction was output, but also how to act to obtain a desired outcome.
To this end, several works have proposed optimization-based methods to generate
nearest counterfactual explanations. However, these methods are often
restricted to a particular subset of models (e.g., decision trees or linear
models) and differentiable distance functions. In contrast, we build on
standard theory and tools from formal verification and propose a novel
algorithm that solves a sequence of satisfiability problems, where both the
distance function (objective) and predictive model (constraints) are
represented as logic formulae. As shown by our experiments on real-world data,
our algorithm is: i) model-agnostic ({non-}linear, {non-}differentiable,
{non-}convex); ii) data-type-agnostic (heterogeneous features); iii)
distance-agnostic ($\ell_0, \ell_1, \ell_\infty$, and combinations thereof);
iv) able to generate plausible and diverse counterfactuals for any sample
(i.e., 100% coverage); and v) at provably optimal distances.

该研究提出了一种基于形式验证的算法，使用逻辑公式表示距离函数（目标）和预测模型（约束），解决满足性问题生成最接近的反事实解释，能够生成可行的多样化反事实解释来满足 100% 的覆盖率。