{"id":"f589e979-79f1-4eda-80ea-8726ec2827ed","arxiv_id":"2412.10917","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"An adaptive reward-shaping method that periodically inflates distance-to-acceptance values for under-progressed stages lets RL agents reach the best achievable task progression on co-safe LTL tasks within a finite number of updates.","lead":"This paper gives reinforcement learning agents a way to earn points for getting closer to finishing a task written in linear temporal logic, and a loop that periodically rewrites those points when the agent gets stuck. On benchmark robot tasks it beats the usual reward-machine baselines in most settings, with a formal guarantee that comes with caveats about how the rewards are updated.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The proof of Theorem 1 relies on the unargued equality R_ap,k+1 = R_ap,k + θ for the transition into B_b*, which fails when that transition starts below b_k or when ρ0 dominates; the theorem also omits the 'sufficiently large θ' condition.","rationale":"The paper's empirical contribution is substantial: 10-trial comparisons with confidence intervals across four domains and three noise regimes, released code, and an honest outlier discussion (noisy office world) plus a case where the naive baseline matches (half-cheetah). The central formal claim, however, is Theorem 1, and the proof in Appendix A is the only support for the claim of finite convergence to the best task progression. The proof's worst-case analysis contains a specific unargued equality that fails in identifiable settings: the transition that first crosses below b_k may not be the transition into B_{b*}, and the max with the original progression reward ρ0 can absorb the θ increment. This is not a matter of disagreement with consensus; it is an internal correctness gap in the presented argument. The theorem statement also omits the 'sufficiently large θ' condition that the proof itself requires, and the algorithm's update trigger uses an estimated success-rate threshold rather than the exact b_k. These are fixable with a corrected statement (quantifying θ or changing the update rule to use the observed best progression), and a k=0 baseline would strengthen the empirical ablation. Hence the reader's CONDITIONAL verdict is appropriate; our concern identifies a sharper defect in the proof than the general 'optimality assumption' concern, but it does not change the verdict.","tokens_in":14405,"tokens_out":15068,"duration_ms":134733,"concrete_test":"Build a three-state tabular product MDP with partitions B2 (start) → B1 → B0 (accept), transition B2→B1 with probability 0.5 and B1→B0 with probability 1, and set d0 = (2,1,0), b_k = 2, θ = 10, and ρ0(B1,B0) = 100. Compute exact optimal policies under R_ap,0 and R_ap,1 (e.g., by value iteration). If the best-progression policy's value gain from R_ap,0 to R_ap,1 is less than p γ^{H-1} θ, then the Appendix A equality is violated; if no sufficiently large θ restores the claimed strict improvement without violating an omitted condition, Theorem 1 as stated is false.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Appendix A's proof of Theorem 1 considers a policy π achieving b* and asserts that for the (single) transition into B_{b*} the reward satisfies R_ap,k+1 = R_ap,k + θ. This is not generally true. Equation 5 updates only states with partition index i ≥ b_k, where b_k = b(π*_k) > b*. If b* < b_k, the last transition into B_{b*} can originate from B_i with i < b_k (e.g., B_1 when b_k=2); then neither the source nor the destination is updated, so the reward is unchanged. Even when the source has i ≥ b_k, R_ap = max{ρ0, ρk}, so the gain is θ only if the updated ρ_{k+1} exceeds the original progression ρ0; otherwise the gain is smaller or zero. The proof's lower bound V^π_{R_{k+1}} ≥ V^π_{R_k} + p γ^{H-1} θ is therefore not established, and the stated threshold θ > σ/(p γ^{H-1}) is insufficient. The theorem statement also omits this 'sufficiently large θ' condition, and the implemented update rule (triggered by average success rate < λ) does not provide the exact b_k assumed in Eq. 5. As written, the formal guarantee does not follow from the proof and does not cover the evaluated algorithm.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes an adaptive reward-shaping framework for reinforcement learning with co-safe LTL specifications. It defines rewards based on a DFA distance-to-acceptance progression function and periodically updates the distance values by adding a scaling factor theta to states whose partition index is at least the current task progression. Two reward families are introduced, adaptive progression and adaptive hybrid, and Theorem 1 claims that after finitely many updates an optimal policy of the shaped product MDP maximizes expected return while also achieving the best possible task progression. The empirical section compares the method with reward-machine baselines in office, taxi, water, and HalfCheetah domains under deterministic, noisy, and infeasible variants, reporting generally improved success rates and normalized returns.","tokens_in":14740,"tokens_out":6766,"duration_ms":63889,"significance":"If the formal guarantee were correct, this would be a useful contribution: it directly addresses the sparse-reward problem for LTL-specified tasks, is compatible with several deep RL algorithms, is evaluated across diverse domains, and ships code. The experimental study also includes an infeasible-task setting that is relevant for real deployments. However, the central correctness claim is not established by the current proof, and the theorem does not match the implemented algorithm. The contribution is therefore currently best viewed as an empirical reward-shaping heuristic with an unproven convergence certificate; the formal part needs substantial repair.","major_comments":[{"comment":"The key inequality in the proof is not established. The proof asserts that for the final transition into B_{b*} one has R^⊗_{ap,k+1} = R^⊗_{ap,k} + θ. By Eq. (5), only states in B_i with i ≥ b_k receive the increment θ. If b* < b_k, the source of the transition into B_{b*} can have partition index i with b* < i < b_k (e.g., B_1 when b*=0 and b_k=2), in which case neither the source nor the destination is updated and the reward is unchanged. Even if the source is updated, Eq. (7) takes the maximum of ρ^0 and ρ^k, so the reward gain is θ only when ρ^k + θ exceeds ρ^0; otherwise the gain is smaller or zero. Consequently, the claimed lower bound V^π_{ap,k+1} ≥ V^π_{ap,k} + pγ^{H-1}θ is not guaranteed, and the threshold θ > σ/(pγ^{H-1}) is insufficient.","section":"Appendix A, proof of Theorem 1"},{"comment":"The theorem statement omits the 'sufficiently large θ' condition that the proof requires. The proof in Appendix A introduces the condition θ > σ/(pγ^{H-1}), where σ, p, and γ depend on the unknown MDP and on the policies under consideration. This condition is load-bearing, and without it the theorem as stated is not supported. The condition must appear in the theorem statement or the claim must be weakened accordingly.","section":"Section 4.2, Theorem 1 statement"},{"comment":"There is a mismatch between the idealized assumptions of the proof and the algorithm actually evaluated. Eq. (5) uses b_k, the task progression of the exact optimal policy of the current reward, and Appendix A assumes that π*_k is the exact optimal policy and that b_k is known. The algorithm in Section 4.2 instead runs N episodes of approximate RL and triggers an update when the average success rate falls below a threshold λ, without measuring b_k exactly. If the learned policy is suboptimal or the success-rate proxy misestimates the task progression, Eq. (5) can update rewards for the wrong stages, and Theorem 1 provides no guarantee for the implemented procedure.","section":"Section 4.2 vs. Appendix A"},{"comment":"The proof for the adaptive hybrid reward function does not go through. Lemma 1 only shows that lim_{k→∞} R^⊗_{ah,k} = R^⊗_{ap,k}, while Theorem 1 claims existence of a finite k for which the optimal policy of R^⊗_{ah,k} achieves b*. Convergence in the limit does not imply equality at any finite index, so the 'without loss of generality' reduction to the adaptive progression case is invalid without an additional argument bounding the finite-k discrepancy and its effect on the optimal policy.","section":"Appendix A, proof for R^⊗_{ah,k}"}],"minor_comments":[{"comment":"The formula for h(q,q') uses an undefined symbol 'n'; it should be clarified (likely 2^{|AP|} or a similar normalizing constant).","section":"Eq. (1)"},{"comment":"The text says 'θ1 = 100' where the intended expression appears to be 'θ = 100'.","section":"Example 8"},{"comment":"The statement 'requiring that θ > 1' is much weaker than the threshold θ > σ/(pγ^{H-1}) used in the proof; the relationship between these two conditions should be stated explicitly.","section":"Section 4.2"},{"comment":"In the HalfCheetah description, 'reaching the farthest location' and 'each of the five locations along the way' would benefit from a precise definition of the locations and the episode horizon, since the distance-based reward may otherwise be ambiguous.","section":"Section 5.1"},{"comment":"The ablation plots would be easier to read if the legend identified which curves correspond to which θ and N values; several curves appear to overlap substantially.","section":"Figures 5 and 6"}],"recommendation":"major_revision","confidential_remarks":"The stress-test concerns raised by the reader are accurate and coincide with my own reading of Appendix A. The central formal claim is not proven as stated, and the theorem/algorithm mismatch is substantial. The empirical study is a useful contribution, but the formal guarantee needs either a repaired proof or a substantially weakened statement. I would not recommend rejection because the underlying idea is plausible and the experiments are suggestive; however, the revision must address the proof gaps and the algorithm/theorem mismatch before the paper can be accepted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: worth a serious referee, but the Theorem 1 proof as written doesn't go through. The practical method is new and the experiments are honest; the formal guarantee needs repair.\n\nWhat's new: the adaptive update of distance-to-acceptance values (Eq. 5), the two adaptive reward functions (Eqs. 7-8), and the finite-update convergence claim. Each component is borrowed (co-safe LTL to DFA, Lacerda's progression, Ng's shaping), but the adaptive mechanism is theirs. The problem they address is real: static progression rewards can make the optimal policy prefer partial progress over completion, and their examples in Section 4.1 show this clearly. The experiments cover four environments, three noise regimes, 10 trials with 95% CIs, and they honestly flag the noisy office world outlier and HalfCheetah where the naive baseline matches. That is credible empirical work.\n\nThe soft spot is the correctness proof. The stress-test note is right: Appendix A asserts R_ap,k+1 = R_ap,k + theta for the single transition into B_b*, but this is not generally true. Eq. 5 updates only states in partitions i >= b_k, so if b* < b_k, the transition into B_b* can start from a partition below b_k and get no update. And the max with rho^0 means the gain is theta only if the updated rho exceeds the original progression. So the lower bound V^pi_{R_{k+1}} >= V^pi_{R_k} + p gamma^{H-1} theta is not established. The theorem statement also omits the \"sufficiently large theta\" condition that the proof itself invokes (theta > sigma/(p gamma^{H-1})). That condition depends on unknown quantities, which is fine for an existence proof, but it must be stated. There is a second gap between the idealized setting in the proof (exact optimal policies, exact b_k) and the implemented algorithm (N episodes of RL, success-rate threshold lambda, estimated progress). The proof does not cover the evaluated algorithm.\n\nNeither gap makes me think the method is wrong. The empirical evidence is decent and the idea is sound. But the paper currently claims a formal guarantee that is not proven. Fixable: correct the theorem statement, repair or replace the Lemma 2 argument, add a discussion of the optimality assumption, and add a k=0 (static progression) baseline to isolate the adaptive mechanism. The ablation currently varies theta and N but never compares against the static version.\n\nBottom line: a good paper for an applied RL or robotics venue, but it needs a corrected proof and a cleaner ablation before it should appear. Send it to peer review; just don't accept the proof as-is.","headline":"Adaptive distance-based reward shaping is a genuinely useful practical contribution, but the formal correctness proof has a real gap that should be fixed before publication.","tokens_in":15301,"tokens_out":1630,"would_cite":true,"duration_ms":14107,"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":"The paper claims that adaptively updated task-progression rewards make an RL agent's optimal policy both maximize expected return and attain the best possible task progression for a co-safe LTL specification, within finitely many updates.","keywords":["reward shaping","linear temporal logic","task progression","co-safe LTL","automaton-based rewards","reinforcement learning","product MDP","adaptive reward update"],"falsifier":"Run the adaptive update on a two-stage product MDP in which the policy that reaches the accepting state has lower expected return than a policy that stops one stage earlier, and set the update size $\\theta$ below $\\sigma/(p\\gamma^{H-1})$ with the initial distance-to-acceptance rewards; if the updated reward's optimal policy still stops early, the finite-update improvement claimed by Theorem 1 has been falsified in that instance.","tokens_in":14149,"feed_emoji":"🎯","tokens_out":8033,"duration_ms":68126,"temperature":0.7,"pith_summary":"This paper asks how to give an RL agent a reward signal for a task expressed as a co-safe Linear Temporal Logic (LTL) formula when task completion may be rare or impossible. It defines task progression through the distance of the task automaton's states to acceptance, then designs progression and hybrid rewards on the product of the environment and the task automaton. Because optimal policies for these fixed rewards can prefer stalling or the wrong sub-goals, the paper adds an adaptive loop that periodically updates the distance-to-acceptance values so that continuing to make progress becomes increasingly rewarding. The stated result is that, within finitely many updates, an optimal policy of the updated reward both maximizes expected return and achieves the best task progression possible in the environment. Computational experiments across discrete and continuous benchmarks indicate earlier convergence to higher success rates and returns than reward-machine baselines.","feed_headline":"Adaptive rewards make RL agents finish more LTL tasks","feed_subtitle":"Periodic reward updates yield earlier convergence and higher returns, even when goals are infeasible.","key_machinery":"The load-bearing object is the product MDP $M^\\otimes = M \\otimes A_\\varphi$ formed from the environment MDP and the deterministic finite automaton for the co-safe LTL task. On its states the paper defines a distance-to-acceptance function $d_\\varphi(q)$, zero on accepting states, and a task-progression function $\\rho_\\varphi(q,q') = \\max\\{0, d_\\varphi(q)-d_\\varphi(q')\\}$ for non-cyclic DFA transitions. The adaptive update in Eq. 5 adds a constant $\\theta$ to $d_\\varphi(q)$ for every DFA state in partitions indexed at least the current policy's task progression $b_k$, which makes the transition that finally lowers the partition index carry extra reward $\\theta$ in the next round; the adaptive hybrid variant pairs this with a self-loop penalty whose weight decays as $\\eta_k = \\eta_{k-1}/\\theta$. The proof mechanism is the threshold condition $\\theta > \\sigma/(p\\gamma^{H-1})$, which forces the better-progression policy's expected return to surpass the current optimum and yields strict descent in $b(\\pi^*_k)$ until $b^*$ is reached.","core_discovery":"The central claim is Theorem 1: given an episodic MDP and a DFA for a co-safe LTL formula, there exists an update round $k$ such that an optimal policy of the product MDP $M^\\otimes = M \\otimes A_\\varphi$ under the adaptive progression reward $R^\\otimes_{ap,k}$ or the adaptive hybrid reward $R^\\otimes_{ah,k}$ maximizes expected return while attaining the best possible task progression $b^*$. The adaptive step adds a positive offset $\\theta$ to the distance-to-acceptance values of every DFA state whose partition index is at least the current policy's progression level, so the specific transition that carries the agent into a strictly better partition gains an extra $\\theta$ of reward in the next round. Repeating this makes the best-progression policy overtake the current optimum once $\\theta > \\sigma/(p\\gamma^{H-1})$, where $\\sigma$ is the return gap and $p$ the probability of the breakthrough path; since progression values are bounded, only finitely many updates are needed.","pith_inferences":["A natural extension is to apply the same update rule to any finite-state task monitor with a well-founded distance-to-acceptance, such as LTLf or general reward machines, since only the automaton's state partition and reachability are used.","In practice one could estimate $b_k$ from rollouts instead of assuming an exact optimal policy; the update would then be approximate, and the finite-update guarantee would become probabilistic or conditional on estimation accuracy.","The reported outlier in the noisy office world offers a direct stress test: if the adaptive reward's optimal policy there does not attain $b^*$, the gap is either in the approximate RL step or in the reward design itself, and the theorem's conditions identify which assumption to inspect."],"forward_implications":["For any co-safe LTL task, an agent that maximizes expected return under the adaptively updated reward should also reach the best reachable task stage within finitely many updates, rather than only maximizing a shaped proxy.","Because the reward is Markovian on the product MDP, it can wrap around standard deep RL agents without changing the learning rule; the paper demonstrates this with value-based, actor-critic, and policy-gradient algorithms across discrete and continuous environments.","In environments where some sub-goals are impossible, the adaptive reward still distinguishes useful sub-task progress from failure, so the agent learns meaningful partial behavior where sparse or potential-based baselines fail.","The update interval $N$ and scale $\\theta$ control a practical trade-off: the ablation suggests feasible tasks prefer longer intervals and larger $\\theta$, while infeasible tasks benefit from smaller $\\theta$ and more frequent updates."],"supporting_citations":[{"why":"Supplies the distance-to-acceptance and task-progression definitions that the adaptive rewards update.","marker":"[Lacerda et al., 2019]"},{"why":"Establishes potential-based reward shaping, the theoretical baseline for shaping without altering optimal policies.","marker":"[Ng et al., 1999]"},{"why":"Shows LTL specifications translate to reward machines via DFA construction and provides a primary baseline.","marker":"[Camacho et al., 2019]"},{"why":"Provides the reward-machine learning algorithms QRM, CRM, and HRM used as baselines and the source of several benchmark environments.","marker":"[Icarte et al., 2022]"},{"why":"Underlies the conversion of co-safe LTL formulas to DFAs accepting exactly the good prefixes.","marker":"[Kupferman and Vardi, 2001]"}],"fun_headline_variants":["Adaptive rewards boost RL on LTL tasks","Reward shaping that adapts improves LTL task completion","Adaptive reward updates lead to better LTL policies","Adaptive rewards improve LTL task completion rates","Reward updates that adapt boost LTL goal completion"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof treats the current learned policy as truly optimal for the current reward and assumes its task-progression level $b_k$ is known exactly, and it requires the update size $\\theta$ to exceed a threshold $\\sigma/(p\\gamma^{H-1})$ that depends on the unknown MDP; when the RL policy is approximate and evaluation is short, these conditions need not hold and the guarantee can stop applying.","fun_headline_variants_meta":{"raw":{"variants":["Adaptive rewards boost RL on LTL tasks","Reward shaping that adapts improves LTL task completion","Adaptive reward updates lead to better LTL policies","Adaptive rewards improve LTL task completion rates","Reward updates that adapt boost LTL goal completion"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000417,"raw_usage":{"total_tokens":2135,"prompt_tokens":912,"completion_tokens":1223,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":528,"completion_tokens_details":{"reasoning_tokens":1148}},"tokens_in":528,"tokens_out":1223,"duration_ms":8270,"temperature":1.0,"reasoning_tokens":1148,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T15:31:30.679841+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the adaptive update on a two-stage product MDP in which the policy that reaches the accepting state has lower expected return than a policy that stops one stage earlier, and set the update size $\\theta$ below $\\sigma/(p\\gamma^{H-1})$ with the initial distance-to-acceptance rewards; if the updated reward's optimal policy still stops early, the finite-update improvement claimed by Theorem 1 has been falsified in that instance.","supporting_citations":[{"cited_title":"Probabilistic planning with formal performance guarantees for mobile service robots","cited_arxiv_id":null,"evidence_quote":"Supplies the distance-to-acceptance and task-progression definitions that the adaptive rewards update."},{"cited_title":"Ltl and beyond: Formal languages for reward function specification in reinforcement learning","cited_arxiv_id":null,"evidence_quote":"Shows LTL specifications translate to reward machines via DFA construction and provides a primary baseline."},{"cited_title":"Reward machines: Exploiting reward function structure in reinforcement learning","cited_arxiv_id":null,"evidence_quote":"Provides the reward-machine learning algorithms QRM, CRM, and HRM used as baselines and the source of several benchmark environments."},{"cited_title":"Model checking of safety properties","cited_arxiv_id":null,"evidence_quote":"Underlies the conversion of co-safe LTL formulas to DFAs accepting exactly the good prefixes."}],"review_version":1}