Pith. sign in

REVIEW 3 major objections 6 minor 58 references

Most General Explanations of Tree Ensembles (Extended Version)

T0 review · 3 major / 6 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper shows how to compute a maximum inflated abductive explanation for a tree ensemble: the widest region around an input's feature values that still guarantees the model's prediction, found by alternating a coverage-maximizing…

desk verdict Good concept, broken encodings: the MaxSAT/MIP candidates are all empty as written; easy fix, but the paper's central correctness claims don't hold yet. read the letter →

arxiv 2505.10991 v3 pith:CD4AM5BG submitted 2025-05-16 cs.AI cs.LGcs.LO

Yacine Izza , Alexey Ignatiev , Sasha Rubin , Joao Marques-Silva , Peter J. Stuckey This is my paper · ORCID
classification cs.AIcs.LGcs.LO
keywords explainableAIabductiveexplanationsinflatedtreeensemblesrandomforestsboostedtreesimplicithittingsetmaximumsatisfiability
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Formal explanations usually answer 'why this prediction?' with a small set of feature values that, taken together, force the model's decision. This paper asks how wide those values can be made while still forcing the decision, and it defines the best possible answer as a maximum inflated abductive explanation (Max-iAXp): a box of feature intervals $E=E_1\times\cdots\times E_m$ that contains the explained input, guarantees the predicted class, and has the largest feature-space coverage $\mathrm{FSC}_s(E)$ among all valid such boxes. The work shows how to compute this explanation for tree ensembles by alternating two oracles: one that proposes the largest unblocked candidate region, and one that checks the region against an encoding of the trees and returns a counterexample region to block if the candidate is too wide. Experiments on random forests and boosted trees report that the resulting explanations cover substantially more of the input space than ordinary inflated explanations, sometimes by orders of magnitude, with no systematic increase in explanation length. If the construction is correct, a human can be shown one explanation with a precise guarantee that no equally trustworthy explanation covers more of the feature space.

What carries the argument

The central object is the inflated abductive explanation (iAXp): a region $E=E_1\times\cdots\times E_m$ with one interval per feature, containing the instance being explained, such that every input in $E$ is classified as the target class $c$. The load-bearing identity is the minimal hitting-set duality between iAXps and inflated contrastive explanations (iCXps): each iAXp must 'hit' every iCXp in the sense that for some feature its interval is disjoint from the iCXp's interval. Algorithm 1 exploits this duality by priming a MaxSAT/MIP oracle with clauses that block known iCXps, letting the oracle propose the candidate region of maximum coverage $\mathrm{FSC}_s(E)$ that hits all blocked iCXps, and then delegating validity to a second oracle that encodes the tree ensemble. The supporting construction is the split-point cell decomposition: for each feature, the sorted split values define elementary intervals, and Boolean variables of the form $[\![x_i<d]\!]$ together with weighted sum variables encode the class scores, so both the candidate search and the counterexample check reduce to weighted MaxSAT or mixed-integer linear programming.

What would settle it

On a small tree ensemble with finite ordinal domains, enumerate every interval over the raw domain values—not just over split points—and for each interval run the paper's own tree-ensemble checker to see whether it is counterexample-free and larger than Algorithm 1's output. If such an interval exists for any feature, the claim that the returned region is the maximum iAXp is false. A concrete place to look is a feature where the trees use split sets $\{1,3\}$ and $\{2,4\}$; the widest valid interval might need a boundary at, say, 1.5 or 3.5, which the split-point-only representation cannot express.

Watch

Extended reading notes

Core claim

The paper's central claim is that, for any tree ensemble and a chosen size measure $s$, Algorithm 1 returns a Max-iAXp $(X,E)$ satisfying conditions (6)–(7): $E$ is a correct inflated abductive explanation of the instance $(v,c)$, and no other correct inflated abductive explanation has a larger score $\mathrm{FSC}_s(E)=\sum_i \log s(E_i)$. The proof mechanism is a hitting-set duality: every inflated abductive explanation must intersect every inflated contrastive explanation, so the algorithm can be organized as an implicit hitting-set loop. The candidate oracle solves a MaxSAT or MILP problem whose hard constraints enforce that each feature is assigned one interval and whose soft clauses maximize $\mathrm{FSC}_s$; any counterexample returned by the verification oracle is shrunk to an inflated contrastive explanation and blocked by a clause. When the checker finds no counterexample, the duality guarantees the current candidate is an iAXp, and the maximizing character of the candidate oracle makes it a maximum one. The paper also contributes a unified propositional encoding covering majority-vote random forests, weighted-vote random forests, and boosted trees, built on the observation that prediction is constant on the cells cut out by all split points.

Load-bearing premise

The algorithm's optimality guarantee rests on the assumption that the most general valid explanation region can always be built from the elementary intervals between tree split points; if a larger valid region exists that crosses those boundaries, the returned explanation is only the best among cell-aligned candidates, not the most general explanation of the model.

Editorial extensions

If this is right

  • A user can be handed a single formal explanation of a decision with a concrete guarantee: among all inflated abductive explanations, it covers the largest feature-space region under the chosen size measure.
  • The same algorithm and encodings handle majority-vote random forests, weighted-vote random forests, and boosted trees, so the most-general explanation task no longer needs a separate treatment for each ensemble family.
  • Because the coverage score can be weighted by training-data proportions, the 'most general' explanation can be optimized to cover the points a user is actually likely to encounter, not merely geometric volume.
  • On the tested benchmarks the bounds-based encodings solved every instance within the resource limits, with the MILP formulation outperforming the MaxSAT formulation in runtime, which indicates practical scalability for realistic random-forest and boosted-tree models.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A consequence the paper leaves implicit is that the completeness guarantee depends on the claim that the largest valid region can always be expressed as a union of the elementary intervals defined by split points; if that fails for some ensemble, the algorithm would return only the best cell-aligned region, not a globally maximum one.
  • The implicit hitting-set scheme is not tied to trees in principle: any classifier family with a propositional encoding and a way to extract a counterexample region could be plugged into the same candidate/checker loop, so piecewise-linear networks or decision diagrams are natural next targets.
  • Under the uniform product measure used by $\mathrm{FSC}_s$, the 'most general' explanation is a rectangular box that ignores correlations between features; if the true data distribution is correlated, the ranking of explanations could change, suggesting that the reference distribution should be chosen with care.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper defines maximum inflated abductive explanations (Max-iAXp) for tree ensembles: a region E of per-feature intervals that is a correct inflated AXp and that maximizes a feature-space coverage score FSC_s(E). The proposed method is an implicit hitting-set dualization loop: a MaxSAT or MIP oracle proposes a candidate region, a tree-ensemble checker decides whether the region contains a counterexample, and if so the algorithm extracts an inflated CXp and adds blocking clauses to the candidate oracle. Three encodings are presented: a naive interval-variable encoding, a bounds-based encoding, and a MIP reformulation. Experiments on random forests and boosted trees report substantially larger coverage than ordinary iAXps and reasonably low runtimes. The paper also introduces a unified propositional encoding for tree ensembles including weighted-vote random forests.

Significance. If the central correctness claims held, the contribution would be a natural and useful advance in formal XAI: a principled way to compute the most general abductive explanation for a tree-ensemble decision, with a concrete objective and an algorithmic scheme. The paper's strengths are its clear problem formulation, the effort to unify RFmv, RFwv, and boosted trees in one encoding, the public availability of the RFxpl implementation, and the breadth of the empirical study. The experimental coverage ratios (e.g., up to several thousand-fold improvements in Table 2) indicate that the intended method, if correctly encoded, can deliver substantially more general explanations than ordinary iAXps. However, the paper currently contains a load-bearing defect in the published candidate-encoding (Eq. (8) allows the empty region as the optimal MaxSAT solution), and the completeness of the interval restriction is asserted rather than proved. These issues must be fixed before the main claim that Algorithm 1 returns a Max-iAXp is supported.

major comments (3)
  1. [Section 4, Eq. (8) and Algorithm 1, line 3] The hard constraint (8) is "at most one interval per feature" (sum of y^i_{l,u} ≤ 1), and the soft weights w^i_{l,u} = log(Σ_{l≤j≤u} s(I^i_j)) are non-positive because s is a proportion or a data proportion. Consequently the all-false assignment to the y variables satisfies every hard clause and attains objective value 0, which is maximal: no nonempty interval selection can yield a positive contribution. The MaxSAT oracle therefore returns no selected interval, Algorithm 1 line 3 produces E_i = ∅ for every feature, and the returned region is not an iAXp because it fails the requirement v_i ∈ E_i. This is not a minor gap: it invalidates the stated correctness claim that Algorithm 1 computes a Max-iAXp. The same defect is inherited by the bounds-based MaxSAT encoding and the MIP encoding, since they maximize the same objective over the same interval variables without a hard at-least-one constraint. The fix is local (replace ≤ by = in Eq. (8), or add hard clauses/inequalities requiring exactly one interval per feature), but as printed the encodings do not implement the intended candidate oracle.
  2. [Section 3, "key property of a TE", and Algorithm 1, candidate generation] The candidate search restricts each E_i to a union of the elementary intervals I^i_j, but the paper only states that predictions are constant on products of these intervals. It does not prove the converse completeness property needed for the Max-iAXp claim: that for every region E satisfying (3), the cell-aligned hull of E (obtained by expanding each E_i to the nearest split points in S_i) also satisfies (3) and has FSC_s(E) at least as large. Without such a lemma, the algorithm optimizes only over a restricted family of regions, and conditions (6)–(7) are not established. The paper should state and prove this lemma explicitly, since the maximality claim depends on it.
  3. [Algorithm 1, correctness and termination discussion] The text after Algorithm 1 asserts that when the checker finds no counterexample the candidate is the maximum inflated AXp, and that MHS duality guarantees termination. This argument is informal and is not stated as a theorem. In particular, the claim that the candidate oracle "finds the largest unblocked interval for each iteration that maximizes FSC_s(E)" presupposes a correct candidate encoding (which Eq. (8) does not provide), and it also requires a proof that any larger iAXp is never blocked by previously discovered counterexamples. With the currently published encoding, the termination claim cannot even be tested because the first oracle call returns the empty region. A formal theorem stating termination and the postcondition (6)–(7) is needed.
minor comments (6)
  1. [Abstract and Section 2.2] There are typos: "fall withing" in the abstract and "mononotic" in the definition of a size measure; both should be corrected.
  2. [Equation (7)] The symbol F CSs(E) in Eq. (7) is a typo for FSC_s(E); the notation should be made consistent.
  3. [Section 4, Example 6] Example 6 states "We require at most one y^4_{l,u} to be true," repeating the defective constraint instead of the intended exactly-one semantics described in the surrounding text.
  4. [Algorithm 1, line 5] The checker call "hasCEx ← ¬ WiAXp(E; X, E)" uses the symbol WiAXp without a formal definition anywhere in the paper; the intended meaning should be stated explicitly.
  5. [Section 5.3 and Table 4] The text and table headers contain typos "RFww" and "RFwm" where "RFwv" is meant.
  6. [Section 4, bounds-based encoding] In the bounds-based encoding, the equivalences defining y^i_{l,u} do not by themselves force one interval to be selected; the paper should state explicitly which hard clauses enforce the exactly-one condition for the bound variables as well.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation found; Max-iAXp is defined and optimized independently, with the self-cited iAXp/iCXp duality serving only as a supporting lemma, not as an input equivalent to the result.

full rationale

The central claim is that Algorithm 1 computes a maximum inflated abductive explanation under the pre-defined coverage objective FSC_s. Section 4 defines FSC_s(E) = sum_i log s(E_i) and then defines Max-iAXp via conditions (6)-(7); the candidate-generation MaxSAT/MIP models maximize exactly this objective, and the checker independently tests condition (3) using the TE encoding. No parameter is fitted to the quantity being predicted, and no equation defining the output is reused as its own proof. The only self-cited item is the iAXp/iCXp hitting-set duality of [Izza et al., 2024b], quoted as 'A consequence of the MHS duality between iAXp's and iCXp's [Izza et al., 2024b] is that the checker oracle reports a new candidate to be an iAXp and the algorithm terminates'. This is a prior formal theorem used as a termination/duality lemma, not an assumption equivalent to the Max-iAXp result; the optimality argument rests on the independent checker and on the fact that a correct iAXp cannot contain any witnessed counterexample, so it is never blocked. I also note that the paper's naive encoding hard-constraint (8) uses 'at most one interval' with non-positive log-proportion weights, so as written the MaxSAT optimum could select no interval; that is an internal consistency and correctness concern about the published encodings, not a circularity, because the definition of Max-iAXp and the optimization objective are not being assumed into existence by the algorithm's output.

Assumptions & free parameters 2 free parameters · 2 assumptions · 0 invented entities

The central result rests on two imported or asserted premises (iCXp duality and cell-completeness) plus a user-chosen size measure; the paper introduces no new physical entities or fitted physical constants.

free parameters (2)
  • size measure s = prop or data (user choice)
    FSC_s(E) in Eq. (5) and the definition of Max-iAXp in (6)-(7) depend on this choice; the 'most general' explanation is optimal only for the chosen measure, and experiments use coverage percentage (prop).
  • infinite-domain size |D_i| = training data range max-min
    Defined in Section 4: for non-finite domains, |D_i| = max{vi in T} - min{vi in T}; this changes prop(E) and therefore which region is considered maximum.
assumptions (2)
  • domain assumption Minimal hitting set duality between iAXps and iCXps (Proposition 1)
    Imported from prior work [Izza et al., 2024b]; termination and optimality of Algorithm 1 rest on it.
  • domain assumption Prediction is constant on every elementary cell of the split-point partition, and any maximal explanation region is a union of such cells
    Used to justify restricting candidates to unions of elementary intervals; stated as 'the key property of a TE' in Section 3 but not proved.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Most General Explanations of Tree Ensembles (Extended Version)." pith.science (2026). https://pith.science/paper/CD4AM5BG

@misc{pith2026250510991,
  author       = {Pith},
  title        = {Pith review of: Most General Explanations of Tree Ensembles (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CD4AM5BG}},
  note         = {Machine review of arXiv:2505.10991}
}
read the original abstract

Explainable Artificial Intelligence (XAI) is critical for attaining trust in the operation of AI systems. A key question of an AI system is ``why was this decision made this way''. Formal approaches to XAI use a formal model of the AI system to identify abductive explanations. While abductive explanations may be applicable to a large number of inputs sharing the same concrete values, more general explanations may be preferred for numeric inputs. So-called inflated abductive explanations give intervals for each feature ensuring that any input whose values fall withing these intervals is still guaranteed to make the same prediction. Inflated explanations cover a larger portion of the input space, and hence are deemed more general explanations. But there can be many (inflated) abductive explanations for an instance. Which is the best? In this paper, we show how to find a most general abductive explanation for an AI decision. This explanation covers as much of the input space as possible, while still being a correct formal explanation of the model's behaviour. Given that we only want to give a human one explanation for a decision, the most general explanation gives us the explanation with the broadest applicability, and hence the one most likely to seem sensible. (The paper has been accepted at IJCAI2025 conference.)

Figures

Figures reproduced from arXiv: 2505.10991 by the authors.

Figure 1
Figure 1. Example of a simple RF trained using Scikit-learn w [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Example of a simple boosted tree (BT) generated by X [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

58 extracted references · 52 canonical work pages

  1. [1]

    On pixel-wise explanations for non-linear classifier decisions by layer-wise relevanc e propagation

    [Bach et al., 2015] Sebastian Bach, Alexander Binder, Gr´ egoire Montavon, Frederick Klauschen, Klaus-Robert M¨ uller, and Wojciech Samek. On pixel-wise explanations for non-linear classifier decisions by layer-wise relevanc e propagation. PloS one, 10(7):e0130140,

    work page 2015

  2. [11]

    Solving MAXSA T by solving a sequence of simpler SA T instances

    [Davies and Bacchus, 2011 ] Jessica Davies and Fahiem Bac- chus. Solving MAXSA T by solving a sequence of simpler SA T instances. In CP, pages 225–239,

    work page 2011

  3. [12]

    Friedman

    [Friedman, 2001] Jerome H. Friedman. Greedy function ap- proximation: A gradient boosting machine. The Annals of Statistics, 29(5):1189–1232,

    2001

  4. [13]

    Suf- ficient reasons for classifier decisions in the presence of domain constraints

    [Gorji and Rubin, 2022 ] Niku Gorji and Sasha Rubin. Suf- ficient reasons for classifier decisions in the presence of domain constraints. In AAAI, pages 5660–5667,

    work page 2022

  5. [15]

    On the failings of shapley values for explainability

    [Huang and Marques-Silva, 2024 ] Xuanxiang Huang and Jo˜ ao Marques-Silva. On the failings of shapley values for explainability. Int. J. Approx. Reason. , 171:109112,

    work page 2024

  6. [16]

    Solving explainability queries with quantification: The case of feature relevancy

    [Huang et al., 2023] Xuanxiang Huang, Y acine Izza, and Jo˜ ao Marques-Silva. Solving explainability queries with quantification: The case of feature relevancy. In AAAI, pages 3996–4006,

    work page 2023

  7. [17]

    Liffiton, and Joao Marques-Silva

    [Ignatiev et al., 2015] Alexey Ignatiev, Alessandro Previti, Mark H. Liffiton, and Joao Marques-Silva. Smallest MUS extraction with minimal hitting set dualization. In CP, pages 173–182,

    work page 2015

  8. [18]

    PySA T: A python toolkit for pro- totyping with SA T oracles

    [Ignatiev et al., 2018] Alexey Ignatiev, Ant´ onio Morgado, and Joao Marques-Silva. PySA T: A python toolkit for pro- totyping with SA T oracles. In SAT, pages 428–437,

    work page 2018

Show all 58 references
  1. [21]

    Towards universally accessible SA T tech- nology

    [Ignatiev et al., 2024] Alexey Ignatiev, Zi Li Tan, and Chris- tos Karamanos. Towards universally accessible SA T tech- nology. In SAT, pages 4:1–4:11,

    2024

  2. [22]

    Towards trustable explain- able AI

    [Ignatiev, 2020] Alexey Ignatiev. Towards trustable explain- able AI. In IJCAI, pages 5154–5158,

    2020

  3. [23]

    On explaining random forests with SA T

    [Izza and Marques-Silva, 2021 ] Y acine Izza and Joao Marques-Silva. On explaining random forests with SA T. In IJCAI, pages 2584–2591,

    2021

  4. [24]

    Efficient contrastive explanations on demand

    [Izza and Marques-Silva, 2024 ] Y acine Izza and Joao Marques-Silva. Efficient contrastive explanations on demand. CoRR, abs/2412.18262,

    2024 arXiv

  5. [25]

    On tackling explanation redundancy in de- cision trees

    [Izza et al., 2022] Y acine Izza, Alexey Ignatiev, and Jo˜ ao Marques-Silva. On tackling explanation redundancy in de- cision trees. J. Artif. Intell. Res. , 75:261–321,

    2022

  6. [26]

    A new class of explanations for classifiers with non-binary features

    [Ji and Darwiche, 2023 ] Chunxi Ji and Adnan Darwiche. A new class of explanations for classifiers with non-binary features. In JELIA, pages 106–122,

    2023

  7. [27]

    Towards trustable SHAP scores

    [L´ etoff´ eet al., 2025] Olivier L´ etoff´ e, Xuanxiang Huang, and Jo˜ ao Marques-Silva. Towards trustable SHAP scores. In AAAI, pages 18198–18208,

    2025

  8. [30]

    Lundberg and Su-In Lee

    [Lundberg and Lee, 2017 ] Scott M. Lundberg and Su-In Lee. A unified approach to interpreting model predictions. In NeurIPS, pages 4765–4774,

    2017

  9. [32]

    Delivering trustworthy AI through formal XAI

    [Marques-Silva and Ignatiev, 2022] Jo˜ ao Marques-Silva and Alexey Ignatiev. Delivering trustworthy AI through formal XAI. In AAAI, pages 12342–12350,

    2022

  10. [33]

    Logic-based ex- plainability in machine learning

    [Marques-Silva, 2022] Jo˜ ao Marques-Silva. Logic-based ex- plainability in machine learning. In Reasoning W eb, pages 24–104,

    2022

  11. [34]

    Logic-based ex- plainability: Past, present and future

    [Marques-Silva, 2024] Jo˜ ao Marques-Silva. Logic-based ex- plainability: Past, present and future. In ISoLA, volume 15222, pages 181–204,

    2024

  12. [35]

    Explanation in artificial intelli- gence: Insights from the social sciences

    [Miller, 2019] Tim Miller. Explanation in artificial intelli- gence: Insights from the social sciences. Artif. Intell. , 267:1–38,

    2019

  13. [36]

    Interpretable machine learning

    [Molnar, 2020] Christoph Molnar. Interpretable machine learning

    2020

  14. [37]

    Olson, William La Cava, Pa- tryk Orzechowski, Ryan J

    [Olson et al., 2017] Randal S. Olson, William La Cava, Pa- tryk Orzechowski, Ryan J. Urbanowicz, and Jason H. Moore. PMLB: a large benchmark suite for machine learn- ing evaluation and comparison. BioData Mining, 10(1):36,

    2017

  15. [38]

    Scikit-learn: Machine learning in Python

    [Pedregosa and et al., 2011 ] Fabian Pedregosa and et al. Scikit-learn: Machine learning in Python. Journal of Ma- chine Learning Research, 12:2825–2830,

    2011

  16. [39]

    Partial MUS enumeration

    [Previti and Marques-Silva, 2013 ] Alessandro Previti and Joao Marques-Silva. Partial MUS enumeration. In AAAI, pages 818–825,

    2013

  17. [40]

    ”why should I trust you?”: Explain- ing the predictions of any classifier

    [Ribeiro et al., 2016] Marco T´ ulio Ribeiro, Sameer Singh, and Carlos Guestrin. ”why should I trust you?”: Explain- ing the predictions of any classifier. In KDD, pages 1135– 1144,

    2016

  18. [41]

    Anchors: High-precision model- agnostic explanations

    [Ribeiro et al., 2018] Marco T´ ulio Ribeiro, Sameer Singh, and Carlos Guestrin. Anchors: High-precision model- agnostic explanations. In AAAI, pages 1527–1535,

    2018

  19. [43]

    Stop explaining black box machine learning models for high stakes decisions and use interpretable models instead

    [Rudin, 2019] Cynthia Rudin. Stop explaining black box machine learning models for high stakes decisions and use interpretable models instead. Nature Machine Intelligence, 1(5):206–215,

    2019

  20. [44]

    Implicit hitting set algorithms for re a- soning beyond NP

    [Saikko et al., 2016] Paul Saikko, Johannes Peter Wallner, and Matti Jarvisalo. Implicit hitting set algorithms for re a- soning beyond NP. In KR, pages 104–113,

    2016

  21. [45]

    Towards explainable artificial intelligence

    [Samek and M¨ uller, 2019] Wojciech Samek and Klaus- Robert M¨ uller. Towards explainable artificial intelligence. In Samek et al. [2019], pages 5–22. [Samek et al., 2019] Wojciech Samek, Gr´ egoire Montavon, Andrea V edaldi, Lars Kai Hansen, and Klaus-Robert M¨ uller, editors....

    2019

  22. [46]

    Anders, and Klaus- Robert M¨ uller

    [Samek et al., 2021] Wojciech Samek, Gr´ egoire Montavon, Sebastian Lapuschkin, Christopher J. Anders, and Klaus- Robert M¨ uller. Explaining deep neural networks and be- yond: A review of methods and applications. Proc. IEEE, 109(3):247–278,

    2021

  23. [47]

    Prediction is deduction but explanation is abduction

    [Shanahan, 1989] Murray Shanahan. Prediction is deduction but explanation is abduction. In IJCAI, pages 1055–1060,

    1989

  24. [49]

    Fooling LIME and SHAP: adversarial attacks on post hoc explanation methods

    [Slack et al., 2020] Dylan Slack, Sophie Hilgard, Emily Jia, Sameer Singh, and Himabindu Lakkaraju. Fooling LIME and SHAP: adversarial attacks on post hoc explanation methods. In AIES, pages 180–186,

    2020

  25. [50]

    Swartout

    [Swartout, 1977] William R. Swartout. A digitalis therapy advisor with explanations. In IJCAI, pages 819–825,

    1977

  26. [53]

    The computational complexity of understanding binary classifier decisions

    [W¨ aldchenet al., 2021] Stephan W¨ aldchen, Jan MacDonald, Sascha Hauch, and Gitta Kutyniok. The computational complexity of understanding binary classifier decisions. J. Artif. Intell. Res., 70:351–387,

    2021

  27. [54]

    [Wu et al., 2023] Min Wu, Haoze Wu, and Clark W . Barrett. V erix: Towards verified explainability of deep neural net- works. In NeurIPS,

    2023

  28. [55]

    [Wu et al., 2024] Min Wu, Xiaofu Li, Haoze Wu, and Clark W . Barrett. Better verified explanations with appli- cations to incorrectness and out-of-distribution detecti on. CoRR, abs/2409.03060,

    2024

  29. [56]

    Copy number variation in plasma as a tool for lung cancer prediction using extreme gradient boosting (xgboost) classifier

    [Y uet al., 2020] Daping Y u, Zhidong Liu, Chongyu Su, Yi Han, XinChun Duan, Rui Zhang, Xiaoshuang Liu, Y ang Y ang, and Shaofa Xu. Copy number variation in plasma as a tool for lung cancer prediction using extreme gradient boosting (xgboost) classifier. Thoracic cancer , 11(1):95–102,

    2020

  30. [57]

    [Y uet al., 2023b] Jinqiang Y u, Alexey Ignatiev, and Peter J. Stuckey. On formal feature attribution and its approxima- tion. CoRR, abs/2307.03380,

    arXiv

  31. [58]

    [Y uet al., 2024] Jinqiang Y u, Graham Farr, Alexey Ignatiev, and Peter J. Stuckey. Anytime approximate formal feature attribution. In SAT, pages 30:1–30:23, 2024

    2024

  32. [1977]

    Swartout

    [Swartout, 1983] William R. Swartout. XPLAIN: A system for creating and explaining expert consulting programs. Artif. Intell., 21(3):285–325,

    1983

  33. [1983]

    https://archive.ics.uci.edu/ml,

    [UCI, 2020] UCI Machine Learning Repository. https://archive.ics.uci.edu/ml,

    2020

  34. [1989]

    A symbolic approach to explaining bayesian net- work classifiers

    [Shih et al., 2018] Andy Shih, Arthur Choi, and Adnan Dar- wiche. A symbolic approach to explaining bayesian net- work classifiers. In IJCAI, pages 5103–5111,

    2018

  35. [2001]

    Karp, Erick Moreno-Centeno, and Santosh S

    [Chandrasekaran et al., 2011] Karthekeyan Chandrasekaran, Richard M. Karp, Erick Moreno-Centeno, and Santosh S. V empala. Algorithms for implicit hitting set problems. In SODA, pages 614–629,

    2011

  36. [2003]

    Logic for explainable AI

    [Darwiche, 2023] Adnan Darwiche. Logic for explainable AI. In LICS, pages 1–11,

    2023

  37. [2005]

    To- wards formal XAI: formally approximate minimal expla- nations of neural networks

    [Bassan and Katz, 2023 ] Shahaf Bassan and Guy Katz. To- wards formal XAI: formally approximate minimal expla- nations of neural networks. In TACAS, pages 187–207,

    2023

  38. [2011]

    XGBoost: A scalable tree boosting system

    [Chen and Guestrin, 2016 ] Tianqi Chen and Carlos Guestrin. XGBoost: A scalable tree boosting system. In KDD, pages 785–794,

    2016

  39. [2013]

    Liffiton, Alessandro Previti, Ammar Malik, and Jo˜ ao Marques-Silva

    [Liffiton et al., 2016] Mark H. Liffiton, Alessandro Previti, Ammar Malik, and Jo˜ ao Marques-Silva. Fast, flexible MUS enumeration. Constraints An Int. J., 21(2):223–250,

    2016

  40. [2015]

    [Bailey and Stuckey, 2005] James Bailey and Peter J. Stuckey. Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In PADL, pages 174–186,

    2005

  41. [2016]

    Clarke, Orna Grum- berg, Somesh Jha, Y uan Lu, and Helmut V eith

    [Clarke et al., 2003] Edmund M. Clarke, Orna Grum- berg, Somesh Jha, Y uan Lu, and Helmut V eith. Counterexample-guided abstraction refinement for sym- bolic model checking. J. ACM, 50(5):752–794,

    2003

  42. [2017]

    Explainability is not a game

    [Marques-Silva and Huang, 2024 ] Joao Marques-Silva and Xuanxiang Huang. Explainability is not a game. Com- mun. ACM, 67(7):66–75, jul

    2024

  43. [2018]

    Interpretable machine learning: Fundamental prin- ciples and 10 grand challenges

    [Rudin et al., 2022] Cynthia Rudin, Chaofan Chen, Zhi Chen, Haiyang Huang, Lesia Semenova, and Chudi Zhong. Interpretable machine learning: Fundamental prin- ciples and 10 grand challenges. Statistics Surveys , 16:1– 85,

    2022

  44. [2019]

    From con- trastive to abductive explanations and back again

    [Ignatiev et al., 2020] Alexey Ignatiev, Nina Narodytska, Nicholas Asher, and Joao Marques-Silva. From con- trastive to abductive explanations and back again. In AIxIA, pages 335–355,

    2020

  45. [2020]

    Stuckey, and Jo˜ ao Marques-Silva

    [Ignatiev et al., 2022] Alexey Ignatiev, Y acine Izza, Peter J. Stuckey, and Jo˜ ao Marques-Silva. Using MaxSA T for ef- ficient explanations of tree ensembles. In AAAI, pages 3776–3785,

    2022

  46. [2021]

    Lobo, Vignesh Viswanathan, and Y air Zick

    [Biradar et al., 2024] Gagan Biradar, Y acine Izza, Elita A. Lobo, Vignesh Viswanathan, and Y air Zick. Axiomatic aggregations of abductive explanations. In AAAI, pages 11096–11104,

    2024

  47. [2022]

    Gurobi Optimizer Reference Manual,

    [Gurobi Optimization, LLC, 2023 ] Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual,

    2023

  48. [2023]

    Handbook of Satisfi- ability - Second Edition

    [Biere et al., 2021] Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfi- ability - Second Edition

    2021

  49. [2024]

    Random forests

    [Breiman, 2001] Leo Breiman. Random forests. Mach. Learn., 45(1):5–32,

    2001

  50. [2025]

    Liffiton and Ammar Ma- lik

    [Liffiton and Malik, 2013 ] Mark H. Liffiton and Ammar Ma- lik. Enumerating infeasibility: Finding multiple muses quickly. In CPAIOR, pages 160–175,

    2013

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.