{"id":"5e8bcf60-4902-4853-9056-4d5b5aa403be","arxiv_id":"2501.06766","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper proves that deciding and finding minimal global necessary reasons is in L for perceptrons, NL-complete for BDDs, and co-NP-complete or DP-complete for multilayer perceptrons.","lead":"This paper studies the computational difficulty of finding and checking global necessary reasons, logical conditions that every instance of a given class must satisfy. It shows these problems are easy for perceptrons, moderately hard for binary decision diagrams, and hard for multilayer perceptrons.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 4.2's proof claims the constructed 2CNF implication graph is undirected, but unit clauses and omitted contrapositives make it directed, so the L-membership of literal entailment is not established and the logspace upper bounds for PRC/BDD rest on an invalid argument.","rationale":"The reader accepted the paper and identified the conjunctive language restriction as the weakest assumption, but the more load-bearing issue is internal: the proof of Theorem 4.2, which underpins every logspace and NL upper bound in the paper, contains a concrete error. The paper's central claim is a complexity classification, and classifications are only as solid as the upper-bound proofs. Theorem 4.2 is not a peripheral lemma; it is invoked in the PRC upper bounds, in the BDD algorithm, and in the generic minimality check, so a gap there affects three of the four main rows of Table 4.1. My objection is not to the theorem's truth: the entailment problem for conjunctions of equalities and inequalities over Booleans is equivalent to implication in a system of linear equations over GF(2), which should be decidable in L via undirected reachability with parity. Rather, the objection is that the proof as written does not establish this, because the implication graph of the constructed 2CNF is not undirected. The counterexample phi=(v_1=1)^(v_1=v_2), ell=(v_2=1) is minimal and directly exposes the flaw: the formula is unsat, but the graph built from the paper's listed implications has no contradictory cycle. I have not found similar problems in Lemma 4.1, the BDD lower bound, or the MLP reductions; those parts appear coherent and well argued. The DP-completeness proof for MLP minimality is also sound assuming the cited encoding lemma of Barceló et al., which is standard. Because the flaw is localized and a fix is likely available, a conditional acceptance is appropriate: the paper should be published once Theorem 4.2 is reproven (or the proof is corrected) and the dependent upper bounds are rechecked. Until then, the advertised L and NL results are not fully justified by the text.","tokens_in":31299,"tokens_out":27730,"duration_ms":285957,"concrete_test":"Re-run the proof of Theorem 4.2 on phi=(v_1=1) ^ (v_1=v_2), ell=(v_2=1). Build psi exactly as the theorem prescribes, write out the implication graph edges for each conjunct (treating unit clauses as x_1 and not-x_2), and check whether the graph is undirected and whether the paper's reachability criterion certifies unsatisfiability. If it fails, Theorem 4.2's proof is invalid. As a second check, implement the alternative XOR-constraint reduction: encode each literal as a parity equation over GF(2), add a dummy zero variable, and test entailment by undirected reachability in the resulting parity-labeled graph; if this succeeds on the same instance, the theorem is true but needs a corrected proof.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The logspace/ NL results all depend on Theorem 4.2, which states that deciding phi|=ell (equiv. phi|/=ell) is in L. It is used directly for the PRC upper bound (Thms 4.3-4.4), in Algorithm 2 for BDDs (Thm 4.6), and in the generic minimality procedure (Thm 4.7). The proof builds a 2CNF psi and claims its implication graph is undirected because every implication has a symmetric counterpart. That claim is false. Unit clauses appear whenever a literal fixes a feature (v_i=1, v_i=0, v_i≠1, v_i≠0) or when the negated conclusion is a unit; such a clause l adds only the directed edge not-l -> l. For v_i=v_j the proof lists x_i->x_j and x_j->x_i but omits the contrapositive implications not-x_j->not-x_i and not-x_i->not-x_j, which are needed in the standard implication graph. Concretely, take phi=(v_1=1) and (v_1=v_2), ell=(v_2=1). Then phi|=ell and the constructed psi=x_1 ^ (x_1->x_2) ^ (x_2->x_1) ^ not-x_2 is unsatisfiable. The graph generated from the listed implications contains edges not-x_1->x_1, x_2->not-x_2, x_1->x_2, x_2->x_1; there is no path from not-x_2 to x_2, so the claimed undirected reachability test does not detect the contradiction. The theorem may be repairable by viewing phi as a system of XOR constraints and using undirected parity reachability, but as written the proof does not establish the lemma, and the central upper bounds are not fully supported.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper studies global necessary reasons for binary classifiers, expressed as conjunctions of equalities and inequalities over feature variables. It introduces two decision problems, Necessity[C] and MinNecessity[C,≤/⊆], for C ∈ {PRC, BDD, MLP}, and claims a complete complexity classification: the problems are in L for perceptrons, NL-complete for BDDs, and co-NP-complete / DP-complete for MLPs. The technical core is a characterization (Lemma 4.1) that reduces minimality to checking whether any single literal is a global necessary reason, a claimed logspace entailment test for the condition language (Theorem 4.2), and reductions for each classifier family. The paper also draws conclusions about computing minimal global necessary reasons with oracles.","tokens_in":31702,"tokens_out":18177,"duration_ms":179862,"significance":"If the classification were fully established, this would be a valuable systematic contribution: it gives a complete complexity picture for a global explainability notion, shows that the two minimality criteria collapse, and yields efficient parallel/SAT-based algorithmic insights for perceptrons, BDDs, and MLPs. The Lemma 4.1 literal-characterization is an elegant and reusable tool, and the high-level framing is clear. However, the specific proof gaps identified below mean that several central claims are not yet supported by the manuscript; the results are plausible and likely repairable, but the paper as written overstates the rigor of its upper and lower bounds.","major_comments":[{"comment":"The proof asserts that the implication graph of the constructed 2CNF formula ψ is undirected, because every implication has a symmetric counterpart. This is not the case. Unit clauses occur whenever a literal fixes a feature (e.g., φ contains v1=1) or when the negated conclusion is a unit, and a unit clause x adds only the directed edge ¬x→x. Moreover, the encoding of vi=vj lists xi→xj and xj→xi but omits the contrapositive edges ¬xj→¬xi and ¬xi→¬xj that belong to the standard implication graph. Concretely, take φ=(v1=1)∧(v1=v2) and ℓ=(v2=1); then φ|=ℓ, but the graph containing x1→x2, x2→x1, ¬x1→x1, and x2→¬x2 has no path from ¬x2 to x2, so the claimed undirected reachability test does not detect the unsatisfiability of ψ. Since Theorem 4.2 is used in Theorems 4.3, 4.4, Algorithm 2, Theorem 4.7, and Theorem 4.9, the L and NL upper bounds are not established by the given argument. The conclusion may be repairable by viewing the constraints as parity (XOR) constraints and using logspace solvability of undirected parity reachability, but the current proof is invalid as written.","section":"Appendix A, proof of Theorem 4.2"},{"comment":"The reduction from UniformRootedAcyclicReach to NotNecessity[BDD] connects every sink of the uniform RDAG to uyes, not only the designated sink t. Therefore a path from the root s through the distinguished edge e to any other sink u (followed by the edge to uyes) witnesses that φ=(s=0) is not a global necessary reason, even if no path from s to t traverses e. In the “only if” direction, after removing uyes the path may end at u rather than at t, and the proof incorrectly identifies an arbitrary sink with the given sink t. This breaks the claimed NL-hardness. The construction can likely be repaired by connecting only the designated sink t to uyes and all other sinks to uno, or by proving that a unique-sink version of UniformRootedAcyclicReach is NL-hard, but as written the lower bound of Theorem 4.6 is unsupported. The adaptation used in the hardness proof of Theorem 4.7 should be re-examined in light of the same issue.","section":"Appendix A, proof of Theorem 4.6 (hardness)"}],"minor_comments":[{"comment":"Several cross-references call Lemma 4.1 and Lemma 4.5 “Theorem 4.1” and “Theorem 4.5”; please make the numbering consistent throughout the text.","section":"Section 4 and Theorem 4.9 proof"},{"comment":"Line 2 says “foreach literal ℓ∈L[n]”, but L[n] is the set of conditions (conjunctions), not the set of literals; the quantification should be over the O(n²) literals of the language.","section":"Algorithm 1"},{"comment":"The claim that one can iterate over all leaves of a decision tree in logarithmic space deserves a short justification, since the naive traversal of a tree with exponentially many leaves is not obviously logspace.","section":"Section 4.2, A Note on Decision Trees"},{"comment":"The notation used for replacing high-outdegree nodes, with u∗₀=u and u∗ₙ₋₁=vₙ, is terse; a small example or a restated indexing scheme would greatly improve readability.","section":"Lemma A.3"}],"recommendation":"major_revision","confidential_remarks":"The main complexity claims may well be true, and the reader's report is right to credit the clear framework and the elegant minimality criterion. However, the paper currently contains two load-bearing proof gaps: the logspace entailment lemma relies on a false symmetry claim, and the BDD hardness reduction conflates an arbitrary sink with the designated sink. Both are fixable in principle, but they require nontrivial rewriting of the appendix, so I cannot recommend acceptance at this stage."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know. First, the paper delivers the first full complexity map for global necessary reasons: L for perceptrons, NL-complete for BDDs, co-NP-complete and DP-complete for MLPs. The minimality characterization (Lemma 4.1) is genuinely useful — it reduces minimality to checking whether any non-entailed literal is itself a necessary reason, and it correctly shows cardinality and subset minimality coincide for this language. Second, the proof of Theorem 4.2, the logspace entailment lemma that carries every upper bound, has a real gap. The stress-test example lands. For φ=(v1=1)∧(v1=v2), ℓ=(v2=1), the constructed ψ is x1∧(x1→x2)∧(x2→x1)∧¬x2, which is unsatisfiable. But the claimed undirected implication graph has directed edges ¬x1→x1 and x2→¬x2 from the unit clauses, plus the symmetric pair x1↔x2. There is no path from ¬x2 to x2, so the undirected reachability test misses the contradiction. The paper's claim that every implication has a symmetric counterpart is simply false once unit clauses appear. This is not cosmetic: Theorem 4.2 feeds the perceptron upper bound, Algorithm 2 for BDDs, and the generic minimality procedure. Without a valid L-membership proof, the PRC results and the BDD upper bounds lack support. The lower-bound reductions look careful, and the theorem is likely repairable — the condition language is a system of equalities/inequalities over Boolean variables, i.e. parity constraints, and undirected parity reachability is plausibly in L. But as written the proof fails.\n\nWhat the paper does well: the related-work separation from INM19 and BAK24 is clear and honest; the BDD characterization (Lemma 4.5) is elegant; the hardness reductions are standard and give genuine completeness; the reliance on free BDDs and the external MLP encoding lemma are explicit and defensible. The appendix is detailed and readable.\n\nWho is this for: people in formal explainability who need to know when global necessary reasons are tractable. For them the complexity map matters, and most of it will survive a proof repair. The paper deserves a serious referee, but only with the explicit instruction that Theorem 4.2 be rewritten and checked. I would not cite it until that fix lands.","headline":"Nice complexity map for global necessary reasons, but Theorem 4.2's proof as written is wrong — the implication graph is directed, not undirected, so the logspace upper bounds are currently unsupported.","tokens_in":32236,"tokens_out":3893,"would_cite":false,"duration_ms":36281,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68Q25","68T05"],"pacs":[],"model":"deepseek-v4-flash","headline":"Checking and minimizing global necessary reasons ranges from logarithmic space for perceptrons to co-NP- and DP-completeness for multilayer perceptrons.","keywords":["global necessary reasons","explainable AI","computational complexity","binary decision diagrams","perceptron","multilayer perceptron","logspace","minimal explanations"],"falsifier":"An exact check would enumerate all small perceptrons, BDDs, and MLPs together with all conditions in $\\mathcal{L}[n]$, compute global necessity and both kinds of minimality by brute force, and compare against the paper's algorithms. One mismatch—for instance a condition that is minimal despite some non-entailed literal being necessary, or a BDD whose path characterization fails—would refute the key lemma and the complexity classification built on it.","tokens_in":31105,"feed_emoji":"🧠","tokens_out":14006,"duration_ms":117020,"temperature":0.7,"pith_summary":"The paper asks how hard it is to decide that a logical condition is a global necessary reason for a classifier to output a class—meaning every instance given that class must satisfy the condition—and how hard it is to find the most informative such reason. It establishes a complete complexity map: the decision problems are in logarithmic space for perceptrons, NL-complete for binary decision diagrams, and co-NP-complete for multilayer perceptrons, with minimality pushing only the MLP case up to DP-complete. The two natural minimality criteria, fewer satisfying instances and a subset of satisfying instances, turn out to select exactly the same reasons and to have the same complexity. This matters because global necessary reasons can expose biases in a classifier, and the map says when such reasons can be computed quickly, in parallel, or only by SAT-style search.","feed_headline":"Global explanation for MLPs is co-NP-complete; perceptrons need logspace","feed_subtitle":"Minimal global necessary reasons are easy for perceptrons and BDDs, but MLPs require SAT-style search.","key_machinery":"The central object is the condition language $\\mathcal{L}[n]$: conjunctions of literals of the form $t \\Diamond t'$ with $\\Diamond \\in \\{=,\\ne\\}$ and terms drawn from feature variables and constants $0,1$. The paper's pivotal lemma says that a global necessary reason $\\varphi$ is minimal under either preorder exactly when no single literal $\\ell$ that $\\varphi$ does not entail is itself a global necessary reason; this turns every minimality question into $O(n^2)$ checks of single literals. The entailment check $\\varphi \\models \\ell$ is shown to be in L by translating it into a two-literal conjunctive normal form whose implication graph has symmetric edges, making it an undirected graph whose reachability is decided in logarithmic space. For BDDs, the non-necessity of $\\varphi$ is characterized by an accepting path whose conjunction of feature assignments fails to entail some literal entailed by $\\varphi$, and an NL algorithm guesses that path. For MLPs, the hardness proofs run through the polynomial-time encoding of arbitrary Boolean formulas as ReLU/Heaviside networks, transferring satisfiability hardness to the explanation problem.","core_discovery":"The central claim is a complete complexity classification for global necessary reasons expressed as conjunctions of equalities and inequalities over feature variables and constants (the condition language $\\mathcal{L}[n]$). For perceptrons, deciding whether a given condition is a global necessary reason is in L (deterministic logarithmic space), and deciding minimality stays in L. For free binary decision diagrams both problems are NL-complete. For multilayer perceptrons with rectified-linear hidden activations and a step output, necessity is co-NP-complete and minimality is DP-complete, where DP is the class of problems formed by combining one NP and one co-NP problem. The paper also proves that the two minimality preorders—comparing numbers of models and comparing model sets—are equivalent for this language, and that computing a minimal reason is polynomial-time with an oracle for the arbitrary-necessity problem, hence polynomial for perceptrons and BDDs and SAT-solver-accessible for MLPs.","pith_inferences":["Editorial inference: the restriction to conjunctions is what keeps the picture tractable; allowing disjunctions would let conditions encode arbitrary classifier behavior, and the logspace/undirected-graph argument would not survive.","Editorial inference: because the two preorders coincide, a greedy extraction loop that repeatedly conjoins any literal that keeps the condition necessary should find a minimal reason; this is a direct implementation recipe the paper does not benchmark.","Editorial inference: for MLPs, the DP-complete characterization suggests encoding non-minimality as a SAT instance and using an off-the-shelf solver, which would be a natural experimental follow-up.","Editorial inference: the results give a formal way to audit bias—finding minimal necessary reasons for a sensitive class on linear classifiers and BDDs is cheap, so fairness checks could run at scale; the paper does not discuss this application."],"forward_implications":["Minimal global necessary reasons for perceptrons and BDDs are computable in polynomial time, so auditing these classifiers for necessary conditions is practical.","For MLPs, minimal global necessary reasons are computable in polynomial time with a co-NP oracle; in practice this means SAT solvers, since the decision problem for arbitrary reasons is co-NP-complete.","The two minimality criteria—fewest satisfying instances and subset of satisfying instances—lead to identical minimal explanations, so model counting is not needed to pick the most informative condition.","Minimality adds no complexity for perceptrons or BDDs, but it moves MLPs from co-NP-complete to DP-complete, so the extra demand is real only for the expressive family.","Computing a minimal reason is at least as hard as deciding whether a given reason is minimal, and is no harder than a polynomial number of calls to the arbitrary-necessity oracle; the decision and search problems therefore have matching practical strategies."],"supporting_citations":[{"why":"Defines the global necessary reason notion and its relation to adversarial examples that the paper extends.","marker":"[INM19]"},{"why":"Supplies the lemma that any Boolean formula can be encoded as a polynomial-size ReLU/Heaviside MLP, supporting the co-NP and DP hardness proofs.","marker":"[Bar+20b]"},{"why":"Shows undirected reachability is decidable in logarithmic space, which the logspace entailment check relies on.","marker":"[Rei08]"},{"why":"Provides the implication-graph reachability method for 2CNF formulas that the logspace entailment reduction adapts.","marker":"[APT79]"},{"why":"Gives logspace arithmetic for the addition and multiplication steps used in perceptron halfspace tests.","marker":"[HAB02]"},{"why":"Supplies the standard complexity class definitions and closure properties used throughout the classification.","marker":"[AB09]"}],"fun_headline_variants":["MLP explanations co-NP-complete; perceptrons in logspace","Perceptrons: logspace; MLPs: co-NP-complete for global reasons","Global necessary reasons: easy for perceptrons, hard for MLPs","From logspace to co-NP: complexity of global explanations"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that an explanation is a conjunction of equalities and inequalities; every equivalence, logspace algorithm, and completeness proof in the paper depends on that restriction, and the MLP hardness also assumes that arbitrary Boolean formulas can be encoded as polynomial-size ReLU/Heaviside networks.","fun_headline_variants_meta":{"raw":{"variants":["MLP explanations co-NP-complete; perceptrons in logspace","Perceptrons: logspace; MLPs: co-NP-complete for global reasons","Global necessary reasons: easy for perceptrons, hard for MLPs","From logspace to co-NP: complexity of global explanations"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000683,"raw_usage":{"total_tokens":3058,"prompt_tokens":860,"completion_tokens":2198,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":476,"completion_tokens_details":{"reasoning_tokens":2118}},"tokens_in":476,"tokens_out":2198,"duration_ms":51370,"temperature":1.0,"reasoning_tokens":2118,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T20:50:35.952640+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"An exact check would enumerate all small perceptrons, BDDs, and MLPs together with all conditions in $\\mathcal{L}[n]$, compute global necessity and both kinds of minimality by brute force, and compare against the paper's algorithms. One mismatch—for instance a condition that is minimal despite some non-entailed literal being necessary, or a BDD whose path characterization fails—would refute the key lemma and the complexity classification built on it.","supporting_citations":[],"review_version":1}