{"id":"c3466082-e93d-4c4b-a4d1-9e6e5b5ddb61","arxiv_id":"2508.15220","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"A hybrid MO-MCTS plus SAT-verification algorithm synthesizes decision-tree interpretations of black-box models with verified local Pareto-optimality guarantees, scaling to benchmarks where the global Pareto-optimal solver times out.","lead":"This paper builds simple decision-tree explanations of black-box AI systems that balance accuracy against understandability, and certifies each explanation with a formal guarantee that no better one exists within a small neighborhood. The authors combine a fast Monte Carlo tree search with a SAT-solver check, and show the approach still finds certified explanations where the previous globally optimal method times out.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Claimed LPO certificates are not backed by the printed proof: Appendix A's F6 = AND_i (¬u_i ↔ u_i) is unsatisfiable, making every SAT check trivially UNSAT and Lemma 2 false as written.","rationale":"The reader's weakest_assumption was the PAC tolerance, a genuine sample-to-population concern. The more immediately load-bearing issue, however, is internal soundness: the appendix's F6 is unsatisfiable, so Lemma 2 cannot be true as printed and Theorem 1 is not established. If the code has corrected the typo, the central approach may survive, but the manuscript must be revised; if the code matches the appendix, all UNSAT markers in the experiments are vacuous. The PAC issue remains secondary but important: even a corrected encoding certifies only sample-level LPO, while ε=0.25 and δc≈0.02 make the true-distribution statement uninformative. Because the flaw is fixable and the reader already required conditional changes, I keep the verdict conditional; no shift from the reader's CONDITIONAL is needed. Agreement is partial: the reader listed the F6 issue in the rationale but their stated weakest assumption was the PAC precision, not this proof hole.","tokens_in":23873,"tokens_out":10075,"duration_ms":114724,"concrete_test":"Clone https://github.com/anirjoshi/ALPO, locate the encoding of Phi_exp/F6, and run Check_SAT on the AutoTaxi candidate P=(0.916,14) from Fig. 6a with δc=0.023, δe=5. If the encoded formula is contradictory, the solver returns UNSAT for P and the certificate is vacuous. If the source differs from the appendix, replace F6 with a corrected unused-node variable v_i ↔ ¬u_i (using v_i in E), rerun on P, and confirm the formula becomes SAT with witness Q=(0.918,14); this distinguishes a typographical slip from a structural unsoundness.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Appendix A defines Phi_exp to include F6 := AND_{1<=i<=B} (¬u_i ↔ u_i). Each conjunct is logically equivalent to false, so Phi(c,e,c+δc,e+δe) is unsatisfiable for every candidate tree. If Check_SAT uses this encoding, the verification phase always reports UNSAT, every MO-MCTS output is moved to S′, and Theorem 1's conclusion is vacuous: it holds because no satisfying assignment can exist, not because no dominating tree lies in the window. Lemma 2, the load-bearing lemma for the certificate, is therefore false as printed. This is independent of the PAC/precision issue: even with exact measures, the printed formula cannot certify anything. If the released implementation contains a corrected variable (e.g., v_i ↔ ¬u_i used in E), the manuscript still does not establish the central guarantee as written.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces a notion of locally Pareto-optimal (LPO) interpretations for black-box ML models: an interpretation D is LPO w.r.t. slacks (δc, δe) if no other decision tree in the class GB has correctness and explainability measures that dominate D while staying within the slacks. The authors propose a two-phase algorithm (ALPO): first, MO-MCTS generates a best-effort Pareto front; second, each candidate is checked by a SAT solver against the LPO condition, replacing the candidate whenever a dominating tree is found and moving verified candidates to the output set S'. Theorem 1 states that every tree in S' is LPO. The experiments compare ALPO with the global-synthesis tool Synplicate on four main benchmarks; on AutoTaxi and Balance Scale the ALPO front closely matches the global front, and on Car Evaluation and Yeast ALPO still produces certified trees where Synplicate times out. The appendix gives a SAT encoding for the verification step.","tokens_in":23990,"tokens_out":7656,"duration_ms":93832,"significance":"If the technical issues are resolved, the LPO approach is a useful middle ground between heuristic multi-objective search and expensive global MaxSAT-based synthesis: it permits anytime guarantees and scales to instances where global certification fails. The paper's separation of search and verification is clean, the problem definition is precise, and the authors provide an open-source implementation (ALPO) and experiments on multiple benchmarks. The empirical comparison is directly relevant, though it is limited to two benchmarks where the global tool terminates. The central proof, however, is undermined by a likely typographical error in the published SAT encoding, and the statistical setting makes the distribution-level interpretation of the certificates questionable. These issues are fixable in revision.","major_comments":[{"comment":"Appendix A defines F6 := ∧_{1≤i≤B}(¬u_i ↔ u_i). Each conjunct is equivalent to false, so F6 — and hence the full formula Φ(c,e,c+δc,e+δe) — is unsatisfiable for every candidate tree. Consequently Check_SAT in Algorithm 1 always returns UNSAT, every MO-MCTS output is moved to S′, and Lemma 2 as stated is false: the formula does not encode existence of a dominating tree. Theorem 1 then holds vacuously. If the intended variable is a different one (e.g., an overline{u}_i encoding 'not used'), the text and the proof of Lemma 2 must be corrected; as printed, the LPO certificate is not established.","section":"Appendix A, F6"},{"comment":"The paper sets ε=0.25 and δ=0.1 for the PAC correctness estimates, while choosing δc≈0.02 (10/K) and reporting differences such as correctness 0.916 vs 0.918 (Figure 6a) as meaningful improvements. The SAT check is exact only with respect to the empirical correctness values; with a PAC tolerance of ±0.25, the certificate 'D is LPO' does not transfer to the true distribution ∆(I×O). To support the claim that ALPO's results 'closely match' global guarantees, either set ε comparable to δc, provide a confidence-interval-aware certificate, or explicitly state that all LPO guarantees are sample-relative and adjust the distribution-level phrasing.","section":"Section 5 (PAC settings, Figure 6a)"},{"comment":"The paper claims 'our approach converges monotonically to the global optimal' (contribution 3). Lemma 1 only shows that the MO-MCTS internal best-effort set is pointwise monotone under ⪯; Corollary 1 shows only that with sufficiently large slacks and timeouts at least one PO interpretation is eventually found. Neither statement establishes convergence of the output front to the global Pareto front as the number of iterations grows. Please add a formal statement and proof of such convergence, or weaken the contribution to 'monotone improvement of the best-effort front with local guarantees at every stop.'","section":"Section 1 (contribution 3), Lemma 1, Corollary 1"}],"minor_comments":[{"comment":"In the definition of S, '(D, C(D), E(E))' should read '(D, C(D), E(D))'. In Algorithm 1, the tuple type '(c,e)' should be declared before being used.","section":"Section 4.2 / Algorithm 1"},{"comment":"The variable u_i is used in F5 for 'reachable from the root' and reused in F6/F7 for 'node not used'. This notational clash likely caused the F6 error and should be resolved with distinct variable names.","section":"Appendix A"},{"comment":"The red crosses ('absence of interpretations') are unclear: a cross at a coordinate presumably means that no tree with that exact explainability/accuracy pair was found. Please define precisely how 'absence' is computed in the discrete measure space.","section":"Figure 6 legend"},{"comment":"Since Synplicate is the authors' own prior tool and was modified in-house ('we modified it slightly to restrict the interpretations to decision trees'), the exact modifications, parameter settings (PAC sample, timeout allocation, slack choices) should be reported for reproducibility, ideally by releasing the modified baseline.","section":"Section 5, Synplicate baseline"},{"comment":"The reference list contains duplicates ([25,26] and [31,32] both refer to the same Yeast and Balance Scale datasets). Please merge them.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The F6 error in Appendix A is the most serious issue: if the released implementation actually contains a corrected variable, the manuscript can be repaired, but as printed Lemma 2 and Theorem 1 are not established. The PAC/slack mismatch is a more subtle but important limitation that the authors should address head-on rather than in passing. I also recommend the editor pay attention to the comparison with Synplicate, since it is the authors' own tool modified in-house; the modification should be described in enough detail for an independent check."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this paper has a genuinely useful idea—replace global Pareto-optimality with a local, user-slacked version so that SAT-based certificates scale—and the two-phase MO-MCTS + SAT architecture is reasonable. But the appendix as printed contains a formula that is unsatisfiable by construction, so the proof of Lemma 2 is false and Theorem 1 is vacuous as written. That is a load-bearing issue, not a cosmetic one.\n\nThe new bits are Definition 2, the anytime framing, and the demonstration that certified local optimality can be computed on benchmarks where Synplicate times out. The writing is honest that local guarantees are weaker than global ones. The algorithm is simple to state and the code is available. If the encoding is corrected, the conceptual contribution stands.\n\nThe problems: Appendix A defines F6 := ∧_i (¬u_i ↔ u_i). Each conjunct is equivalent to false, so Φexp is unsatisfiable, making Φ unsatisfiable for every candidate. Check_SAT would always return UNSAT; every candidate gets moved to S′; Theorem 1 holds vacuously. This is not a subtle issue. The intended constraint was probably something like (¬u_i ↔ unused_i), but as written the certificate proves nothing. The authors must fix the formula and re-run the verification; the empirical claims might survive, but they are not currently backed by the printed proof.\n\nSecond, the PAC accuracy estimate is the value used in the certificate. With ε=0.25 and slacks around 0.02, the certified local optimality is only about the empirical counts, not the true distribution. The paper should state this limitation clearly; as written, readers could infer a distributional guarantee that the numbers cannot support.\n\nThird, Lemma 1 (monotone improvement of MO-MCTS) is asserted without proof. That is a minor gap in the anytime story, but worth a proof sketch.\n\nFourth, the comparison baseline is the authors' own tool with an in-house modification. That's acceptable for a first report, but an independent baseline or a sensitivity analysis would strengthen the empirical claim.\n\nWho should read this: researchers in XAI and formal methods who want a practical relaxation of the global Pareto-synthesis problem. The paper deserves a serious referee, but only after the encoding bug is fixed. I would not cite the guarantee in its current form.","headline":"A useful local-Pareto relaxation with a clean two-phase design, but the printed SAT encoding is unsatisfiable by construction, so the certificate is vacuous as written.","tokens_in":24624,"tokens_out":2680,"would_cite":false,"duration_ms":30387,"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":"This paper shows that decision-tree interpretations of black-box models can be certified Pareto-optimal within a user-chosen neighborhood, and that this local certificate is attainable on benchmarks where computing the global Pareto-optimal","keywords":["interpretability","Pareto optimality","local optimality","decision trees","SAT solving","Monte Carlo tree search","black-box explanations","multi-objective optimization"],"falsifier":"On a small benchmark such as Balance Scale with the stated node budget, exhaustively enumerate all semantically distinct decision trees, compute their correctness exactly on the full dataset, and check whether any tree inside the claimed slack window Pareto-dominates one of ALPO's certified trees; finding one would refute the certificate's transfer from sample to data.","tokens_in":23658,"feed_emoji":"🌳","tokens_out":7081,"duration_ms":77075,"temperature":0.7,"pith_summary":"Explaining a black-box ML model usually means trading accuracy against explainability. The paper formalizes a weaker but more tractable notion of optimality for this trade-off: an interpretation is locally Pareto-optimal if, within user-chosen slack windows for correctness and explainability, no other interpretation dominates it on both measures at once. It then gives a two-phase algorithm — multi-objective Monte-Carlo tree search to propose candidate decision trees, SAT solving to verify or improve them — and proves that every tree it outputs carries this local certificate. On the AutoTaxi and Balance Scale benchmarks the certified trees closely match the global Pareto-optimal curve of the earlier Synplicate tool; on Car Evaluation and Yeast, where Synplicate times out, ALPO still returns certified trees. The upshot is that users who accept a local guarantee can get verifiable Pareto-optimal interpretations in settings where a global guarantee is computationally out of reach.","feed_headline":"SAT certifies no better tree hides in the local window","feed_subtitle":"ALPO verifies by SAT that a decision-tree interpretation is Pareto-optimal within user-set slack, scaling where global methods time out.","key_machinery":"The central mechanism is the local Pareto-optimality window: given an interpretation with goodness tuple (c,e), a tree is LPO if no other tree in the same grammar dominates (c,e) while keeping correctness within δc and explainability within δe. Verification is carried by a Boolean formula Φ = Φsyntax ∧ Φcorr ∧ Φexp ∧ Φdom: the first conjunct restricts the syntax to decision trees, the next two bound correctness and explainability within the slack window using cardinality constraints, and the last enforces strict Pareto dominance. A SAT solver evaluates this formula for each candidate; unsatisfiability certifies local optimality, while a satisfying assignment yields a dominating tree that rep","core_discovery":"The central claim is Theorem 1: whenever the two-phase procedure terminates, every decision tree in the confirmed output set is locally Pareto-optimal with respect to the user-provided correctness slack δc and explainability slack δe, and every best-effort tree is no worse, under the dominance order, than some tree produced by the search phase. The local check is exact relative to the empirical correctness and explainability measures: the Boolean formula Φ(c,e,c+δc,e+δe) is satisfiable iff a decision tree in the grammar dominates (c,e) and stays within the window. Empirically, the paper reports that the certified points found by ALPO coincide with or closely approximate the global Pareto fro","pith_inferences":["The certificate's force is limited by the correctness estimate: with PAC tolerance ε = 0.25 and slack windows δc around 0.02, the SAT check proves local optimality only with respect to the sampled counts, not the underlying distribution. A quick test would be to re-verify the same certified trees using exact counts on a fixed dataset and compare.","Any candidate generator — not just multi-objective Monte-Carlo tree search — could feed the SAT verification phase, so the local certificate could be combined with other search heuristics such as beam search or local search to scale even further.","Because the SAT encoding's correctness constraints grow with the number of samples, the practical bottleneck will shift to sample count; sample compression or incremental SAT solving could extend the method to larger datasets, an effect not evaluated in the paper.","The paper's own future-work suggestion — feeding SAT-discovered dominating trees back into the search as new seeds — would turn the verifier into a search-improvement operator, potentially accelerating convergence toward the global Pareto front."],"forward_implications":["Users can stop ALPO at any time and still receive a set of certified locally Pareto-optimal interpretations; with more time, the best-effort set monotonically improves under the Pareto order and approaches the global front.","Because every globally Pareto-optimal interpretation is also locally Pareto-optimal for any slack, the local certificates coincide with global ones whenever the full front is found; the experiments exhibit this coincidence on AutoTaxi and Balance Scale.","If the slack windows are set large enough, a local certificate becomes a global Pareto-optimality certificate, so the framework can recover global guarantees given sufficient slack and timeout.","The verification phase is compatible with any explainability measure that can be encoded symbolically, not just the size-and-feature-weight score used in the experiments.","On benchmarks with larger feature spaces (Car Evaluation, Yeast), ALPO outputs certified locally Pareto-optimal trees where the global synthesis method produces nothing at all.","The anytime property means the approach degrades gracefully under tighter time budgets, still yielding non-empty LPO sets at the 5-minute timeout.","The local Pareto-optimality notion captures interpretations that cannot be perturbed into a strictly better one within a small neighborhood, which is a useful robustness property for explanations."],"supporting_citations":[{"why":"Supplies the Pareto-optimal interpretation problem formalism, the correctness and explainability measures, the SAT encoding that ALPO adapts, and the Synplicate baseline.","marker":"[35]"},{"why":"Supplies the multi-objective Monte-Carlo Tree Search algorithm used to generate the candidate interpretations.","marker":"[36]"},{"why":"Supplies the Kissat SAT solver that answers the local-optimality verification queries.","marker":"[7]"},{"why":"Supplies the PAC framework and sample-complexity bounds used to estimate correctness measures.","marker":"[30]"},{"why":"Supplies the Balance Scale dataset, one of the two benchmarks where Synplicate terminates and enables global-vs-local comparison.","marker":"[31]"},{"why":"Supplies the Car Evaluation dataset, a benchmark where Synplicate times out but ALPO still produces certified trees.","marker":"[8]"},{"why":"Supplies the Yeast dataset, a benchmark where Synplicate times out but ALPO still produces certified trees.","marker":"[25]"},{"why":"Source of the AutoTaxi benchmark, used for the central global-vs-local Pareto-front comparison.","marker":"[34]"}],"fun_headline_variants":["SAT-verified local Pareto optimality for interpretable models","Local Pareto optimality, now certified by SAT","SAT verifies local Pareto-optimal interpretations","Local Pareto certificate: no better tree within slack","SAT check proves local Pareto optimality for trees"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"The guarantee's strength depends on treating the measured accuracy on a sample as the true accuracy; with a 25-percent tolerance and slack windows of about two percent, a tree can be certified as locally optimal on the sample while a genuinely better tree exists on the true distribution.","fun_headline_variants_meta":{"raw":{"variants":["SAT-verified local Pareto optimality for interpretable models","Local Pareto optimality, now certified by SAT","SAT verifies local Pareto-optimal interpretations","Local Pareto certificate: no better tree within slack","SAT check proves local Pareto optimality for trees"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000837,"raw_usage":{"total_tokens":3498,"prompt_tokens":765,"completion_tokens":2733,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":509,"completion_tokens_details":{"reasoning_tokens":2661}},"tokens_in":509,"tokens_out":2733,"duration_ms":23768,"temperature":1.0,"reasoning_tokens":2661,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T18:03:42.628027+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"On a small benchmark such as Balance Scale with the stated node budget, exhaustively enumerate all semantically distinct decision trees, compute their correctness exactly on the full dataset, and check whether any tree inside the claimed slack window Pareto-dominates one of ALPO's certified trees; finding one would refute the certificate's transfer from sample to data.","supporting_citations":[{"cited_title":"In: FMCAD","cited_arxiv_id":null,"evidence_quote":"Supplies the Pareto-optimal interpretation problem formalism, the correctness and explainability measures, the SAT encoding that ALPO adapts, and the Synplicate baseline."},{"cited_title":"In: ACML","cited_arxiv_id":null,"evidence_quote":"Supplies the multi-objective Monte-Carlo Tree Search algorithm used to generate the candidate interpretations."},{"cited_title":"In: Heule, M., Iser, M., Järvisalo, M., Suda, M","cited_arxiv_id":null,"evidence_quote":"Supplies the Kissat SAT solver that answers the local-optimality verification queries."},{"cited_title":"Cambridge University Press (2014) 22 A","cited_arxiv_id":null,"evidence_quote":"Supplies the PAC framework and sample-complexity bounds used to estimate correctness measures."},{"cited_title":"In: Feng, L., Fisman, D","cited_arxiv_id":null,"evidence_quote":"Source of the AutoTaxi benchmark, used for the central global-vs-local Pareto-front comparison."}],"review_version":1}