{"id":"42318dad-b2c8-4623-b266-ceaf85c4be5b","arxiv_id":"2412.12700","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":2,"one_line_summary":"ParMod parallelizes learning of LTL_f-specified non-Markovian tasks by classifying DFA states into rank-based task phases and training one agent per phase.","lead":"ParMod splits tasks written in temporal logic into phases using the task's automaton, then trains one reinforcement-learning agent per phase in parallel. The authors report faster training and higher success rates than several automaton-based RL baselines on continuous-control benchmarks.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 4's optimality proof is unsupported: terminal-state bootstrapping and nonzero terminal potential shaping can move the fixed point away from the product MDP's Q*.","rationale":"The paper's empirical work is substantial: open-sourced code, multiple continuous benchmarks, and consistent advantages over the selected baselines. Those results do not, however, establish the central optimality claim. On the reader's weakest assumption, I only partly agree: the statement that modular Q-functions collectively equal the global Q-function is close to a definition, since the global table can be taken as the disjoint union of the Q_k over ranks; the cross-rank bootstrap then matches standard Q-learning. The genuinely unproven parts are the terminal-state treatment and the reward shaping with nonzero terminal potentials. Both are visible in Algorithm 2 and neither appears in the proof of Theorem 4. The proof also never addresses Theorem 3's Equation 4, where E[gamma^L] is replaced by P(s0)gamma^L with random L; that invalid identity would be needed to justify the 'minimizes steps / maximizes probability' characterization. For these reasons the rejection is warranted: a revision that either proves convergence for the actual update with explicit terminal states and potential shaping, or drops the optimality theorem and reframes ParMod as an empirical method, would be the appropriate path. My concern does not change the reader's verdict, so I mark the adjustment as unchanged.","tokens_in":23061,"tokens_out":14430,"duration_ms":138563,"concrete_test":"Implement Algorithm 2 in tabular form on a small discrete MDP with a DFA containing accepting and error states and at least one rank shared by multiple DFA states (e.g., a grid version of Task 7 with N=2). Run two variants: (a) the paper's update as written, with terminal next states left undefined; (b) the standard fix Q_terminal = 0. Keep the rank-change reset (line 19) and the paper's potential shaping with rho(F)=C. After every state-action pair has been updated many times, evaluate the greedy policy under the original sparse reward (100 only in F) and compare its expected discounted return with value iteration on M^otimes. If either variant is suboptimal, Theorem 4 is false for that protocol; if both match Q*, the concern is resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"ParMod's central claim is Theorem 4: tabular ParMod converges to an optimal policy under infinite visitation. The proof transfers Q-learning convergence by declaring that the modular Q_k collectively equal the global Q-function. That equality is not the real gap: if one defines Q(s,a) := Q_{rank(s)}(s,a), the cross-rank bootstrap in Algorithm 2 is formally the standard Q-learning bootstrap. The load-bearing gaps are the two places where this reading breaks. First, Algorithm 2 line 22 computes a bootstrap target with k' = rank(q_{i+1}), but Algorithm 1 assigns ranks only to Q \\setminus F \\setminus E. Accepting and error states have no rank, so the update is undefined on exactly the transitions that deliver completion/failure reward. Silently setting Q_terminal = 0 is a convention that neither Algorithm 2 nor Theorem 4 states. Second, line 17 reshapes rewards with potential rho(F)=C and rho(E)=C/(N+1), i.e., nonzero potentials on terminal states. Potential-based shaping is policy-preserving only with zero terminal potential; with nonzero terminal potentials the reshaped return contains gamma^{L+1}rho(F) - rho(s0), which depends on completion time L and changes the tradeoff between success probability and horizon. Therefore the tabular update can converge to the optimum of a reshaped, phase-truncated MDP, not to the optimum of the product MDP asserted in Theorem 4. Neither effect is analyzed in the proof.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes ParMod, a parallel and modular RL framework for non-Markovian tasks (NMTs) specified in LTL_f. The method converts an LTL_f specification into a DFA, partitions the DFA states into ranks (task phases) via Algorithm 1, trains one agent per phase with separate initial-state buffers and experience buffers, and reshapes rewards using a potential function defined over DFA states. The paper claims that ParMod with tabular Q-learning converges to an optimal policy of the product MDP (Theorem 4), and empirically reports faster convergence, higher success rates, and better policy quality than Base, Mod, QRM, IMPALA, and DPPO on continuous benchmarks including Waterworld, Racecar, and Halfcheetah.","tokens_in":23228,"tokens_out":8606,"duration_ms":73793,"significance":"If the theoretical claims were valid, ParMod would be a useful contribution connecting temporal-logic specifications with scalable RL through parallel modular training. The empirical work is extensive: open-source code, 13 tasks, multiple ablations (TPC vs. random classification, SPECTRL reward comparison, distributed version), and comparisons against distributed RL baselines. These engineering and empirical contributions are real and should be credited. However, the theoretical core of the paper is not sound: the convergence proof is circular, the algorithm's update rule is undefined on key transitions, and the reward shaping changes the underlying objective. The paper's central guarantee of optimality is therefore not established, and the theoretical section contains concrete mathematical errors.","major_comments":[{"comment":"The proof of Theorem 4 is circular. It states that \"Q(s⊗,a) actually represents the global Q-function, whose value is equal to Q_k(s⊗,a) for each state-action pair\" and then concludes that Q-learning convergence transfers to the modular Q-functions. That equality is precisely what the cross-rank bootstrap update (Algorithm 2, lines 21-24) must establish; it is assumed without proof. The coupled update equations across ranks define a different operator from standard Q-learning, and no argument shows that its fixed point coincides with the global Q-function.","section":"Section 5, Theorem 4"},{"comment":"The update rule in Algorithm 2 is undefined for transitions into accepting or error states. Algorithm 1 assigns ranks only to states in Q \\ F \\ E, yet line 22 computes k' = rank(q_{i+1}) for every stored experience, including those with q_{i+1} in F or E. The pseudocode therefore does not specify the bootstrap target for exactly the transitions that deliver completion or failure reward. Any convention that sets Q_terminal = 0 is not stated in the algorithm or used in the proof of Theorem 4.","section":"Algorithm 2, line 22; Algorithm 1"},{"comment":"The potential function assigns nonzero potentials to terminal states: rho(F) = C and rho(E) = C/(N+1). Potential-based reward shaping preserves the optimal policy only when terminal-state potentials are zero. With nonzero terminal potentials, the reshaped return of a trajectory ending at time L contains the extra term gamma^{L+1} rho(q_L) - rho(q_0), which depends on the completion time L and on whether the terminal state is accepting or error. Consequently, the tabular Q-learning in ParMod converges to the optimum of the reshaped, phase-truncated MDP, not to the optimum of the original product MDP asserted in Theorem 4.","section":"Section 4.2, reward shaping"},{"comment":"Equation (4) incorrectly replaces E[gamma^L] with P(s0) gamma^L. The expression \"P(s0) gamma^L\" mixes a probability with a random variable; the correct factor is E[gamma^L 1_{success}] (or r E[gamma^L] after conditioning on success). For gamma < 1, maximizing E[gamma^L] is not equivalent to minimizing the expected number of steps, and for gamma = 1 the argument only recovers the success probability if L is independent of the success event, which is not shown. This invalidates the stated characterization of the product MDP's optimal policy.","section":"Section 5, Theorem 3, Eq. (4)"},{"comment":"The convergence proof ignores the phase truncation that is built into Algorithm 2. Line 19 terminates an episode whenever the DFA state reaches a different rank or enters F/E, so each modular Q-function is trained on a truncated sub-MDP. The theorem asserts convergence to the optimal policy of the full product MDP without analyzing how the composition of phase-local value functions, connected by the initial-state buffers and cross-rank bootstrapping, reconstructs the global optimal value. This is a load-bearing gap in the proof.","section":"Section 5, Theorem 4; Algorithm 2, line 19"}],"minor_comments":[{"comment":"There are several typos: \"algorhtims\" should be \"algorithms\", \"nuder\" in the proof of Lemma 1 should be \"under\", and \"is is\" in the proof of Theorem 4 should be \"is\".","section":"Section 4.2"},{"comment":"The text describing Figure 2 mentions \"the accepting state q5\", but the DFA in Figure 3 (used in the running Example 1) has q4 as the accepting state. Please clarify whether Figure 2 uses a different DFA or correct the caption/text.","section":"Section 4"},{"comment":"In the description of the distributed experiment, \"CUP cores\" should be \"CPU cores\".","section":"Section 6.1"},{"comment":"The initial-state buffer notation is inconsistent: the text uses \"B_i\" in Section 4.2 but the algorithm listing uses \"B_k\" without a formal definition of B_k. Please define the buffer symbols consistently.","section":"Algorithm 2"}],"recommendation":"reject","confidential_remarks":"The paper's empirical work is substantial, but its theoretical foundation is not salvageable by modest revision. Theorem 4's proof is circular, the update rule is undefined for terminal transitions, and the reward shaping demonstrably changes the objective. Even if the authors removed the optimality claims, the paper's framing as a theoretically grounded framework would need to change substantially. The comparison against IMPALA/DPPO is encouraging, but it does not compensate for the incorrect guarantees in Section 5. I would recommend rejection, though the authors might resubmit an empirical-focused version if they clearly drop or substantially revise the theoretical claims."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper is worth reading, but not for the reasons it gives itself. The empirical contribution is real: ParMod's parallel phase-based training, rank-based TPC, and cross-rank critic updates are a plausible and well-tested recipe for LTL_f-defined non-Markovian tasks. The experiments are broad and consistently favor ParMod over Base, Mod, QRM, IMPALA, and DPPO, and the code and data are open-sourced. That alone justifies a serious look.\n\nThe theory does not hold up. Theorem 3's Equation 4 replaces E[gamma^L] with P(s0)gamma^L, which is not valid; the expectation of a discounted random completion time does not factor that way. Theorem 4 is the real problem: it assumes the modular Q-functions collectively equal the global Q-function, which is exactly what the cross-rank bootstrap in Algorithm 2 has to prove. The stress-test note is right that if you define Q(s,a) := Q_{rank(s)}(s,a), the bootstrap is formally ordinary Q-learning, but two gaps remain. First, Algorithm 1 assigns ranks only to Q \\ F \\ E, so accepting and error states have no rank; Algorithm 2's bootstrap target on line 22 is undefined for the transitions that actually deliver the completion or failure reward. Silently setting terminal Q to zero is a convention the paper never states or analyzes. Second, the potential shaping in line 17 sets nonzero potentials on terminal states (rho(F)=C, rho(E)=C/(N+1)); potential-based shaping only preserves optimality when terminal potentials are zero. With nonzero terminal potentials, the reshaped return depends on completion time and changes the success/horizon tradeoff. So the tabular update converges to the optimum of a reshaped, phase-truncated MDP, not to the product MDP optimum asserted in Theorem 4.\n\nNone of this is fatal to the empirical method. A revision that either proves convergence for the actual coupled update, or removes the optimality theorem and reframes the paper as an empirical framework, would be honest. The paper also needs error bars or seed-level detail; the current Table 2 gives only 200-run success rates with no variance. The number of phases N is tuned per task, and the paper admits it cannot be determined theoretically—that is acceptable as a limitation but should be stated clearly.\n\nWho is this for? Researchers working on temporal-logic RL and reward machines. They should read the empirical sections carefully and treat the theory as aspirational. I would not reject it out of hand; a serious referee can help the authors fix the framing or the proofs. Send it to review, but expect major revision.","headline":"A genuinely useful modular RL framework with strong empirical results, but the convergence-to-optimality proof doesn't hold as written; worth a serious referee but not acceptance as-is.","tokens_in":23929,"tokens_out":2072,"would_cite":true,"duration_ms":18592,"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":"ParMod claims that a non-Markovian task written in LTL_f can be decomposed by DFA-state ranks into phases, trained in parallel by separate agents, and still converge to an optimal policy of the product MDP.","keywords":["Reinforcement Learning","Temporal Logic","Non-Markovian reward","Parallel training","Reward shaping","Task-phase classification","Product MDP","LTL_f"],"falsifier":"Run ParMod's tabular update from Algorithm 2 on a tiny product MDP (for example, two environment states and a two-state DFA whose rank-0 phase transitions into rank-1) and compare the learned values of each modular Q-table against a standard single Q-learning run on the same product MDP; any difference at a shared state-action pair would falsify the transferred convergence argument.","tokens_in":22702,"feed_emoji":"🧩","tokens_out":9324,"duration_ms":75489,"temperature":0.7,"pith_summary":"This paper is about learning tasks whose reward depends on history, not just the current state. ParMod takes a formal specification in LTL_f, converts it into a deterministic automaton, and splits the automaton states into ranked 'task phases' by their average distance to acceptance. Each phase is trained by its own agent in parallel, with an initial-state buffer that hands the next phase a starting point whenever a phase boundary is crossed, and with rewards shaped by a potential that depends only on the automaton rank. The paper's central claim is that this does not sacrifice optimality: with tabular Q-learning, ParMod is said to converge to an optimal policy of the product MDP under infinite visitation. The value of the claim is practical: if it holds, sparse non-Markovian tasks that defeat monolithic or merely distributed RL become a set of denser, parallelizable sub-problems.","feed_headline":"Parallel phase-splitting RL hits 100% on non-Markovian tasks","feed_subtitle":"Splitting an LTL_f task into ranked sub-tasks with separate agents learns faster than standard or distributed RL.","key_machinery":"The central object is the rank, a task-phase index assigned to each DFA state by the Task Phase Classification (TPC) algorithm: the average graph distance from the state to accepting states is normalized into $N$ ranks. The machinery is the product MDP $M^\\otimes$ whose states are pairs $(s,q)$ of environment state and DFA state; ParMod trains one agent per rank, and its critic TD target for an experience ending in rank $k'$ uses the critic of network $k'$ rather than the current network. Initial-state buffers store product states at phase boundaries to seed later phases, and a potential function $\\rho(q)=C/(N-\\mathrm{rank}(q))$ reshapes rewards as $\\gamma\\rho(q_{t+1})-\\rho(q_t)$ so that every phase transition produces a dense signal. These pieces carry the argument: the partition creates short-horizon sub-problems, the buffers eliminate the exploration bottleneck of late phases, and the shaping is designed to preserve the optimal policy of the product MDP.","core_discovery":"The paper's central discovery is that the memory required by a non-Markovian task can be read off an automaton and turned into a partition of the task into phases: each non-accepting, non-error DFA state gets a rank between 0 and N-1 by normalizing the average distance from that state to the accepting states, and states with the same rank belong to the same phase. ParMod trains one agent per phase, and each agent's critic update uses the next phase's critic rather than its own when the automaton rank changes, so the value signal propagates backward across phase boundaries. Initial-state buffers collected during training let later phases start from states that a single agent would rarely reach, and a potential-based reward shaping term $\\gamma\\rho(q_{t+1})-\\rho(q_t)$ with $\\rho(q)=C/(N-\\mathrm{rank}(q))$ makes the reward dense. The theoretical claim is Theorem 4: ParMod with tabular Q-learning converges to an optimal policy of the product MDP whenever every state-action pair is visited infinitely often. The empirical claim is that on nine benchmarks from Waterworld, Racecar, and Halfcheetah, ParMod reaches a 100% success rate with shorter policies and faster convergence than the flat baseline, the modular DDPG-style baseline, reward-machine Q-learning, and the distributed IMPALA and DPPO baselines.","pith_inferences":["A direct test of Theorem 4 would be to run the tabular update on a small hand-built two-phase product MDP and compare each resulting $Q_k$ with a single global Q-learning run; the paper assumes these coincide but does not verify it.","The rank metric is purely structural; replacing the graph distance with a distance weighted by environment transition probabilities could produce phases that are better matched to actual learning difficulty, and could be tested on the same benchmarks.","The cross-phase critic bootstrap resembles asynchronous value iteration with changing targets; one might prove convergence under a contraction condition on the phase partition, or construct adversarial partitions that break convergence.","Because initial-state buffers resample from product states discovered by previous trajectories, the training distribution is off-policy in a way that standard RL theory does not cover; the framework might benefit from off-policy correction or importance weighting as the number of phases grows."],"forward_implications":["For any NMT expressible in LTL_f, the same pipeline works: formula to DFA, TPC ranks, parallel agents, and shaped rewards; the paper demonstrates it with both SAC and PPO as underlying algorithms.","Because the shaping potential depends only on the DFA state, it should preserve the optimal policy of the product MDP, so the parallel speedup does not change the task being solved.","Tasks with much larger automata (up to 290 DFA states and 1091 transitions in the paper) still show steadily rising reward curves, indicating the decomposition scales beyond the small benchmarks.","The initial-state buffers directly attack the sparse-reward bottleneck: later phases get explored even when a single agent would almost never reach them, which the paper identifies as the reason IMPALA and DPPO fail.","If Theorem 4 is accepted, ParMod acts as a general wrapper: any convergent base RL algorithm can be plugged into the phases and inherit the optimality guarantee."],"supporting_citations":[{"why":"Defines NMRDPs and establishes the product construction that turns non-Markovian rewards into a Markovian MDP, the foundation of ParMod's state space.","marker":"Thiébaux et al. (2006)"},{"why":"Supplies the compositional translation of LTL_f formulas into deterministic finite automata, which ParMod needs to obtain the DFA and its ranks.","marker":"De Giacomo & Favorito (2021)"},{"why":"Provides the Q-learning convergence proof that Theorem 4 relies on to transfer optimality from the global Q-function to the modular Q-functions.","marker":"Melo (2001)"},{"why":"Introduces reward machines and QRM, the automaton-based RRL approach and the baseline against which ParMod is evaluated.","marker":"Icarte et al. (2022)"},{"why":"Presents the Modular DDPG architecture with task dividers that ParMod extends into rank-based parallel phases and compares against as Mod.","marker":"Hasanbeig et al. (2020)"},{"why":"Defines SPECTRL and its reward shaping mechanism, which ParMod compares against in the reward-shaping experiment.","marker":"Jothimurugan et al. (2019)"},{"why":"Provides IMPALA, one of the distributed RL baselines whose failure to reach later task phases motivates the initial-state buffers.","marker":"Espeholt et al. (2018)"},{"why":"Provides DPPO, the second distributed baseline compared in the experiments.","marker":"Heess et al. (2017)"},{"why":"Supplies the Ray distributed framework used for the distributed version of ParMod in the final experiment.","marker":"Moritz et al. (2018)"}],"fun_headline_variants":["Automaton phases guide parallel RL to perfect non-Markovian scores","ParMod: parallel sub-agents solve temporal logic tasks at 100%","From automaton ranks to dense rewards: ParMod masters NMTs","One agent per phase: parallel RL cracks non-Markovian benchmarks","Modular, parallel, and provably optimal: ParMod beats flat RL"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole optimality argument rests on assuming that the value assigned by each phase's own Q-table to a state-action pair is exactly the value a single global Q-table would assign; the paper asserts this equality but does not prove it.","fun_headline_variants_meta":{"raw":{"variants":["Automaton phases guide parallel RL to perfect non-Markovian scores","ParMod: parallel sub-agents solve temporal logic tasks at 100%","From automaton ranks to dense rewards: ParMod masters NMTs","One agent per phase: parallel RL cracks non-Markovian benchmarks","Modular, parallel, and provably optimal: ParMod beats flat RL"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000972,"raw_usage":{"total_tokens":4202,"prompt_tokens":1088,"completion_tokens":3114,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":704,"completion_tokens_details":{"reasoning_tokens":3016}},"tokens_in":704,"tokens_out":3114,"duration_ms":19857,"temperature":1.0,"reasoning_tokens":3016,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T13:50:09.140857+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run ParMod's tabular update from Algorithm 2 on a tiny product MDP (for example, two environment states and a two-state DFA whose rank-0 phase transitions into rank-1) and compare the learned values of each modular Q-table against a standard single Q-learning run on the same product MDP; any difference at a shared state-action pair would falsify the transferred convergence argument.","supporting_citations":[{"cited_title":", & author Favorito, M","cited_arxiv_id":null,"evidence_quote":"Supplies the compositional translation of LTL_f formulas into deterministic finite automata, which ParMod needs to obtain the DFA and its ranks."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the Q-learning convergence proof that Theorem 4 relies on to transfer optimality from the global Q-function to the modular Q-functions."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduces reward machines and QRM, the automaton-based RRL approach and the baseline against which ParMod is evaluated."},{"cited_title":", author Kroening, D","cited_arxiv_id":null,"evidence_quote":"Presents the Modular DDPG architecture with task dividers that ParMod extends into rank-based parallel phases and compares against as Mod."},{"cited_title":", author Alur, R","cited_arxiv_id":null,"evidence_quote":"Defines SPECTRL and its reward shaping mechanism, which ParMod compares against in the reward-shaping experiment."},{"cited_title":", author Soyer, H","cited_arxiv_id":null,"evidence_quote":"Provides IMPALA, one of the distributed RL baselines whose failure to reach later task phases motivates the initial-state buffers."}],"review_version":1}