{"id":"75f192ff-e4f3-49c5-be56-c721df7f8744","arxiv_id":"2505.10991","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"A MaxSAT/MIP-based implicit hitting-set algorithm computes a maximum-size inflated abductive explanation (Max-iAXp) for random forests and boosted trees.","lead":"This paper defines the 'most general' formal explanation for a tree ensemble decision as the largest region of input space that provably keeps the same prediction, and gives SAT/MaxSAT and MIP-based algorithms to compute it. Experiments show these explanations cover up to 10 times more input space than previous inflated explanations.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The published candidate-encoding in §4 is self-defeating: with at-most-one interval variables and non-positive log-proportion weights, the MaxSAT/MIP optimum selects no interval, so Algorithm 1 returns an empty region rather than a Max-iAXp.","rationale":"The most load-bearing claim is that Algorithm 1 returns a maximum iAXp. That claim fails on the published encodings for a reason independent of the cell-completeness question: the hard clauses permit selecting no interval, and the non-positive objective makes 'no interval' the unique optimum. I verified this from the text alone: equation (8) is '≤ 1', weights are logarithms of proportions ≤ 1, so all soft weights are non-positive. Therefore the MaxSAT/MIP oracle returns the empty region at every iteration, and the algorithm cannot produce the intended explanation. This is an internal inconsistency, not a disagreement with consensus. The reader flagged the cell-alignment assumption as the weakest point; that is a legitimate gap (the 'key property' only gives one direction), but it is likely repairable and secondary. The encoding defect is the one that lands immediately. No ad hominem is intended: the authors provide reproducible code and the experiments are suggestive, but the formal correctness assertion as written is not valid. The conditional verdict remains appropriate: fix the encoding, add the exactly-one constraint, and optionally prove the cell-boundary lemma.","tokens_in":22031,"tokens_out":7667,"duration_ms":85962,"concrete_test":"Run RC2 (or Gurobi) on the Naive MaxSAT encoding for a single-feature, two-split toy model, using hard constraint (8) and the given log-proportion soft weights, with the explained instance in the middle interval. Inspect the optimal model: if all y^i_{l,u} are false (objective 0), the bug is confirmed. Then replace '≤ 1' with '= 1' in (8) and re-run; if the solver now returns the middle interval and Algorithm 1 produces a nonempty Max-iAXp on a small dataset like iris, the defect and its repair are both verified.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 4 (Naive MaxSAT encoding) defines hard clauses (8) as ∑ y^i_{l,u} ≤ 1 for each feature, and soft clauses (y^i_{l,u}, w^i_{l,u}) with w^i_{l,u} = log(∑_{l≤j≤u} s(I^i_j)). Since s is a proportion or data proportion, each weight is ≤ 0. The all-false assignment satisfies every hard clause and gives objective 0, which is maximal; any assignment selecting one or more intervals has objective ≤ 0 and is therefore never optimal. Thus the claimed statement 'A solution to the MaxSAT model assigns exactly one interval to each feature' is false. Algorithm 1 line 3 then sets E_i = ∅ for every feature, so the candidate does not contain the explained instance v and is not an iAXp in the intended sense. The same defect is inherited by the bounds-based encoding and the MIP encoding, since they use the same soft objective over interval variables. This is not a subtle completeness gap but an internal inconsistency: as published, the oracle cannot propose any nonempty candidate region, so the algorithm does not compute a Max-iAXp at all. The fix is straightforward—replace '≤ 1' by '= 1' in (8) and in the corresponding MIP constraints, or add hard clauses requiring at least one y per feature—but the paper's correctness claims (conditions (6)–(7), termination with a maximum explanation) are unsupported for the encodings as written.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":22295,"tokens_out":6237,"duration_ms":75401,"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":[{"comment":"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.","section":"Section 4, Eq. (8) and Algorithm 1, line 3"},{"comment":"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.","section":"Section 3, \"key property of a TE\", and Algorithm 1, candidate generation"},{"comment":"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.","section":"Algorithm 1, correctness and termination discussion"}],"minor_comments":[{"comment":"There are typos: \"fall withing\" in the abstract and \"mononotic\" in the definition of a size measure; both should be corrected.","section":"Abstract and Section 2.2"},{"comment":"The symbol F CSs(E) in Eq. (7) is a typo for FSC_s(E); the notation should be made consistent.","section":"Equation (7)"},{"comment":"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.","section":"Section 4, Example 6"},{"comment":"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.","section":"Algorithm 1, line 5"},{"comment":"The text and table headers contain typos \"RFww\" and \"RFwm\" where \"RFwv\" is meant.","section":"Section 5.3 and Table 4"},{"comment":"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.","section":"Section 4, bounds-based encoding"}],"recommendation":"major_revision","confidential_remarks":"The experiments in Tables 2–4 report substantial coverage gains and reasonable runtimes, which suggests that the implemented system uses a different candidate constraint than the one printed in Eq. (8). I would ask the authors to verify that the public code contains an exactly-one (or at-least-one) constraint and to align the paper's encodings with the code. I would also encourage the authors to add the missing cell-alignment completeness lemma and a formal correctness theorem for Algorithm 1; with those additions the paper would be much stronger, but as it stands the central claim is not supported by the published formulation."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"I checked the stress-test note against the paper. It's right. The MaxSAT/MIP encodings in Section 4, as written, cannot propose any nonempty candidate region. Hard constraint (8) is a per-feature at-most-one over interval variables; soft weights are logarithms of proportions or data proportions, so they are all ≤0. The all-false assignment satisfies every hard clause with objective 0, and any assignment selecting one or more intervals has objective ≤0. So the claimed 'exactly one interval per feature' solution is never optimal. Algorithm 1 then sets E_i = ∅ for every feature, the candidate doesn't contain the explained instance, and the output is not an iAXp. The bounds-based and MIP encodings use the same objective, so they inherit the defect. This is a genuine load-bearing bug, and the paper's correctness claims (conditions (6)–(7), termination with a maximum explanation) are unsupported for the encodings as printed.\n\nThat said, the underlying idea is worthwhile. The Max-iAXp problem—choose the region that is a correct inflated abductive explanation and has maximum feature-space coverage—is a sensible formalization of 'most general' for numeric features, and the implicit hitting-set loop is a reasonable way to attack it. The unified TE encoding for weighted-voting random forests is a real convenience. The experiments show large coverage gains over inflated explanations, and even if the baseline iAXp isn't described clearly, the direction is empirically interesting.\n\nThe rest of the soft spots are small. The cell-aligned completeness claim (that the largest region can be found among unions of elementary intervals) is asserted but not proved; it's true because prediction is constant on each cell, so a maximal correct region can always be expanded to a union of cells—worth stating in a revision. The baseline iAXp should be specified. The repeated 'safeguard against scooping' remarks are unnecessary but not a technical problem.\n\nI'd want the authors to fix the ≤1 to =1 (or add hard 'at least one' clauses), re-run, and then the paper would be solid. As it stands, the main algorithm is presented with an implementation that provably does not do what the text claims. This deserves peer review and heavy revision: the concept should be out there, but the current encodings are not trustworthy. For my own work I wouldn't cite this version.","headline":"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.","tokens_in":22874,"tokens_out":3407,"would_cite":false,"duration_ms":36223,"reading_group":"maybe","serious_thinker":"no","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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…","keywords":["explainable AI","abductive explanations","inflated explanations","tree ensembles","random forests","boosted trees","implicit hitting set","maximum satisfiability"],"falsifier":"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.","tokens_in":21802,"feed_emoji":"🌳","tokens_out":11807,"duration_ms":111524,"temperature":0.7,"pith_summary":"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.","feed_headline":"Compute the widest explanation that still forces a tree model's answer","feed_subtitle":"Formal duality lets a solver-checker loop return the largest possible region that still guarantees the decision.","key_machinery":"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