Pith. sign in

REVIEW 2 major objections 6 minor 14 references

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations

T0 review · 2 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read An explanation verified on a neuron-merged miniature network is provably sufficient for the original network, and iterative refinement recovers the same minimal explanation in 36–56% less time.

desk verdict Novel and plausible abstraction-refinement for provable explanations, but the algorithm as written depends on an unstated counterexample-extraction step the backend likely can't provide. read the letter →

arxiv 2506.08505 v1 pith:WQI7PX5H submitted 2025-06-10 cs.LG cs.AIcs.LO

Shahaf Bassan , Yizhak Yisrael Elboher , Tobias Ladner , Matthias Althoff , Guy Katz This is my paper
classification cs.LGcs.AIcs.LO
keywords provablysufficientexplanationsneuralnetworkverificationabstractionrefinementminimalneuronmergingformalexplainabilitycounterexample-guided
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

The paper aims to make 'provably sufficient' explanations — subsets of input features whose fixed values guarantee the predicted class never changes under perturbation of everything else — practical for real neural networks. Its strategy is to compute the explanation on a much smaller abstract network first, merging neurons that behave alike, because an explanation proven on the abstract network is automatically proven on the original; when the abstract check fails, the network is gradually enlarged until the final explanation is certified as both sufficient and minimal. The paper's claim is that this abstraction-refinement ladder returns exactly the same minimal explanation as the standard verification-heavy greedy method, at 36–56% lower computation time on MNIST, CIFAR-10, and GTSRB. A reader should care because it turns a formal but computationally prohibitive explanation method into an interactive one, and because each intermediate abstraction level is itself a certified explanation, offering a time-to-insight dial.

What carries the argument

An abstract neural network: a reduced network in which groups of neurons that behave similarly over the perturbed input region are replaced by a single neuron, with the discarded weights folded into biases via Minkowski sums (Lemma 1) so that the abstract output is a set enclosing the original network's output for every input in the region. The load-bearing fact is the enclosure property f(xS;x̃S̄) ∈ f′(xS;x̃S̄) for all x̃ in the εp ball, which turns any strict class separation in the abstract network (sufficiency of S for f′, Def. 3) into a strict class separation in the original (Prop. 1). The refinement ladder carries the rest of the argument: re-splitting merged neurons in 10% steps of the reduction rate ρ tightens the enclosure (f(xS;x̃S̄) ∈ f′′(xS;x̃S̄) ⊂ f′(xS;x̃S̄)), so explanations on the refined network are subsets of the earlier ones and remain sufficient for the original, until the chain reaches the original network and exact greedy minimality.

What would settle it

Re-run the benchmark suite with both algorithms on the same images and identical feature ordering and compare the returned feature sets: any image on which Algorithm 2's minimal explanation differs from Algorithm 1's would refute Proposition 5. In the same run, log each failed abstract sufficiency check: if the verifier ever reports a violation without returning a concrete input inside the εp ball, or returns an input that the original network still classifies as the target class, then the refinement branch cannot execute as written for over-approximating verifiers.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that sufficiency survives neuron-merging abstraction: for a query ⟨f,x,S,εp⟩ — the assertion that fixing the features in S to their values guarantees the network's predicted class stays the same for every perturbation of the remaining features within an εp ball — an abstract network f′ built by merging similarly behaving neurons satisfies suff(f′,x,S,εp) ⇒ suff(f,x,S,εp) (Prop. 1). Minimality does not survive abstraction, so the paper adds refinement: re-splitting merged neurons produces a network f′′ whose output enclosure is strictly tighter, every sufficient explanation for f′′ remains sufficient for f, and sufficient explanations for f′′ are subsets of those for f′ (Props. 2–3), with minimality transferring down the chain (Prop. 4). The headline result (Prop. 5) is that Algorithm 2 — a greedy deletion loop that tests each candidate feature removal on the current abstraction, refines the abstraction whenever the abstract check fails, and evaluates purported counterexamples on the original network — terminates with the same minimal sufficient explanation as Algorithm 1 run on the original network, because refinement eventually reproduces the original network exactly. The experiments claim this equality of outcomes at 36–56% lower computation cost, with certified intermediate explanations at every abstraction level.

Load-bearing premise

The refinement loop only works if every failed sufficiency check on the reduced network comes with a concrete input example that actually produces the failure; over-approximating verifiers can report violations that no real input causes, and the paper does not describe how such a counterexample would be extracted.

Editorial extensions

If this is right

  • Provably sufficient and provably minimal explanations become computable in 36–56% less wall-clock time on the tested image benchmarks (MNIST, CIFAR-10, GTSRB), so the formal guarantee stops being the bottleneck that limits explanation methods to tiny networks.
  • Under a time budget, the method returns smaller explanations than the standard greedy algorithm: at equal timeouts it produced substantially smaller subsets (for example, 204 versus 409 features on MNIST), because coarse abstractions let more features be processed early.
  • A user can halt early with a certified explanation: every intermediate abstraction level yields an explanation that is provably sufficient for the original network, though not yet proven minimal.
  • Because the method's queries are ordinary neural-network verification queries on smaller networks, any future speedup in verifiers transfers directly to faster provable explanations.
  • The monotone ladder from coarse to fine also serves as an interpretation device: the sequence of explanations shrinking with each refinement step shows which features are essential at every scale.

Reading between the lines

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

  • Beyond the paper's reported experiments, the fixed 10%-step refinement schedule could be made adaptive: choosing the next reduction rate from the slack in the failed abstract check would trade the number of refinement queries ξ against per-query time, a trade-off the paper's O((n+ξ)·maxt) bound makes explicit but does not optimize.
  • A natural further use of the ladder is a necessity ordering of features: features that persist in the explanation at ρ near 100% are the explanatory core, while features dropped at coarse ρ are peripheral — the paper stops at the minimal subset and does not pursue this ranking, but its data already show features being freed at different rates.
  • The reported speed-ups were obtained with a set-based over-approximating verifier; re-running with an exact, counterexample-producing verifier would clarify how much of the gain survives when spurious violations cannot be resolved by cheap refinement — a comparison the paper does not make.
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

2 major / 6 minor

Summary. This paper proposes an abstraction-refinement algorithm (Alg. 2) for computing minimal sufficient explanations of neural network predictions. Starting from a coarse abstract network obtained by the neuron-merging construction of Ladner and Althoff (2023), the algorithm greedily tries to remove features, checking sufficiency on the current abstract network. If an abstract check succeeds, the feature is removed; if it fails, the algorithm attempts to use a counterexample to decide whether the feature is indispensable, and otherwise refines the abstraction by increasing the reduction rate ρ. The main theoretical claims are that any sufficient explanation of an abstract network is also sufficient for the original network (Prop. 1), that refined networks produce tighter enclosures (Prop. 2), and that the algorithm converges to the same minimal explanation as the standard greedy baseline (Prop. 5). Experiments on MNIST, CIFAR-10, and GTSRB report 36–56% reductions in computation time over the baseline, plus ablations on perturbation radius, feature ordering, activation functions, and network size.

Significance. If the correctness results hold, this is a valuable contribution to formal explainability: it transfers a well-studied abstraction technique from formal verification to explanation computation, offers provable sufficiency and minimality guarantees, and provides an interpretable sequence of explanations at different abstraction levels. The paper is honest about the dependence on verification tool scalability, and the experimental design does not appear to be tuned to force the speedup. Nonetheless, the present version has two load-bearing weaknesses: the algorithm's reliance on concrete counterexample generation from an over-approximating set-based verifier is not substantiated, and the proof of the refinement containment (Prop. 2) is only a sketch. If the authors can close these gaps, the contribution would be a solid advance in the field.

major comments (2)
  1. [Sec. 4, Alg. 2 (lines 8–13); Sec. 5; Sec. B.2] The branch structure of Alg. 2 depends on the verification backend being able to return a concrete input x̃ that witnesses the failure of suff(f′,x,S\{i},εp), so that the output of f(x̃) can be compared with t in line 9. The paper states that CORA is used as the backend (Sec. 5) and gives no description of how such witnesses are extracted from CORA's set-based, over-approximating reachability analysis; an over-approximation violation does not in general correspond to a realizable input. Without this step, lines 8–10 are not executable, and the proof of Prop. 5 in A.6, which reasons about the absence of a counterexample, does not apply to the implemented algorithm. This is a load-bearing gap: either the authors must show that CORA (or their wrapper) produces sound concrete witnesses, or they must modify the algorithm to refine on every abstract failure, in which case the reported 36–56% time reduction may no longer hold and the experiments would need to be re-run.
  2. [Appendix A.3, proof of Prop. 2] The proof of Prop. 2 is a paragraph sketch. The strict containment f″(x; x̃) ⊂ f′(x; x̃) is justified by the statement that 'as all additionally merged neurons N′\N″ in f′ induce outer approximations and everything else is equal,' but no inductive argument is given to show that the neuron-merging construction of Lemma 1 is monotone with respect to the set of merged neurons when the input bounds and downstream layers are taken into account. Since Prop. 3, and therefore the invariant used in Prop. 5, relies on this containment, the central correctness claim is not fully proven. The statement may be true, but a formal proof is required.
minor comments (6)
  1. [Section A.2, proof of Prop. 1] The final sentence 'we conclude that f′(xS ; ˜x′ ¯S )∈f′(xS ; ˜x′ ¯S ) must be true' contains a typo; the left-hand side should be f(xS ; ˜x′ ¯S ), not f′(xS ; ˜x′ ¯S ).
  2. [Section A.5, proof of Prop. 4] The reasoning is garbled; a correct argument should state that if S′⊂S is sufficient for f′′, then by Prop. 1 it is sufficient for f, contradicting the minimality of S. Please rewrite this proof.
  3. [Table 1 caption] The timeout values '100s, 103s, and 104s' should be typeset as 10^2 s, 10^3 s, and 10^4 s (or equivalent) for clarity.
  4. [Table 3 header] The header contains a typo: 'Paramater' should be 'Parameter'.
  5. [Section 5.1] The reported speedups '−41% for MNIST, −36% for CIFAR-10, −56% for GTSRB' are stated without specifying how they are aggregated over the 100 images; please define the metric precisely.
  6. [Figure 6] The x-axis is labeled 'Nr. of processed features' while the caption describes 'percentage of processed features'; please align the label and the description.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the abstraction-soundness proof rests on an independent neuron-merging containment lemma restated in the paper, and the efficiency gains are empirical against the standard greedy baseline.

full rationale

The derivation chain is not circular. The only bridge from the abstract network to the original network is Prop. 1 (suff(f',x,S,eps_p) implies suff(f,x,S,eps_p)), whose proof reduces to showing that f(x_S;x~_notS) is contained in f'(x_S;x~_notS) for every perturbed input. That containment is established in A.2 by induction using the neuron-merging construction of Lemma 1, which is restated in full in A.1: W'_k := W_k(B_k,.), b'_k+1 = b_k+1 + W_k+1(.,B_k)I_k(B_k), and H*_{k+1} is a subset of H'_{k+1}. Lemma 1 is prior work by two co-authors, but it is a self-contained, parameter-free containment theorem about merged neurons; it contains no mention of sufficiency, minimality, or explanations, so citing it is a dependency, not an import of the paper's own conclusion. Props. 2-5 are then derived with proofs in A.3-A.6, and none of them equates the abstraction output to the target explanation by definition. Definitions 4 and 5 are explicitly labeled definitions (abstract and refined sufficient explanations), not claimed derivations. The reported 36-56% time savings are empirical measurements against the standard greedy Alg. 1 on the same CORA backend; the 10% reduction-rate schedule is a design choice and no fitted parameter is relabeled as a prediction. The reviewer concern about extracting concrete counterexamples from a set-based over-approximating verifier is a real soundness or executability question about the algorithm's interface with CORA, but it is not circularity because it does not make the theorem's conclusion equal to its assumptions.

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

The central claim rests on two external building blocks: the neuron-merging abstraction lemma from co-authored prior work and the verifier's counterexample-generation capability. Both are domain assumptions rather than facts proved in this paper. There are two hand-chosen design parameters (reduction schedule, feature ordering) that affect the results but are not fitted constants. No new physical or conceptual entities are introduced.

free parameters (2)
  • reduction-rate schedule (ρ from 10% to 100% in 10% steps) = 10% steps, starting at 10%
    This schedule controls the granularity of refinement and was fixed for all benchmarks; results (explanation size and runtime) depend on it, and no sensitivity analysis beyond the fixed steps is reported.
  • feature ordering = descending sensitivity (main), Shapley and in-order in ablation
    The greedy algorithm's output minimal explanation depends on feature order; the paper adopts the sensitivity ordering from Wu et al. 2023, with ablation showing different explanation sizes and computation times.
assumptions (3)
  • domain assumption Lemma 1 (Neuron-Merging Construction) from Ladner & Althoff 2023, Prop. 4: merging neurons with interval bounds yields an outer approximation H*_{k+1} ⊆ H′_{k+1}.
    The soundness of Prop. 1 relies entirely on this lemma, which is cited from co-authored prior work and not reproved in this paper.
  • domain assumption The neural network verifier (CORA) is sound and can produce a concrete input counterexample whenever an abstract sufficiency query fails.
    Alg. 2 lines 8-13 require a witness x′ from the abstract verifier; the paper does not prove or cite that CORA's set-based analysis provides such witnesses.
  • domain assumption Neuron merging can be applied to ReLU and sigmoid activations with the same soundness guarantees.
    The abstraction is defined for general element-wise activations, but the merging relies on layer-wise interval bounds; experiments use sigmoid and ReLU, and the appendix does not discuss limitations for other activations.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations." pith.science (2026). https://pith.science/paper/WQI7PX5H

@misc{pith2026250608505,
  author       = {Pith},
  title        = {Pith review of: Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WQI7PX5H}},
  note         = {Machine review of arXiv:2506.08505}
}
read the original abstract

Despite significant advancements in post-hoc explainability techniques for neural networks, many current methods rely on heuristics and do not provide formally provable guarantees over the explanations provided. Recent work has shown that it is possible to obtain explanations with formal guarantees by identifying subsets of input features that are sufficient to determine that predictions remain unchanged using neural network verification techniques. Despite the appeal of these explanations, their computation faces significant scalability challenges. In this work, we address this gap by proposing a novel abstraction-refinement technique for efficiently computing provably sufficient explanations of neural network predictions. Our method abstracts the original large neural network by constructing a substantially reduced network, where a sufficient explanation of the reduced network is also provably sufficient for the original network, hence significantly speeding up the verification process. If the explanation is in sufficient on the reduced network, we iteratively refine the network size by gradually increasing it until convergence. Our experiments demonstrate that our approach enhances the efficiency of obtaining provably sufficient explanations for neural network predictions while additionally providing a fine-grained interpretation of the network's predictions across different abstraction levels.

Figures

Figures reproduced from arXiv: 2506.08505 by the authors.

Figure 1
Figure 1. Demonstration of an abstraction-based explanation process. As the size of the abstract network [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Running example. a) Original network with winner class [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Running example (cont.). c) Minimal sufficient explanation for the original network (c.1) which is insufficient for [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (12 more)
Figure 4
Figure 4. Figure 4: The explanation size over cumulative time for MNIST, CIFAR10, and GTSRB, throughout the entire abstraction [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]
Figure 5
Figure 5. Figure 5: Examples of explanations at varying reduction rates for MNIST, CIFAR-10, and GTSRB. [PITH_FULL_IMAGE:figures/full_fig_p008_5.png]
Figure 6
Figure 6. Figure 6: The percentage of processed features—either included or excluded from the explanation—over cumulative time, [PITH_FULL_IMAGE:figures/full_fig_p008_6.png]
Figure 7
Figure 7. Figure 7: An example of a full abstraction refinement procedure using the tighter Minkowski sum instead of the weighted [PITH_FULL_IMAGE:figures/full_fig_p017_7.png]
Figure 8
Figure 8. Figure 8: The percentage of features successfully processed—identified as either included or excluded from the explana [PITH_FULL_IMAGE:figures/full_fig_p019_8.png]
Figure 9
Figure 9. Figure 9: The explanation size over cumulative time for MNIST, CIFAR10, and GTSRB, segmented by reduction rate, [PITH_FULL_IMAGE:figures/full_fig_p019_9.png]
Figure 10
Figure 10. Figure 10: Original images compared to images featuring the complete abstraction-refinement grid at various abstraction [PITH_FULL_IMAGE:figures/full_fig_p020_10.png]
Figure 11
Figure 11. Figure 11: A step-by-step visualization of the different abstraction levels for both the network and explanation across [PITH_FULL_IMAGE:figures/full_fig_p021_11.png]
Figure 12
Figure 12. Figure 12: Visual comparisons of sufficiency and minimality of explanations. [PITH_FULL_IMAGE:figures/full_fig_p021_12.png]
Figure 13
Figure 13. Figure 13: An autonomous aircraft taxiing scenario ( [PITH_FULL_IMAGE:figures/full_fig_p023_13.png]
Figure 14
Figure 14. Figure 14: Varying results of explanations across different abstraction levels for the Taxinet benchmark. [PITH_FULL_IMAGE:figures/full_fig_p024_14.png]
Figure 15
Figure 15. Figure 15: (a) The percentage of features successfully processed—identified as either included or excluded from the [PITH_FULL_IMAGE:figures/full_fig_p024_15.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

14 extracted references · 12 canonical work pages

  1. [1]

    17 Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations Table 3: Dimensions for the MNIST classifier. Layer type Paramater Activation Input784×200Sigmoid Fully-connected200×200Sigmoid Fully-connected200×200Sigmoid Fully-connected200×200Sigmoid Fully-connected200×200Sigmoid Fully-connected200×200Sigmoid Fully-connected200×200Sigmo...

    work page 2023

  2. [3]

    Clarke, E., Grumberg, O., Jha, S., Lu, Y ., and Veith, H

    Technical Report.https://arXiv:2411.08875. Clarke, E., Grumberg, O., Jha, S., Lu, Y ., and Veith, H. Counterexample-Guided Abstraction Refinement. In Proc. 12th Int. Conf. on Computer Aided Verification (CAV), pp. 154–169,

    arXiv

  3. [4]

    Probabilistic Stability Guarantees for Feature Attributions

    Technical Report.https://arXiv:2504.13787. Julian, K., Lee, R., and Kochenderfer, M. Validation of Image-Based Neural Network Controllers through Adap- tive Stress Testing. In2Proc. 23rd IEEE Int. Conf. on Intelligent Transportation Systems (ITSC), pp. 1–7,

    work page Pith review arXiv

  4. [6]

    20 Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations Network size ρ = 10% 20% 30% 40% 50% 60% 70% 80% 90% 100% (a) Original image (b) ρ ≤ 10% (c) ρ ≤ 30% (d) ρ ≤ 50% (e) ρ ≤ 80% (f) Original network Explanation size increases Network size ρ and computation time increases Figure 11: A step-by-step visualization of the different...

    work page

  5. [8]

    Definition 6(Neural Network).Letx∈R n0 be the input of a neural networkfwithκlayers, its outputy:=f(x)∈R nκ is obtained as follows: h0 :=x,h k :=L k (hk−1),y=h κ, k∈[κ], where Lk :R nk−1 →R nk represents the operation of layer k and is given by Lk (hk−1) :=σ(W khk−1 +b k) with weight matrixW k ∈R nk×nk−1, biasb k ∈R nk, activation functionσ:R nk →R nk, an...

    work page 2023

  6. [9]

    Analyzing different network sizes While the previous experiment already show the scalability of our approach on different network sizes (Sec

    C.4. Analyzing different network sizes While the previous experiment already show the scalability of our approach on different network sizes (Sec. B), the networks are on different datasets. In this study, we show results comparing three networks taken from the Marabou benchmark of VNN-COMP (Brix et al., 2023), which all have CIFAR-10 images as input (Tab...

    work page 2023

  7. [11]

    Choice of Activation Function In our main experiments, we used networks with either ReLU or sigmoid activation, respectively (Sec

    C.3. Choice of Activation Function In our main experiments, we used networks with either ReLU or sigmoid activation, respectively (Sec. B). While this networks are taken from VNN-COMP (Brix et al., 2023), we provide a full picture in this study including both activation functions for both networks in Tab

    work page 2023

  8. [13]

    traditional

    which ran a “traditional” computation of a provably sufficient explanation for neural networks over the Taxinet benchmark, which is a real-world safety-critical airborne navigation system (Julian et al., 2020). The authors of (Wu et al.,

    work page 2020

Show all 14 references
  1. [14]

    We additionally provide visualizations for some of our obtained explanations (Fig

    (8814.85 seconds, and explanation size was not reported). We additionally provide visualizations for some of our obtained explanations (Fig. 13 and 14). Extension to language tasks.We present results from experiments conducted on the safeNLP benchmark (Casadio et al., 2025), t...

    2025

  2. [2009]

    https://www.cs.toronto.edu/ ~kriz/learning-features-2009-TR.pdf

    Tech- nical Report. https://www.cs.toronto.edu/ ~kriz/learning-features-2009-TR.pdf. La Malfa, E., Zbrzezny, A., Michelmore, R., Paoletti, N., and Kwiatkowska, M. On Guaranteed Optimal Robust Explanations for NLP Models. InProc. Int. Joint Conf. on Artificial Intelligence (IJC...

    2009

  3. [2017]

    Logic-Based Explainability in Machine Learning

    Marques-Silva, J. Logic-Based Explainability in Machine Learning. InReasoning Web. Causality, Explanations and Declarative Knowledge: 18th Int. Summer School 2022, Berlin, Germany, September 27–30, 2022, Tutorial Lectures, pp. 24–104

    2022

  4. [2023]

    LeCun, Y

    Technical Report.https://arXiv:2305.01932. LeCun, Y . The MNIST Database of Handwritten Digits, 1998.http://yann.lecun.com/exdb/mnist/. Liu, J., Xing, Y ., Shi, X., Song, F., Xu, Z., and Ming, Z. Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Net...

    1998 arXiv

  5. [2024]

    What makes an Ensemble (Un) Interpretable? InProc

    Bassan, S., Amir, G., Zehavi, M., and Katz, G. What makes an Ensemble (Un) Interpretable? InProc. 42nd Int. Conf. on Machine Learning (ICML), 2025a. Bassan, S., Eliav, R., and Gur, S. Explain Yourself, Briefly! Self-Explaining Neural Networks with Concise Sufficient Reasons. I...

    arXiv

  6. [2025]

    https://arXiv:2502.02719

    Technical Report. https://arXiv:2502.02719. Barceló, P., Monet, M., Pérez, J., and Subercaseaux, B. Model Interpretability Through the Lens of Computa- tional Complexity.Proc. 33rd Int. Conf. on Advances in Neural Information Processing Systems (NeurIPS), pp. 15487–15498,

    arXiv

Pith tools

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