{"id":"06f7628f-4985-4717-b34a-b8281637f264","arxiv_id":"2412.18262","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"Parallelized dichotomic search with feature-disjunction pruning computes distance-restricted contrastive explanations for deep neural networks far faster than a sequential baseline, demonstrated on MNIST and GTSRB.","lead":"This paper presents algorithms that compute formal contrastive explanations for neural network predictions by reusing adversarial robustness solvers, and reports large speedups on MNIST and GTSRB image classifiers. The methods make symbolic explanations, which are often too slow for large networks, more practical, though this preprint is explicitly labeled as a timestamp against copycats.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Algorithm 2 lines 14–15 invert the update: u is set to the first false oracle result while the invariant requires u to be a true index, so the published SwiftCXp can return a non-dCXp. This undermines the central correctness claim independent of oracle timeouts.","rationale":"The single most load-bearing concern is not the oracle timeout handling, which the reader identified, but an internal inconsistency in Algorithm 2 that breaks the algorithm's correctness even with a perfect oracle. The paper's central claim is that SwiftCXp computes one dCXp and outperforms the dichotomic baseline. If the published pseudocode can return a set S for which dWCXp(S) is false, then the algorithm as described does not implement what is evaluated, and the reproducibility and formal validity of the central claim collapse. The reader's weakest assumption about timed-out verifier calls is real but secondary: fixing that would not fix the update-rule inversion. A concrete implementation test on a toy example with an exact oracle would settle the question immediately. If the test confirms the bug, the paper cannot be accepted in its current form; it would need a corrected algorithm, a rigorous invariant proof, and re-run experiments. The underlying idea of parallelized dichotomic search is plausible and a one-line fix (replacing AEi=false by AEi=true in line 14) may restore correctness, but as written the formal contribution is unsupported. Therefore the appropriate verdict moves from CONDITIONAL to REJECT pending major revision and re-review.","tokens_in":14779,"tokens_out":14013,"duration_ms":122011,"concrete_test":"Implement Algorithm 2 exactly as printed (including lines 14–15) and run it on a small classifier with an exact brute-force AEx oracle and a known dCXp, e.g., the l1-bounded running example in Section 2 or a three-feature ReLU network. Check whether the returned S satisfies dWCXp(S) and is subset-minimal. If it fails, the published algorithm is incorrect; if it passes, the pseudocode needs a clarifying rewrite.","verdict_should_be":"REJECT","load_bearing_attack":"In Algorithm 2 (line 8) the invariant is dWCXp(S∪W1..u), i.e., the oracle predicate AEu = FindAdvEx(ϵ, F\\(S∪W1..u)) is true. In the parallel inner loop, for each split index i∈D, AEi is computed as FindAdvEx(ϵ, F\\(S∪W1..i)), so AEi is monotone non-decreasing in i (more free features makes existence of an adversarial example easier). To find the first index t with AEt=true, the correct update is ℓ ← max({i∈D | AEi=false} ∪ {ℓ}) and u ← min({i∈D | AEi=true} ∪ {u}). Instead, lines 14–15 set u ← min({i∈D | AEi=false} ∪ {u}) and ℓ ← max({i∈D | i<u} ∪ {ℓ}), which moves u to a false oracle result and breaks the invariant. Concretely, for a predicate with AE1=false, AE2=true, AE3=true, D={1,2,3}, the first iteration sets u=1, and after the inner loop line 18 adds W1 to S, returning S={1} although dWCXp({1}) is false. Thus the published Algorithm 2 does not in general compute a dCXp even with a perfect oracle; the experimental claim therefore rests on an unstated corrected update rule. This is a direct correctness gap in the central algorithm, independent of verifier timeouts.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":15062,"tokens_out":16042,"duration_ms":140830,"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":[{"comment":"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.","section":"Section 3.2, Algorithm 2"},{"comment":"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.","section":"Section 4.2, Claim 1"},{"comment":"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.","section":"Section 3.1 and Section 5.1"},{"comment":"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.","section":"Section 5.1 and Table 1"},{"comment":"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.","section":"Section 4.2, Algorithm 5"}],"minor_comments":[{"comment":"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.","section":"Section 3.2, Algorithm 2"},{"comment":"The notation F \\ S ∪ W_{1..i} is ambiguous; use F \\ (S ∪ W_{1..i}) consistently for the set of fixed features.","section":"Algorithms 1 and 2"},{"comment":"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.","section":"Section 3.2, Algorithm 2"},{"comment":"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.","section":"Table 1"},{"comment":"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.","section":"Section 2, Proposition 1"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is explicitly marked as a CoRR timestamp, and several of the issues look like fixable pseudocode errors rather than conceptual impossibilities. I would encourage a quick re-review after the authors supply corrected algorithms and proofs, and after they clarify how oracle timeouts are handled. The resource mismatch in the experiments should also be treated seriously in revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short take: This is a genuine algorithmic-engineering contribution to formal XAI. The SwiftCXp algorithm—parallelized dichotomic search over a monotone predicate with a feature-disjunction optimization—is sound as far as the oracle is complete, and the experimental speedups over the baseline are large even after discounting the unequal core counts. The stress-test note about Algorithm 2 inverts the monotonicity: AEi is non-increasing in i (more fixed features makes adversarial existence harder), so the updates u←min(false) and ℓ←max(i<u) are exactly right. The toy example in that note (true after false) cannot occur under the monotone predicate. So that concern does not hold up.\n\nWhat is genuinely new: the parallel chunked dichotomic search and the CLD-inspired FD heuristic. The paper adapts known techniques (Hemery, CLD, MARCO) to the distance-restricted setting defined in the authors' earlier work, and the engineering is careful enough that the empirical gains are plausible. The enumeration and smallest-CXp sections are less fleshed out, but they're secondary.\n\nWhere it's soft: (1) Claim 1 in section 4.2 is false as written—the hard constraint uses κ(x)=c, but a contrastive explanation needs κ(x)≠c. That is likely a typo, but it is load-bearing for the MaxSAT formulation. (2) The experimental section treats MN-BaB calls as exact, but there is a 4-hour time limit per call and no discussion of how timeouts or unknown answers are processed. If a timed-out call is counted as a definitive answer, the minimality guarantee of the returned set is void. (3) The baseline comparison uses 1 core vs 30, and there are no error bars or repeated trials. (4) No code released yet, despite the paper saying it will be. (5) Table 1 says 'dAXp' in the caption where it should say 'dCXp'.\n\nBottom line: For a researcher working on distance-restricted explanations, this is worth reading and citing. It needs revisions—fix the MaxSAT constraint, add a timeout-handling paragraph, run a fair baseline, and release the code—but the core algorithm is defensible. Send it to review.","headline":"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.","tokens_in":15658,"tokens_out":6764,"would_cite":true,"duration_ms":57979,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Parallelized adversarial-example queries make contrastive explanations practical for large neural networks.","keywords":["contrastive explanations","distance-restricted explanations","adversarial robustness","neural network verification","dichotomic search","parallel algorithms","feature importance","explainable AI"],"falsifier":"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.","tokens_in":14527,"feed_emoji":"🧠","tokens_out":6877,"duration_ms":55706,"temperature":0.7,"pith_summary":"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.","feed_headline":"Parallel search finds contrastive explanations for big neural nets","feed_subtitle":"Where the baseline binary search times out, the new method finishes in about 16 minutes on the largest test network.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Introduces the distance-restricted AXp/CXp definitions and the connection to robustness oracles that the new algorithms build on.","marker":"Izza et al., 2024a"},{"why":"Provides the pixel-sensitivity feature ordering heuristic and the VeriX-style dAXp computation that serves as the performance baseline context.","marker":"Wu et al., 2023"},{"why":"Establishes the minimal-hitting-set duality between AXp and CXp that underlies the enumeration algorithm.","marker":"Ignatiev et al., 2020"},{"why":"The clause-D (CLD) algorithm for minimal correction sets that the feature-disjunction heuristic adapts.","marker":"Marques-Silva et al., 2013a"},{"why":"The complete neural-network verifier used as the adversarial-example oracle; its completeness is the load-bearing assumption.","marker":"Ferrari et al., 2022"},{"why":"The MARCO-style enumeration procedure adapted for listing dCXps and dAXps.","marker":"Liffiton et al., 2016"}],"fun_headline_variants":["Parallel adversarial queries speed up contrastive explanations","SwiftCXp: parallel oracle calls for contrastive explanations","Parallel search solves contrastive explanations for big nets","SwiftCXp makes contrastive explanations practical","Fast contrastive explanations via parallel oracle search"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Parallel adversarial queries speed up contrastive explanations","SwiftCXp: parallel oracle calls for contrastive explanations","Parallel search solves contrastive explanations for big nets","SwiftCXp makes contrastive explanations practical","Fast contrastive explanations via parallel oracle search"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000834,"raw_usage":{"total_tokens":3590,"prompt_tokens":849,"completion_tokens":2741,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":465,"completion_tokens_details":{"reasoning_tokens":2671}},"tokens_in":465,"tokens_out":2741,"duration_ms":20360,"temperature":1.0,"reasoning_tokens":2671,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T04:52:58.820467+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"From contrastive to abductive explanations and back again","cited_arxiv_id":null,"evidence_quote":"Establishes the minimal-hitting-set duality between AXp and CXp that underlies the enumeration algorithm."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The complete neural-network verifier used as the adversarial-example oracle; its completeness is the load-bearing assumption."}],"review_version":1}