{"id":"0cb14ce2-1f98-4ee4-896e-a2db74688c7e","arxiv_id":"2501.10126","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"dtPaynt uses SMT-based deductive synthesis with abstraction refinement to find small decision-tree policies for MDPs, outperforming the prior MILP tool OMDT on large models.","lead":"This paper introduces dtPaynt, an algorithm that synthesizes small decision trees representing near-optimal policies for large Markov decision processes. It combines SMT-based tree encoding with abstraction refinement, and reports trees up to 38 times smaller than existing tools while keeping high policy quality.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Random-action fallback changes the policy class: the headline size reductions versus dtControl compare different objects, so the empirical central claim needs a fallback-free rerun.","rationale":"I read the paper in good faith. The algorithmic core—Theorem 4, the SMT encoding, and the abstraction-refinement pruning argument—appears sound: the pruning steps on lines 6 and 7 of Algorithm 1 correctly discard only families that cannot improve on the current best, and termination by finite splitting is argued. The random-action fallback is explicitly defined and the synthesis problem is stated relative to it, so the formal result is internally consistent. However, the paper's most attention-grabbing empirical claims are the size reductions over dtControl and the 90% reduction for csma-Q4. Since dtControl solves a different problem (exact mapping of a fixed optimal policy) and is not allowed the fallback, the comparison mixes a randomized-fallback policy class with an exact policy class. This is the most load-bearing weakness in the central claim as presented. The proposed test—re-running the comparisons without the fallback—would show whether the size advantages are an artifact of the semantic extension or a genuine property of the synthesis loop. I also flag the NP-hardness proof in App. A.4 as apparently flawed: the constructed state variables allow a depth-q+2 tree to distinguish all states individually, so the claimed reduction from X3C does not go through as written. This is a correctness defect in a side theorem, not in the main algorithm, but it should be fixed. My verdict remains CONDITIONAL, matching the reader: the main algorithm and experiments are plausible, but the fallback comparison and the NP-hardness proof require author response.","tokens_in":22550,"tokens_out":18896,"duration_ms":192733,"concrete_test":"Re-run the Q2 and Q4 experiments with the fallback disabled: modify the SMT encoding of Section 3.1 so that act_{s,α,n} is satisfiable only if α ∈ Act(s) for every state reaching leaf n (with αrand allowed only as an explicit leaf action), and compare the resulting tree sizes and normalized values against dtControl on the same benchmarks. If the 20x/38x and 90% reductions persist without the fallback, the concern is resolved; if they collapse, the headline size claims depend on the random-action fallback and must be reframed as comparing different policy classes.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Definition 4 defines the induced policy of a DT as δ(leaf(s)) when that action is available, and as αrand otherwise. This is a coherent, explicitly stated semantics, and Theorem 4 is sound for it. The load-bearing issue is that the paper's central empirical claims—20x/38x smaller trees than dtControl, and the 90% size reduction in §5 Q4—compare these fallback-enabled, randomized-fallback policy trees against dtControl trees that exactly represent a fixed optimal policy σ* on the relevant states. dtControl is not given the same fallback freedom, so the comparison is not within a common policy class. The size advantage may come from the ability to write an unavailable leaf action that silently becomes αrand, rather than from the abstraction-refinement loop finding genuinely better small trees. This matters because the stated motivation is interpretable, human-readable policies: a tree whose leaves do not actually prescribe the action a reader sees is not the same artifact. The formal synthesis result is internally consistent; the concern is load-bearing for the empirical and interpretability parts of the central claim. A secondary issue is that the NP-hardness proof in App. A.4 appears incorrect as written: state-specific predicate variables allow a depth-q+2 DT to distinguish all n+3 states without using any set predicates, so the claimed X3C equivalence fails; this should be corrected but is not central to Theorem 4.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies the synthesis of small decision-tree (DT) policies for Markov decision processes. It introduces an SMT-based encoding of a fixed tree template (Section 3.1), including unsatisfiable-core-based diagnosis and a harmonization technique (Section 3.2), and combines these with an abstraction-refinement loop (Algorithm 1) to find a DT of bounded depth with maximum reachability/reward value. The central formal result is Theorem 4, which states that Algorithm 1 is sound and complete for this objective under the induced-policy semantics of Definition 4. The experimental section compares dtPaynt with OMDT and dtControl, reporting scalability to hundreds of thousands of states and size reductions up to 90% on a 1.5M-state model at 1% value loss.","tokens_in":22774,"tokens_out":11252,"duration_ms":107435,"significance":"If the results hold, the paper makes a useful contribution to the concise-policy-synthesis literature: it offers a deductive, SMT-driven alternative to monolithic MILP encodings, with public code and benchmarks. The abstraction-refinement loop with harmonizing parameterizations is a clever adaptation of prior Paynt ideas. The main caveats are that the random-action fallback in Definition 4 changes the policy class in some of the experiments, weakening the explanatory-power interpretation, and that the NP-hardness proof in Appendix A.4 is, as written, not a valid reduction. Neither issue invalidates the core synthesis algorithm, but both need to be addressed before the empirical and complexity-theoretic claims can be taken at face value.","major_comments":[{"comment":"The fallback semantics of Definition 4 — a leaf prescribing an unavailable action induces the random action αrand — is explicit and coherent, and Theorem 4 is sound for it. However, the paper's interpretability claims and some empirical comparisons are affected. In Q3 (Table 1), the 0-DT for ij-20 is optimal precisely because the fallback lets the single leaf action be replaced by αrand where the action is unavailable, and the Q4 reduction of the csma-Q4 DT (90% size reduction) can likewise rely on fallback leaves. dtControl, by contrast, is run on a fixed tabular policy and does not have this fallback freedom, so the reported size advantages in these experiments compare policies in different classes. Moreover, a tree whose displayed leaf action is not actually executed is a weaker fit for the stated motivation of human-readable policies. Please rerun the Q3/Q4 experiments with the fallback disabled (leaf actions restricted to Act(s)) or, if fallback is retained, report how often it is actually used, and provide a dtControl baseline that is given the same fallback capability.","section":"§4.2 / §5, Q3 and Q4; Definition 4; Remark 2"},{"comment":"The NP-hardness reduction from X3C is not correct as written. The state variables include a variable for every state s with s(v)=1 only in that state; since predicates are of the form v≤b, the predicate 'v≤0' uniquely identifies that state. With these predicates a tree of depth about log2(|S|) can distinguish all n+3 states without using any set predicates from T, and for n>7 this depth is strictly smaller than k=|U|/3+2. Hence the claimed equivalence with the existence of an exact cover fails even when no exact cover exists. The combinatorial step in the 'Correctness' paragraph is asserted without proof, and the citation to [28] is to the PRISM 4.0 paper, which does not support the claim. The theorem may be true, but the proof must be repaired or the claim removed.","section":"Appendix A.4, Theorem 3"}],"minor_comments":[{"comment":"The reference '[28]' in the correctness argument should be replaced by the intended source; as written it points to the PRISM 4.0 tool paper.","section":"Appendix A.4"},{"comment":"The modification that makes every action available in every state is disclosed, but the paper should state explicitly that the baseline tools and dtPaynt are all evaluated on this modified MDP, and should comment on how the fallback αrand interacts with this modification.","section":"Section 5, Setting"},{"comment":"The word 'impelementable' is misspelled; it should be 'implementable'.","section":"Theorem 2 statement"},{"comment":"The termination argument states that any nontrivial splitting makes Algorithm 1 terminate; since this rests on splitInformed and splitArbitrary always producing strictly smaller parameter families, it would be clearer to state and prove this property explicitly.","section":"Section 4.2, paragraph after Algorithm 1"}],"recommendation":"major_revision","confidential_remarks":"The manuscript's main synthesis algorithm is a solid contribution and the public artifact is valuable. The two concerns above — the fallback semantics in the empirical evaluation and the flawed NP-hardness proof — are substantial but repairable. I do not see grounds for rejection, but the present form overstates the comparisons with dtControl and the complexity result. The Q2 comparisons appear far less affected by the fallback issue because all actions are made available there; the authors should state that distinction clearly. No other concerns about novelty or scope."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know: this is a genuine systems paper, with code and data publicly available, and the core abstraction-refinement loop looks sound. The SMT encoding of k-implementability and the harmonization-based splitting are genuinely new relative to OMDT's monolithic MILP. The experiments are extensive (21 models, depths up to 8), and the comparison against OMDT is convincing: dtPaynt scales to models where the MILP solver stalls, and when both finish the values are close.\n\nThe main theorem (Theorem 4) is plausible, and the appendix proof reads correctly to me, modulo the issues below. The bounded-depth mode with tree hints is a sensible engineering contribution.\n\nTwo soft spots. First, the NP-hardness proof in App. A.4 is wrong as written. The MDP has state-specific predicates that are true for exactly one state. A binary tree of depth about log n can isolate every state, so a depth |U|/3+2 tree can pick the unique correct action in each state without any reference to the set-cover predicates. The claimed X3C reduction therefore does not force an exact cover. There is also a citation error in that section ([28] cannot be the PRISM paper). This does not touch Theorem 4, but the proof should be corrected or removed.\n\nSecond, the random-action fallback in Definition 4 is coherent and explicitly stated, but it changes what the tree actually represents: a leaf reading 'go up' in a state where 'up' is unavailable silently becomes the uniform random action. For the paper's interpretability motivation, that is a caveat readers should not have to dig for. Note, though, that in the Q1/Q2 benchmarks all actions were made available in every state, so the fallback does not explain the 20x/38x size reductions there; it matters for Q3/Q4. I would ask for a fallback-free run or at least a measure of how often leaves trigger alpha_rand.\n\nThe comparison with dtControl is also slightly apples-to-oranges: dtControl reproduces an optimal policy exactly, while dtPaynt is allowed to lose value. That is a legitimate trade-off, but the headline 'times smaller' numbers need the value difference stated alongside.\n\nBottom line: this deserves a serious referee. The main algorithm and the experimental story are worth publishing; the NP-hardness proof needs repair, and the fallback should be discussed more prominently. Send it to review with an expectation of major revision.","headline":"A real, reproducible systems contribution for synthesizing small decision-tree MDP policies; the main loop is sound, but the NP-hardness proof is faulty and the fallback semantics deserves more careful framing.","tokens_in":23362,"tokens_out":6592,"would_cite":true,"duration_ms":63690,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","90C40","68Q17"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper establishes that the bounded-depth decision-tree synthesis problem for MDPs can be solved by a sound and complete abstraction-refinement loop, and that an SMT-based implementation scales beyond the previous MILP-based tool…","keywords":["Markov decision processes","decision tree policies","bounded-depth synthesis","abstraction refinement","SMT solving","policy compression","unsatisfiable cores","model checking"],"falsifier":"Take a small benchmark such as lake-4, fix $k=2$, exhaustively enumerate every depth-2 decision tree over the allowed predicates, and compare the maximum value of that enumeration with dtPaynt's output; any gap would refute Theorem 4. A cheaper conceptual check is to modify the fallback rule so leaves may only name available actions; if the best value drops, the paper's optimality claim is tied to the randomized-fallback semantics rather than to fully realizable deterministic trees.","tokens_in":22314,"feed_emoji":"🌳","tokens_out":7971,"duration_ms":74572,"temperature":0.7,"pith_summary":"Optimal policies of Markov decision processes are usually lookup tables, too large for a human to inspect, so a natural goal is to compress them into small decision trees. This paper targets the harder variant: instead of compressing one fixed optimal policy, search directly over all policies induced by decision trees of depth at most $k$ and return the tree with the best reachability, reward, or discounted value. The proposed loop, dtPaynt, alternates model checking of an overapproximating family of MDPs with SMT queries that decide whether an abstract optimal policy can be realized by a tree; when it cannot, an unsatisfiable core and a harmonizing pair of parameterizations guide a split. The authors prove the loop sound and complete, and their experiments show it outperforms the prior MILP-based solver on larger models and, with a heuristic mapping tool, cuts tree sizes by up to 90% while sacrificing under 1% of value on a 1.5-million-state model.","feed_headline":"SMT loop finds provably optimal small policy trees","feed_subtitle":"dtPaynt beats the MILP baseline and shrinks a 1.5M-state policy tree by 90%.","key_machinery":"The load-bearing object is the tree template with parameterizations: a template is a binary tree whose nodes are not yet assigned predicates or actions, and a parameterization $f=(D,B,A)$ chooses a variable index, a bound, and an action for each node, thereby instantiating a concrete decision tree. The abstraction-refinement engine then uses the family-MDP $M(\\mathcal{F})$, defined so that an action is available in a state exactly when some parameterization in $F$ could produce it, giving a sound upper bound on the value of every tree in the family. When the optimal policy of $M(\\mathcal{F})$ is spurious, the SMT encoding of the mapping problem returns an unsatisfiable core together with harmonizing parameterizations $f_1,f_2$ that differ in exactly one variable; splitting the domain of that harmonizing variable bisects the family in a way informed by the conflict, and the loop repeats until every family is pruned or realized.","core_discovery":"The central discovery is that the bounded-depth synthesis problem — maximize the value over all policies representable by a decision tree of depth at most $k$ — reduces to a finite search over rectangular families of tree parameterizations, with each family overapproximated by a sub-MDP. For a family $F$ of parameterizations, the family-MDP $M(\\mathcal{F})$ enables an action exactly in states where some assignment in $F$ could select it, so its optimal policy $\\sigma$ has value at least that of any tree in $F$. If $\\sigma$ itself is $F$-implementable, the SMT encoding returns a witness and the search for that family is done; if not, an unsatisfiable core isolates a small set of critical states, and two harmonizing parameterizations differing in a single variable show where the family must be split. Because every split shrinks a finite domain and each leaf is a single parameterization with a single policy, the loop always terminates and never discards an optimal assignment, which is the content of Theorem 4. On large benchmarks this makes the anytime version of the problem practical: good trees are found early via bounded-depth iteration and tree hints, and the same machinery can repair subtrees of a large tree compositionally.","pith_inferences":["The random-action fallback means the headline size reductions compare policies that may randomize when a leaf action is unavailable against exact policy trees; a reader wanting purely deterministic, always-available leaf actions is looking at a different, harder optimization target than the one Theorem 4 certifies.","The template-and-harmonization recipe is not specific to depth-bounded trees: any policy class that admits a finite parameterization and a harmonizing split could in principle be synthesized by the same abstraction-refinement scheme.","Because the algorithm's baseline is the uniform-random 0-tree, its normalized-value reports could be used to pick the smallest depth that meets a performance budget, turning depth selection into a simple online stopping rule."],"forward_implications":["For any MDP and depth bound $k$ for which a good $k$-implementable policy exists, the algorithm will eventually return the best one instead of settling for a compression of a precomputed table.","The optimality guarantee must be read with the random-fallback semantics: a leaf naming an action unavailable in a state plays $\\alpha_{\\mathrm{rand}}$, and this is why a depth-0 tree can already be optimal for models like ij-20.","On the tested models with up to 10k states, the SMT-based approach outperforms the monolithic MILP approach, and the advantage grows with depth because the abstraction-refinement loop prunes rather than enumerates.","When paired with a heuristic policy-to-tree mapper, the same machinery reduces large trees, for example from 236 to 22 inner nodes on a 1.5M-state model, while losing less than 1% of optimal value."],"supporting_citations":[{"why":"states the bounded-depth synthesis problem and supplies the MILP-based baseline and the benchmark instances.","marker":"[40]"},{"why":"provides the heuristic policy-mapping tool whose trees are the size and value baselines.","marker":"[5]"},{"why":"introduces the abstraction-refinement loop for families of Markov chains that Algorithm 1 is modelled on.","marker":"[13]"},{"why":"gives the NP-completeness of optimal binary decision trees used in the hardness reduction.","marker":"[29]"},{"why":"introduces propositional encodings of decision-tree structure that the SMT encoding adapts.","marker":"[33]"},{"why":"is the source of the theorem that optimal memoryless deterministic policies exist, validating the random-action construction.","marker":"[34]"},{"why":"is the model checker used to compute optimal policies for the family-MDPs in the loop.","marker":"[23]"},{"why":"is the SMT solver used to answer the mapping and harmonization queries.","marker":"[32]"}],"fun_headline_variants":["SMT loop provably shrinks MDP policy trees to optimal size","SMT-based abstraction-refinement finds small optimal MDP trees","Provably optimal small decision trees from SMT synthesis","20x smaller policy trees via SMT and abstraction-refinement","SMT encodes bounded-depth MDP policies into small trees"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole optimality result depends on the convention that a leaf action unavailable at a state is replaced by the uniform random action, so the class of $k$-implementable policies contains randomized fallback behavior rather than only deterministic policies whose leaf actions are always available.","fun_headline_variants_meta":{"raw":{"variants":["SMT loop provably shrinks MDP policy trees to optimal size","SMT-based abstraction-refinement finds small optimal MDP trees","Provably optimal small decision trees from SMT synthesis","20x smaller policy trees via SMT and abstraction-refinement","SMT encodes bounded-depth MDP policies into small trees"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000244,"raw_usage":{"total_tokens":1551,"prompt_tokens":982,"completion_tokens":569,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":598,"completion_tokens_details":{"reasoning_tokens":484}},"tokens_in":598,"tokens_out":569,"duration_ms":6077,"temperature":1.0,"reasoning_tokens":484,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T19:23:08.870094+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a small benchmark such as lake-4, fix $k=2$, exhaustively enumerate every depth-2 decision tree over the allowed predicates, and compare the maximum value of that enumeration with dtPaynt's output; any gap would refute Theorem 4. A cheaper conceptual check is to modify the fallback rule so leaves may only name available actions; if the best value drops, the paper's optimality claim is tied to the randomized-fallback semantics rather than to fully realizable deterministic trees.","supporting_citations":[{"cited_title":"In: IJCAI","cited_arxiv_id":null,"evidence_quote":"states the bounded-depth synthesis problem and supplies the MILP-based baseline and the benchmark instances."},{"cited_title":"In: TACAS","cited_arxiv_id":null,"evidence_quote":"provides the heuristic policy-mapping tool whose trees are the size and value baselines."},{"cited_title":"In: TACAS","cited_arxiv_id":null,"evidence_quote":"introduces the abstraction-refinement loop for families of Markov chains that Algorithm 1 is modelled on."},{"cited_title":"Information processing letters 5(1), 15–17 (1976)","cited_arxiv_id":null,"evidence_quote":"gives the NP-completeness of optimal binary decision trees used in the hardness reduction."},{"cited_title":"In: IJCAI","cited_arxiv_id":null,"evidence_quote":"introduces propositional encodings of decision-tree structure that the SMT encoding adapts."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"is the model checker used to compute optimal policies for the family-MDPs in the loop."},{"cited_title":"In: TACAS","cited_arxiv_id":null,"evidence_quote":"is the SMT solver used to answer the mapping and harmonization queries."}],"review_version":1}