Pith. sign in

REVIEW 5 major objections 5 minor 51 references

Efficient Contrastive Explanations on Demand

T0 review · 5 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

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

Pith's one-line read Parallelized adversarial-example queries make contrastive explanations practical for large neural networks.

desk verdict A parallel dichotomic search for distance-restricted contrastive explanations that is fast in practice; the algorithmic core holds up, but a MaxSAT formulation typo and silent timeout handling need fixing. read the letter →

arxiv 2412.18262 v1 pith:C6V7RQE7 submitted 2024-12-24 cs.LG

Yacine Izza , Joao Marques-Silva This is my paper · ORCID
classification cs.LG
keywords contrastiveexplanationsdistance-restrictedadversarialrobustnessneuralnetworkverificationdichotomicsearchparallelalgorithmsfeatureimportanceexplainableAI
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

This paper sets out to make formal contrastive explanations — the "why not this other class?" question — computable for deep neural networks with tens of thousands of features. Its central proposal, the SwiftCXp algorithm, runs many adversarial-example queries in parallel and uses a feature-disjunction heuristic to certify several features as essential at once. The authors report that this approach finds one contrastive explanation on every tested benchmark, including a convolutional MNIST network where the standard dichotomic search times out on all instances. If the results hold, contrastive explanations become a practical byproduct of adversarial robustness verification rather than a separate, much harder problem.

What carries the argument

The machinery is the distance-restricted contrastive explanation itself (Definition 2): a subset-minimal set Y of features that, when all features outside Y are fixed to their instance values, admits a point within l_p distance ϵ of the instance that changes the prediction. The algorithms assume a robust oracle FindAdvEx that answers, for any set of fixed features, whether such a point exists. SwiftCXp combines parallel dichotomic search over ordered feature chunks with a feature-disjunction heuristic adapted from the clause-D (CLD) correction-set algorithm, so that a single round of oracle calls can certify many features as essential. All claims of minimality rest on the oracle's answers being exact.

What would settle it

Take a network and a sample for which SwiftCXp reports a dCXp; re-verify the reported set with an independent, exact robustness checker that runs without a timeout, and also re-check each feature removed along the way. If any reported set is not actually subset-minimal, or permits no class change within the stated distance, the central claim fails.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that computing one distance-restricted contrastive explanation (dCXp) can be reduced to a small number of parallel calls to a complete adversarial-example oracle, and that the number of calls can be further cut by a disjunctive feature check. Algorithm 2 (SwiftCXp) maintains a set S of features already known to be essential and an interval of candidate features W; each inner iteration partitions W into q chunks and queries the oracle on each boundary in parallel, then zooms into the chunk containing the transition feature. When few features remain, Algorithm 3 tests q features at once and, if all are essential, moves them all into S. The paper reports that SwiftCXp returns a dCXp on all tests in under 4 hours on the largest network (average 932.8 seconds), whereas the baseline dichotomic algorithm fails on every test of the convolutional models.

Load-bearing premise

The algorithms assume that every call to the adversarial-example oracle returns a definitive yes-or-no answer, but the implementation runs each query under a four-hour timeout and does not say how timed-out or undecided calls are handled, so the minimality of every returned explanation depends on an oracle that may not be complete.

Editorial extensions

If this is right

  • Distance-restricted contrastive explanations for image-sized networks become feasible: the largest convolutional network in the experiments receives one explanation in about 16 minutes on average, with no timeouts.
  • Explanation computation inherits improvements in adversarial-robustness solvers; any faster complete verifier directly reduces the time to produce a dCXp.
  • The feature-disjunction check can shrink the remaining candidate set rapidly when the target explanation is large, so the method is strongest exactly in the regime where sequential search is slowest.
  • The MARCO-style enumeration and the smallest-dCXp formulations give a route to feature-importance scores and provably minimal contrastive explanations on top of the same oracle.
  • With the same oracle, the authors' results imply that the gap between adversarial robustness and formal explainability is now mainly a degree of parallelism, not a difference in difficulty.

Reading between the lines

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

  • The same parallel-chunking plus disjunction strategy should transfer to abductive explanations (sufficient reasons), since dAXp extraction also calls the same oracle; the paper's own enumeration experiments already treat both sides symmetrically.
  • A reader should expect the measured speedups to depend on the oracle's exactness: if the verifier ever returns "unknown" or times out internally, the returned set may be a contrastive set certified only up to the verifier's precision, not a formal dCXp.
  • The gaussian-like feature sharing reported among enumerated explanations hints that a small core of pixels explains most decisions; if confirmed across datasets, it would justify predicting explanations from previous ones rather than recomputing from scratch.
  • The 30-versus-1 core comparison in the experiments makes the headline runtime gap partly a parallelization result; a natural test is to give the baseline the same core budget.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

5 major / 5 minor

Summary. The paper proposes exact algorithms for computing distance-restricted contrastive explanations (dCXps) of neural-network classifiers by querying an oracle for constrained adversarial examples. Its central algorithmic contribution is SwiftCXp (Algorithm 2), a parallelized dichotomic search combined with a feature-disjunction heuristic (Algorithm 3). The paper also presents MARCO-style enumeration (Algorithm 4), a MaxSMT/MaxSAT formulation for smallest dCXps, and an abstraction-refinement procedure (Algorithm 5). Experiments on MNIST and GTSRB networks report that SwiftCXp succeeds on all tested instances, including the largest network mnist-conv, where the dichotomic baseline times out on all tests.

Significance. If the algorithmic claims were correct, the paper would be a meaningful step toward making formal contrastive explanations practical for image-sized networks: it directly links the computation of dCXps to the availability of exact robustness oracles and demonstrates that parallelized dichotomic search can drastically reduce the wall-clock time needed to find one explanation. The feature-disjunction heuristic is an interesting analogue of clause-D search for contrastive explanations, and the enumeration experiments with feature-attribution scores illustrate a useful downstream application. However, the current version contains load-bearing correctness gaps in the central algorithm and in the MaxSAT claim, and the experimental comparison is not resource-neutral; these issues must be repaired before the practical claims can be accepted. The paper does not yet ship code (it announces release after acceptance), so reproducibility currently rests on the pseudocode and the experimental description.

major comments (5)
  1. [Section 3.2, Algorithm 2] The update rules on lines 14-15 invert the intended dichotomy. Under the paper's convention, AE_i = FindAdvEx(ϵ, F \ (S ∪ W_{1..i})) is monotone non-decreasing in i: increasing i frees more features, making the adversarial-existence predicate easier. The invariant dWCXp(S∪W_{1..u}) therefore requires AE_u=true, and the transition feature is the first index t with AE_t=true. The correct parallel update is u ← min({i∈D | AE_i=true} ∪ {u}) and ℓ ← max({i∈D | AE_i=false} ∪ {ℓ}). As printed, line 14 moves u to a false index. For example, if AE_1=false and AE_2=AE_3=true with D={1,2,3}, the first inner iteration sets u=1; line 16 then returns S=∅ if FindAdvEx(ϵ,F\∅) is true, and if it is false line 18 returns S={1}, which is not a dWCXp because AE_1=false. Hence the published Algorithm 2 does not compute a dCXp even with a perfect oracle; the correctness proof and the implementation must use the corrected update rule.
  2. [Section 4.2, Claim 1] Claim 1 is false as stated because the hard constraint B uses κ(x)=c rather than κ(x)≠c. A dCXp is defined through the existence of x with κ(x)≠c (Definition 2, Eq. (9)), but the MaxSMT/MaxSAT formulation requires the classification to remain c. With B as printed, the assignment x=v and s_i=1 for all i∈F satisfies every hard and soft clause, so the solver returns the empty set as the 'smallest CXp' independent of the adversarial behavior. Replacing κ(x)=c by κ(x)≠c would make the formulation consistent with Definition 2, but as written the claim does not follow.
  3. [Section 3.1 and Section 5.1] The correctness of every returned dCXp is certified by calls to an exact oracle FindAdvEx. The implementation, however, uses MN-BaB/Gurobi with a 4-hour time limit per test, and the paper never states how timed-out or inconclusive verifier calls are processed. If a timeout is treated as a negative answer, the minimality of the reported explanation can be invalid; if it is treated as positive, the algorithm may return a set that is not a dCXp. This issue needs to be resolved in the algorithm description, and the experiments should report how many individual oracle calls hit the timeout.
  4. [Section 5.1 and Table 1] The performance comparison is unbalanced: the baseline dichotomic search uses 2 cores (1 oracle process plus 1 control process), while SwiftCXp uses 30 processes (Table 1 caption), and the setup text mentions 60 cores for the parallel runs. The conclusion that SwiftCXp 'significantly outperforms the dichotomic search on all tested benchmarks' conflates algorithmic speedup with parallelism. An equal-core baseline or a per-core efficiency measure is needed to support the claimed comparison.
  5. [Section 4.2, Algorithm 5] Algorithm 5 is not executable as printed: line 6 tests ¬WCXp(Y, ϵ; E) but Y is never defined in the procedure, and the comment 'S ⊇ dAXp' suggests the intended test concerns the complement F\S rather than an undefined Y. Because the abstraction-refinement procedure is one of the stated contributions for computing smallest dCXps, this needs to be corrected and its correctness argument supplied.
minor comments (5)
  1. [Section 3.2, Algorithm 2] The output type is described as 'a dAXp S' in the text and algorithm header, but the algorithm computes a dCXp; the labels should be corrected.
  2. [Algorithms 1 and 2] The notation F \ S ∪ W_{1..i} is ambiguous; use F \ (S ∪ W_{1..i}) consistently for the set of fixed features.
  3. [Section 3.2, Algorithm 2] The text says the lower and upper bounds ℓ and u are initialized to 1 and |W|, while the pseudocode initializes ℓ=0; the text and pseudocode should be aligned.
  4. [Table 1] The table title says 'computing dAXp' while Section 5.2 reports dCXp results, and the '—' entries in the GTSRB rows of the Dichotomic columns are not explained in the caption.
  5. [Section 2, Proposition 1] Proposition 1(2) does not quantify x in the consequent; as written, the bound ∥y−v∥≤∥x−v∥ refers to an x that is not introduced in the premise.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the algorithms are evaluated against an external robustness oracle and no claimed output reduces to the inputs by construction.

full rationale

The paper's central claim is algorithmic and empirical: it proposes SwiftCXp for computing distance-restricted contrastive explanations using calls to an external robustness oracle. The distance-restricted definitions and MHS duality are adopted from prior work (Izza et al. 2024a; Ignatiev et al. 2020), but these are stated definitions and established results with explicitly given assumptions, not conclusions derived from the present paper's own outputs. No parameter is fitted to the data and then renamed as a prediction: the heuristic feature order and the feature-disjunction threshold affect runtime but do not determine whether the returned set is a dCXp, which is certified by the external oracle. The experimental comparison against the sequential dichotomic baseline is an independent benchmark, not a consequence of the definitions. The skeptical observation about Algorithm 2's update rule, if correct, would be a soundness bug rather than circularity, since the apparent flaw would make the algorithm return a non-dCXp, not merely reproduce an input. Overall, the derivation chain does not exhibit any step where an explanation, performance gain, or theorem reduces by construction to the paper's own inputs, fitted values, or self-citations. Score 0.

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

The paper adds no fitted physical constants and no invented entities. Its load-bearing assumptions are inherited from prior formal-XAI work (distance-restricted explanations, MHS duality) and from the availability of exact robustness oracles. The free parameters delta and q are experimental knob settings that affect runtime, not correctness.

free parameters (2)
  • delta (threshold for feature disjunction) = 0.75 to 0.9 per dataset/distance
    Chosen manually in the experiments to activate the FeatDisjunct optimization in later SwiftCXp iterations; no sensitivity analysis is reported.
  • q (number of parallel oracle calls) = 30 for all models
    Fixed number of processes for SwiftCXp experiments; controls chunking of the feature set and is not justified by a scaling analysis.
assumptions (4)
  • domain assumption dAXp/dCXp definitions and MHS duality (Proposition 2) from Izza et al. 2024a are adopted without proof.
    The paper builds on the distance-restricted explanation framework from prior work; the enumeration and smallest-explanation algorithms rely on this duality.
  • standard math The adversarial-example existence predicate is monotone with respect to freeing features, so dichotomic search over feature indices is valid.
    Required for the binary-search invariants in Algorithms 1 and 2; it follows from the logical form of Eq. (9), but is not stated as a lemma.
  • domain assumption A complete robustness oracle FindAdvEx is available for constrained adversarial examples in the chosen lp norm.
    All algorithms treat oracle calls as exact yes/no decisions; no handling of incomplete or timed-out verifier responses is described (Sections 3.1 and 5.1).
  • domain assumption The ML model used in the MaxSMT/MaxSAT formulation can be logically encoded in the solver's theory.
    Claim 1 in Section 4.2 requires a logical encoding of the classifier and distance constraints; this is available for some model families but not all.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Efficient Contrastive Explanations on Demand." pith.science (2026). https://pith.science/paper/C6V7RQE7

@misc{pith2026241218262,
  author       = {Pith},
  title        = {Pith review of: Efficient Contrastive Explanations on Demand},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/C6V7RQE7}},
  note         = {Machine review of arXiv:2412.18262}
}
read the original abstract

Recent work revealed a tight connection between adversarial robustness and restricted forms of symbolic explanations, namely distance-based (formal) explanations. This connection is significant because it represents a first step towards making the computation of symbolic explanations as efficient as deciding the existence of adversarial examples, especially for highly complex machine learning (ML) models. However, a major performance bottleneck remains, because of the very large number of features that ML models may possess, in particular for deep neural networks. This paper proposes novel algorithms to compute the so-called contrastive explanations for ML models with a large number of features, by leveraging on adversarial robustness. Furthermore, the paper also proposes novel algorithms for listing explanations and finding smallest contrastive explanations. The experimental results demonstrate the performance gains achieved by the novel algorithms proposed in this paper.

Figures

Figures reproduced from arXiv: 2412.18262 by the authors.

Figure 1
Figure 1. Visualize Feature Attribution-based Contrastive explanations for image datasets: MNIST and GTSRB. References ACM. Fathers of the deep learning revolution receive ACM A. M. Turing award. https://awards.acm.org/ about/2018-turing, 2019. BBC. British-Canadian AI expert Geoffrey Hinton wins Turing award. https://www.bbc.com/news/ technology-47721129, 2024. BBC. ’godfather of ai’ shares Nobel physics prize. https://www.b… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

51 extracted references · 44 canonical work pages

  1. [1]

    Fathers of the deep learning revolution receive ACM A

    ACM. Fathers of the deep learning revolution receive ACM A. M. T uring award. https://awards.acm.org/about/2018-turing, 2019

    work page 2018

  2. [2]

    British- C anadian AI expert G eoffrey H inton wins T uring award

    BBC. British- C anadian AI expert G eoffrey H inton wins T uring award. https://www.bbc.com/news/technology-47721129, 2024

    work page 2024

  3. [3]

    'godfather of ai' shares N obel physics prize

    BBC. 'godfather of ai' shares N obel physics prize. https://www.bbc.com/news/articles/c62r02z75jyo, 2024

    work page 2024

  4. [4]

    Google D eep M ind boss wins N obel for proteins breakthrough

    BBC. Google D eep M ind boss wins N obel for proteins breakthrough. https://www.bbc.com/news/articles/czrm0p2mxvyo, 2024

    work page 2024

  5. [5]

    Handbook of Satisfiability - Second Edition

    Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition . 2021

    work page 2021

  6. [6]

    Lobo, Vignesh Viswanathan, and Yair Zick

    Gagan Biradar, Yacine Izza, Elita A. Lobo, Vignesh Viswanathan, and Yair Zick. Axiomatic aggregations of abductive explanations. In AAAI , pages 11096--11104, 2024

    work page 2024

  7. [7]

    Johnson, and Changliu Liu

    Christopher Brix, Mark Niklas M \" u ller, Stanley Bak, Taylor T. Johnson, and Changliu Liu. First three years of the international verification of neural networks competition (VNN-COMP) . Int. J. Softw. Tools Technol. Transf. , 25(3):329--339, 2023

    work page 2023

  8. [8]

    Logic for explainable AI

    Adnan Darwiche. Logic for explainable AI . In LICS , pages 1--11, 2023

    2023

Show all 51 references
  1. [9]

    The mnist database of handwritten digit images for machine learning research

    Li Deng. The mnist database of handwritten digit images for machine learning research. IEEE Signal Processing Magazine , 29(6):141--142, 2012

    2012

  2. [10]

    Claudio Ferrari, Mark Niklas M \" u ller, Nikola Jovanovic, and Martin T. Vechev. Complete verification via multi-neuron relaxation guided branch-and-bound. In ICLR , 2022

    2022

  3. [11]

    Gurobi Optimizer Reference Manual , 2023

    Gurobi Optimization, LLC . Gurobi Optimizer Reference Manual , 2023

    2023

  4. [12]

    Extracting MUCs from constraint networks

    Fred Hemery, Christophe Lecoutre, Lakhdar Sais, and Fr \' e d \' e ric Boussemart. Extracting MUCs from constraint networks. In ECAI , pages 113--117, 2006

    2006

  5. [13]

    Horn and Charles R

    Roger A. Horn and Charles R. Johnson. Matrix Analysis, 2nd Ed . Cambridge University Press, 2012

    2012

  6. [14]

    From decision trees to explained decision sets

    Xuanxiang Huang and Jo \ a o Marques - Silva. From decision trees to explained decision sets. In ECAI , pages 1100--1108, 2023

    2023

  7. [15]

    From robustness to explainability and back again

    Xuanxiang Huang and Jo \ a o Marques - Silva. From robustness to explainability and back again. CoRR , abs/2306.03048, 2023

    2023 arXiv

  8. [16]

    On efficiently explaining graph-based classifiers

    Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, and Jo \ a o Marques - Silva. On efficiently explaining graph-based classifiers. In KR , pages 356--367, 2021

    2021

  9. [17]

    SAT -based rigorous explanations for decision lists

    Alexey Ignatiev and Joao Marques - Silva. SAT -based rigorous explanations for decision lists. In SAT , pages 251--269, 2021

    2021

  10. [18]

    Abduction-based explanations for machine learning models

    Alexey Ignatiev, Nina Narodytska, and Joao Marques - Silva. Abduction-based explanations for machine learning models. In AAAI , pages 1511--1519, 2019

    2019

  11. [19]

    From contrastive to abductive explanations and back again

    Alexey Ignatiev, Nina Narodytska, Nicholas Asher, and Joao Marques - Silva. From contrastive to abductive explanations and back again. In AIxIA , pages 335--355, 2020

    2020

  12. [20]

    Stuckey, and Jo \ a o Marques - Silva

    Alexey Ignatiev, Edward Lam, Peter J. Stuckey, and Jo \ a o Marques - Silva. A scalable two stage approach to computing optimal decision sets. In AAAI , pages 3806--3814, 2021

    2021

  13. [21]

    Stuckey, and Jo \ a o Marques - Silva

    Alexey Ignatiev, Yacine Izza, Peter J. Stuckey, and Jo \ a o Marques - Silva. Using MaxSAT for efficient explanations of tree ensembles. In AAAI , pages 3776--3785, 2022

    2022

  14. [22]

    On explaining random forests with SAT

    Yacine Izza and Joao Marques - Silva. On explaining random forests with SAT . In IJCAI , pages 2584--2591, 2021

    2021

  15. [23]

    On computing relevant features for explaining nbcs

    Yacine Izza and Jo \ a o Marques - Silva. On computing relevant features for explaining nbcs. pages 75--86, 2023

    2023

  16. [24]

    On explaining decision trees

    Yacine Izza, Alexey Ignatiev, and Joao Marques - Silva. On explaining decision trees. CoRR , abs/2010.11034, 2020

    2010 arXiv

  17. [25]

    On tackling explanation redundancy in decision trees

    Yacine Izza, Alexey Ignatiev, and Jo \ a o Marques - Silva. On tackling explanation redundancy in decision trees. J. Artif. Intell. Res. , 75:261--321, 2022

    2022

  18. [26]

    Cooper, and Jo \ a o Marques - Silva

    Yacine Izza, Alexey Ignatiev, Nina Narodytska, Martin C. Cooper, and Jo \ a o Marques - Silva. Provably precise, succinct and efficient explanations for decision trees. CoRR , abs/2205.09569, 2022

    2022 arXiv

  19. [27]

    Cooper, and Jo \ a o Marques - Silva

    Yacine Izza, Xuanxiang Huang, Alexey Ignatiev, Nina Narodytska, Martin C. Cooper, and Jo \ a o Marques - Silva. On computing probabilistic abductive explanations. Int. J. Approx. Reason. , 159:108939, 2023

    2023

  20. [28]

    Distance-Restricted Explanations: Theoretical Underpinnings & Efficient Implementation

    Yacine Izza, Xuanxiang Huang, Antonio Morgado, Jordi Planes, Alexey Ignatiev, and Joao Marques-Silva. Distance-Restricted Explanations: Theoretical Underpinnings & Efficient Implementation . In KR , pages 475--486, 2024

    2024

  21. [29]

    Stuckey, and Jo \ a o Marques - Silva

    Yacine Izza, Alexey Ignatiev, Peter J. Stuckey, and Jo \ a o Marques - Silva. Delivering inflated explanations. In AAAI , pages 12744--12753, 2024

    2024

  22. [30]

    Meel, and Jo \ a o Marques - Silva

    Yacine Izza, Kuldeep S. Meel, and Jo \ a o Marques - Silva. Locally-minimal probabilistic explanations. In ECAI , volume 392, pages 1092--1099, 2024

    2024

  23. [31]

    From SHAP scores to feature importance scores

    Olivier Letoffe, Xuanxiang Huang, Nicholas Asher, and Jo \ a o Marques - Silva. From SHAP scores to feature importance scores. CoRR , abs/2405.11766, 2024

    2024 arXiv

  24. [32]

    On correcting SHAP scores

    Olivier Letoffe, Xuanxiang Huang, and Jo \ a o Marques - Silva. On correcting SHAP scores. In AAAI , 2024

    2024

  25. [33]

    Liffiton, Alessandro Previti, Ammar Malik, and Jo \ a o Marques - Silva

    Mark H. Liffiton, Alessandro Previti, Ammar Malik, and Jo \ a o Marques - Silva. Fast, flexible MUS enumeration. Constraints An Int. J. , 21(2):223--250, 2016

    2016

  26. [34]

    Reasoning about inconsistent formulas

    Jo \ a o Marques - Silva and Carlos Menc \' a. Reasoning about inconsistent formulas. In IJCAI , pages 4899--4906, 2020

    2020

  27. [35]

    On computing minimal correction subsets

    Jo \ a o Marques - Silva, Federico Heras, Mikol \' a s Janota, Alessandro Previti, and Anton Belov. On computing minimal correction subsets. In IJCAI , pages 615--622, 2013

    2013

  28. [36]

    Minimal sets over monotone predicates in boolean formulae

    Jo \ a o Marques - Silva, Mikol \' a s Janota, and Anton Belov. Minimal sets over monotone predicates in boolean formulae. In CAV , pages 592--607, 2013

    2013

  29. [37]

    Minimal sets on propositional formulae

    Jo \ a o Marques - Silva, Mikol \' a s Janota, and Carlos Menc \' a. Minimal sets on propositional formulae. problems and reductions. Artif. Intell. , 252:22--50, 2017

    2017

  30. [38]

    Cooper, Alexey Ignatiev, and Nina Narodytska

    Jo \ a o Marques - Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, and Nina Narodytska. Explaining naive bayes and other linear classifiers with polynomial time and delay. In NeurIPS , 2020

    2020

  31. [39]

    Logic-based explainability in machine learning

    Jo \ a o Marques - Silva. Logic-based explainability in machine learning. In Reasoning Web , pages 24--104, 2022

    2022

  32. [40]

    Logic-based explainability: Past, present and future

    Jo \ a o Marques - Silva. Logic-based explainability: Past, present and future. In ISoLA , pages 181--204, 2024

    2024

  33. [41]

    Explanation in artificial intelligence: Insights from the social sciences

    Tim Miller. Explanation in artificial intelligence: Insights from the social sciences. Artif. Intell. , 267:1--38, 2019

    2019

  34. [42]

    Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala

    Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas K \" o pf, Edward Z. Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Stei...

    2019

  35. [43]

    why should I trust you?

    Marco T \' u lio Ribeiro, Sameer Singh, and Carlos Guestrin. "why should I trust you?": Explaining the predictions of any classifier. In KDD , pages 1135--1144, 2016

    2016

  36. [44]

    An introduction to abstract algebra

    Derek JS Robinson. An introduction to abstract algebra . Walter de Gruyter, 2003

    2003

  37. [45]

    A symbolic approach to explaining bayesian network classifiers

    Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining bayesian network classifiers. In IJCAI , pages 5103--5111, 2018

    2018

  38. [46]

    Johannes Stallkamp, Marc Schlipsing, Jan Salmen, and Christian Igel. Man vs. computer: Benchmarking machine learning algorithms for traffic sign recognition. Neural Networks , 32:323--332, 2012

    2012

  39. [47]

    Min Wu, Haoze Wu, and Clark W. Barrett. VeriX : Towards verified explainability of deep neural networks. CoRR , abs/2212.01051, 2022

    2022 arXiv

  40. [48]

    Min Wu, Haoze Wu, and Clark W. Barrett. Verix: Towards verified explainability of deep neural networks. In NeurIPS , 2023

    2023

  41. [49]

    Min Wu, Xiaofu Li, Haoze Wu, and Clark W. Barrett. Better verified explanations with applications to incorrectness and out-of-distribution detection. CoRR , abs/2409.03060, 2024

    2024

  42. [50]

    Jinqiang Yu, Alexey Ignatiev, and Peter J. Stuckey. On formal feature attribution and its approximation. CoRR , abs/2307.03380, 2023

    2023 arXiv

  43. [51]

    Jinqiang Yu, Graham Farr, Alexey Ignatiev, and Peter J. Stuckey. Anytime approximate formal feature attribution. In SAT , pages 30:1--30:23, 2024

    2024

Pith tools

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