{"id":"4bb7acd6-f557-4e05-aac8-64762b931432","arxiv_id":"2511.02304","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"ACC-MARL trains decentralized multi-agent policies that solve many automaton-specified cooperative tasks at once, with a proof of optimality for the Markovian reformulation and value-based task assignment.","lead":"This paper trains multiple AI agents to cooperate on tasks written as simple state machines, so one set of policies can handle many different missions instead of retraining for each one. It proves the training setup preserves optimality in the limit and shows agents learning to hold doors open and help each other finish tasks faster.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Per-agent PBRS in Eq. (6) is not policy-invariant in this episodic setting: nonzero terminal potentials make the telescoping shaping term depend on completion time, so the shaped objective can favor fast-but-suboptimal policies; the cited [5] invariance does not apply.","rationale":"The reader identified exactly the same weak point. I independently checked §3.3 and Appendix B.1. Theorem 1's proof only establishes equivalence between the original history-dependent game and the Markovian product game with the sparse team reward; it does not touch reward shaping. The only justification for Eq. (6) is a citation to [5]. Standard PBRS invariance (Ng et al., and Devlin-Kudenko) requires that the total shaping term telescopes to a policy-independent constant. In this episodic product game, with terminal potential Φ_i(A)=1 if A[i]=A_top, the telescoped term is γ^TΦ_i(A_T)−Φ_i(A_0), which is not constant: for a successful agent it is γ^T (or γ^T−1 if the agent started accepted), and for a failed agent it is 0. So slower successful episodes are penalized. This can change the argmax. Since the paper's Contributions and Section 3.3 explicitly claim that maximizing the shaped objective preserves optimality w.r.t. Problem 1, this is a central theoretical gap. A minimal exact DP counterexample would settle it; if the counterexample shows divergence, Sections 3.3–3.5 overclaim and the paper should condition acceptance on a corrected invariance proof (e.g., zeroing Φ at terminal or proving episodic invariance). The empirical results remain useful, so CONDITIONAL rather than REJECT is appropriate.","tokens_in":19158,"tokens_out":9602,"duration_ms":107683,"concrete_test":"Build a minimal episodic two-agent MDP where each agent has a safe action (always succeeds, takes 2 steps) and a risky action (succeeds with probability 0.5, takes 1 step); team success requires both agents' DFAs accepted. Solve exactly by dynamic programming/value iteration on the finite product MDP for J(π) (Eq. 1) and for the per-agent shaped objective (Eqs. 5–6 with γ=0.99 and defaults Φ_i). If the argmax policies differ, Eq. (6) does not preserve optimality w.r.t. Problem 1. To isolate the per-agent issue, repeat with the same global potential Φ=Σ_iΦ_i applied identically to both agents; if this also diverges, the terminal-potential failure is independent of the multi-agent asymmetry. A JAX implementation can enumerate all deterministic policies in <1s.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing step is the optimality-preservation claim for the full ACC-MARL pipeline, which depends not on Theorem 1 alone but on §3.3, Eq. (6). There, each agent's reward is shaped with Φ_i(A)=1[A[i]=A_top], and the paper says maximizing this shaped objective 'preserves optimality' citing [5]. That citation does not cover this setup for two reasons. (i) Nonzero terminal potentials: episodes stop when A_{t+1}∈D_T^n or s_{t+1}∈S_T. For an agent whose DFA is accepted at termination, Φ_i(A_T)=1, not 0. The discounted telescoping sum of γΦ_i(A_{t+1})−Φ_i(A_t) is γ^TΦ_i(A_T)−Φ_i(A_0), which depends on the completion time T and on whether that agent succeeded. Thus the shaped return differs from the original return by a policy-dependent term; standard PBRS policy invariance assumes terminal potential is zero (or an infinite-horizon proper policy with γ^TΦ→0). (ii) Per-agent potentials: agents are trained with different shaping functions, so no single potential transformation of the team reward is being optimized. If one instead interprets the method as optimizing Σ_i R^(i), the extra term is γΦ_tot(A_T)−Φ_tot(A_0), again nonconstant at terminal states (Φ_tot is the number of completed agents). Consequently a fast, unreliable policy can dominate a slow, certain team-optimal policy under the shaped objective even in the γ→1 limit. A helper agent whose DFA is initially A_top also receives γ−1<0 at every nonterminal step, an artifact of the nonzero initial potential. Appendix B.1 proves only the unshaped Markovian reformulation and does not address Eq. (6); the Limitations section does not flag this.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes ACC-MARL, a framework for multi-task cooperative multi-agent reinforcement learning with tasks specified as deterministic finite automata (DFAs). The authors identify three challenges — history dependency, sparse team reward, and a representation bottleneck — and propose three corresponding remedies: (i) a Markovian reformulation in which agents observe the current minimal DFA of every agent's task; (ii) per-agent potential-based reward shaping designed to densify the team reward; and (iii) the use of pretrained RAD embeddings for DFA representations. The paper gives a formal problem statement (Problem 1), proves a Theorem 1 that the Markovian reformulation is asymptotically optimal as the discount factor tends to 1, asserts that the reward shaping preserves optimality, asserts that RAD embeddings carry over to a modified encoder, and proposes using learned value functions for optimal task assignment at test time. Experiments on Button and Room environments with two and four agents are reported, including ablations and a qualitative analysis of coordinated behaviors.","tokens_in":19601,"tokens_out":9146,"duration_ms":108192,"significance":"If the theoretical claims were correct, the paper would make a useful contribution to multi-agent RL with symbolic temporal specifications: it would provide a principled way to convert a non-Markovian team task into a Markovian one, a dense reward that provably does not change the optimal policy, and a scalable latent representation for DFA-conditioned policies. The empirical results, particularly the four-agent experiments and the qualitative demonstrations of door-holding and short-circuiting, are suggestive and the code release (DFAx, ACC-MARL) is a practical asset. The main source of value is the combination of a formal framework with a working implementation. However, the formal claims are currently under-supported, and one of them — the optimality of the shaped reward — is undermined by a standard and well-known failure mode of potential-based shaping with nonzero terminal potentials.","major_comments":[{"comment":"The claim that the per-agent shaped reward preserves optimality is not correct for the given potential. Summing the shaping term over an episode gives γ^T Φ_i(A_T) − Φ_i(A_0), and since terminal states of the product DFA space include all-trivial vectors, an agent whose task is satisfied has Φ_i(A_T)=1. Thus the shaped return differs from the original return by a policy-dependent quantity that rewards both faster completion and the agent's own success rather than team success. For example, a helper agent whose DFA is initially A_top receives −(1−γ) at every nonterminal step, penalizing longer episodes even when they are necessary for team success. The cited result [5] is for a common potential and, in the general case, assumes zero (or asymptotically vanishing) terminal potential. This is a load-bearing error: the proof that ACC-MARL solves Problem 1 relies on this step. The authors must","section":"Section 3.4, Eq. (7) and Appendix B.4"},{"comment":"The paper asserts that the RAD encoder Ψ satisfies the injectivity condition (7), and then uses this condition to claim that the latent-space reformulation over Z^n is equivalent to the DFA-space reformulation. However, the actual encoder is a modified GATv2 with a different featurization: DFA transitions are treated as edges rather than nodes, and the update rule (Appendix B.4) differs from the architecture in the cited works. No proof or reference is provided that this modified encoder preserves injectivity up to DFA minimization. Since the optimality of the π'' policies depends on this equivalence, the assertion is load-bearing. The authors should either supply a theorem for the new architecture, reduce it to the earlier results with explicit conditions, or state the injectivity as an assumption and verify it empirically.","section":"Section 3.5"},{"comment":"The statement that the value-based assignment A★ maximizes the team success probability is not established. The functions V_i are the value functions of policies trained on the shaped objective, which (even ignoring the first concern) are not guaranteed to be optimal for Problem 1. Maximizing a sum of per-agent value functions over assignments does not imply maximizing the joint success probability; a Pareto-optimal point with respect to per-agent values is not necessarily one that maximizes J(π). The formal inequality asserted for all A′ in perm(A) needs a proof. As stated, this is an unsupported theoretical claim, although the experimental results in Rooms-2/Rooms-4 provide some empirical support.","section":"Appendix B.1"}],"minor_comments":[{"comment":"The proof of Theorem 1 interchanges the limit γ→1− with the maximization over policies. Since episodes can in principle be unbounded and the objective is a discounted sum, the authors should justify this interchange (e.g., by bounded rewards and a properness condition) or state the result under an explicit finite-horizon/absorbing assumption.","section":"Appendix B.1"},{"comment":"The paper uses 'potential-based reward shaping' and cites [5] without noting that the standard policy-invariance result applies to the sum of shaping terms over infinite horizons or with zero terminal potential. The text should be explicit about the terminal potential issue, even if a fix is adopted.","section":"Section 3.3"},{"comment":"Helper agents (trivially accepting DFAs) are sampled with positive probability. With the current shaping potential, these agents receive a negative reward at each step before termination. This artifact is not mentioned and can affect learning. Rewriting the potential as suggested would also eliminate this artifact.","section":"Section 4.2"},{"comment":"In Eq. (5), the terminal condition includes A_{t+1}∈D_T^n, but the reward R_D^n only fires when the vector equals A_top. It may be useful to distinguish all-trivial states with some rejecting entries from the all-accepting state; the current notation is slightly ambiguous.","section":"Section 3.2"},{"comment":"The table formatting is dense; the distinction between random and optimal assignment results is not as clear as it could be. Consider using separate rows or a clearer header.","section":"Table 1"}],"recommendation":"major_revision","confidential_remarks":"The paper has a good empirical core and a thoughtful architecture, but the theoretical narrative currently overclaims. The most serious issue is the reward-shaping invariance claim, which is not covered by standard PBRS results and can be falsified with simple examples involving helper agents. The RAD embedding transfer is also asserted rather than proved. I would not recommend rejection, because the framework and experiments may survive a careful rewrite; however, the authors need to either repair the theory with corrected potentials and proofs, or substantially weaken the optimality claims to claims about approximate or heuristic behavior. I would also encourage the authors to add a limitations subsection that explicitly acknowledges the terminal-potential and value-assignment issues."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this is a genuinely useful framework—multi-task, decentralized policies conditioned on DFA progress, with pretrained automata embeddings and a JAX implementation. The central Theorem 1, that the Markovian reformulation preserves the team-success objective as γ→1, is plausible and the appendix proof holds up. The experiments are credible: ablations show each component matters, and the qualitative traces show real emergent coordination (door holding, short-circuiting). The code release is a plus. If I worked on symbolic-task MARL, I would build on this.\n\nThe soft spot is Section 3.3. The per-agent potential shaping in Eq. (6) is not covered by the PBRS invariance theorem they cite. The terminal potentials are nonzero—an agent whose DFA is accepted at the end has Φ_i=1—and the potentials differ across agents, so the telescoping term is γ^{T+1}Φ_i(A_T)−Φ_i(A_0), which depends on completion time and on whether that agent is a helper. For any fixed γ<1, that term favors faster completion and penalizes helpers for every step before success. The limit as γ→1 does not obviously recover the unshaped team objective, because the convergence is not uniform over policies: a fast-but-less-reliable policy can have higher shaped return for every γ<1 while the unshaped limit favors the slower certain policy. So the claim 'maximizing this objective preserves optimality' is not supported. This is a genuine gap in the theoretical contribution, though not in the empirical one—the ablations show PBRS helps in practice.\n\nTwo smaller things. The 'optimal task assignment' in Section 3.5 is a heuristic: summing learned value functions over permutations and calling the argmax Pareto optimal is stated without proof, and the learned value functions are from IPPO with shaped rewards, not necessarily optimal. The experiments justify it as a heuristic, not as optimality. Also, the injectivity of the modified edge-featurized GATv2 encoder is asserted from prior work that used a different architecture; that probably needs checking, but it is minor compared to the shaping issue.\n\nBottom line: this paper deserves a serious referee. The empirical contribution is solid and the framing is useful. But the authors need to either prove the shaping claim under the terminal-potential condition or explicitly frame it as a heuristic that works in practice, and tone down the optimality language accordingly.","headline":"Solid empirical framework for automata-conditioned MARL, but the optimality proof for reward shaping has a real gap.","tokens_in":20116,"tokens_out":7474,"would_cite":true,"duration_ms":81072,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"By feeding each agent the minimized automaton remaining for every task, the paper turns a non-Markovian cooperative planning problem into a Markovian game and proves the reformulation is optimal in the infinite-horizon limit.","keywords":["multi-agent reinforcement learning","deterministic finite automata","automata-conditioned policies","potential-based reward shaping","task-conditioned learning","centralized training decentralized execution","temporal task generalization","RAD embeddings"],"falsifier":"Take a two-agent grid world where one agent's sub-task is reachable by a shortcut that permanently blocks the other agent's path; train with the shaped reward and with the sparse team reward, and check whether the shaped policy converges to the same success probability as the sparse policy as γ→1. Alternatively, evaluate the term γ^T Φ(s_T) − Φ(s_0) under two policies with identical team-success probability but different completion times; if the shaped return differs, the shaping is not policy-invariant and Theorem 1 does not extend to the shaped reward.","tokens_in":19008,"feed_emoji":"🤖","tokens_out":4779,"duration_ms":52152,"temperature":0.7,"pith_summary":"The paper tries to establish that cooperative multi-agent reinforcement learning for temporally extended tasks can be made practical when tasks are given as deterministic finite automata (DFAs). Its core move is to show that the non-Markovian problem of tracking progress through a trace collapses to a Markovian game: at each step, agents observe the minimal DFA remaining after reading the latest labels, and the paper proves (Theorem 1) that maximizing discounted rewards in this reformulated game yields the same optimal policy as the original team-success objective in the limit γ→1. To make learning feasible, it adds potential-based reward shaping per agent, pretrained automata embeddings to avoid learning task representations from scratch, and shows that learned value functions can rank task assignments so the best permutation can be selected at test time. A sympathetic reader would care because this is a path from symbolic temporal specifications to decentralized team policies that scale from two to four agents and generalize across task classes.","feed_headline":"DFA tasks become learnable for cooperative multi-agent teams","feed_subtitle":"Markovian reformulation, reward shaping, and pretrained automata embeddings make temporal team tasks provably learnable.","key_machinery":"The load-bearing construction is the product DFA space D^n with the progression operation A/σ, which maps a vector of assigned DFAs to a vector of minimized residual DFAs after reading the latest labels. This turns the non-Markovian history-tracking problem into an MDP over (state, DFA-vector) pairs. Carrying the argument are: (i) the potential-based shaped reward R_D^n + γΦ_i(T)−Φ_i for each agent, where Φ_i=1 exactly when agent i's residual DFA is trivially accepting; (ii) RAD embeddings, a pretrained encoder Ψ that is injective up to DFA minimization, so the MDP can be compressed to a latent product space Z^n without changing rewards or transitions; and (iii) the induced value function V(","core_discovery":"The central claim is Theorem 1: for a Markov game with n agents and n DFAs drawn from a prior, the joint policy that maximizes the discounted expected reward of the Markovian product game, where each agent observes its current minimized DFA progression, is also optimal for the original problem of maximizing the probability that all agents' traces satisfy their assigned DFAs, in the limit as the discount factor approaches 1. The paper further claims that this remains true after applying potential-based reward shaping with per-agent potential functions that fire when an individual DFA becomes accepting, and that using pretrained, provably correct RAD embeddings in place of the DFAs themselves","pith_inferences":["The progression-based Markovian trick is not limited to DFAs; it should transfer to reward machines, LTL, or any automaton with a progression operation, potentially giving a unified treatment for symbolic multi-agent RL.","A natural testable extension is to use the same value functions to reassign tasks mid-episode, not just at the start; the paper leaves this unexplored, but the framework's state already contains all residual DFAs.","The optimal-assignment argument relies on full observability and enumeration; for larger teams, the RAD embedding space could be searched directly, which the paper itself notes as future work.","If the shaping preservation fails in the multi-agent case (see weakest assumption), the practical gains might still hold but the optimality guarantee would break; a direct test would be to compute shaped versus unshaped returns in a small grid world."],"forward_implications":["In the γ→1 limit, training on the shaped Markovian objective is equivalent to training on the sparse team-success objective, so the framework inherits optimality with respect to the ACC-MARL problem.","Because RAD embeddings uniquely represent minimized DFAs, policies trained on them can be reused across task classes; experiments show generalization to Reach and ReachAvoid tasks and to out-of-distribution DFAs with up to 10 states.","Learned value functions rank task assignments, so at test time the team can enumerate permutations and pick a Pareto-optimal assignment, improving success probability in asymmetric environments like Rooms.","The ablation results show that either removing reward shaping or learning embeddings from scratch degrades performance, particularly in four-agent settings, identifying the two ingredients as necessary for feasibility.","The framework produces emergent cooperative behaviors—button-pressing to unlock doors, door-holding, and task short-circuiting—that are not explicitly rewarded beyond the shaped sub-task signal."],"fun_headline_variants":["Automata-conditioned policies make team tasks provably optimal","DFA-conditioned MARL achieves optimal coordination","Learnable automata make multi-agent team tasks provably optimal","Automata-conditioned multi-agent RL: optimal for temporal team tasks"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The argument that potential-based reward shaping preserves optimality in this multi-agent episodic setting is inherited from the single-agent, zero-terminal-potential theorem in reference [5]; here the terminal potential is nonzero—an agent completing its own DFA receives 1—so the telescoping term γ^T Φ(s_T) − Φ(s_0) is policy-dependent, and the paper provides no proof that the shaped objective has the same optima as the original team-success objective.","fun_headline_variants_meta":{"raw":{"variants":["Automata-conditioned policies make team tasks provably optimal","DFA-conditioned MARL achieves optimal coordination","Learnable automata make multi-agent team tasks provably optimal","Automata-conditioned multi-agent RL: optimal for temporal team tasks"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000774,"raw_usage":{"total_tokens":3227,"prompt_tokens":675,"completion_tokens":2552,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":419,"completion_tokens_details":{"reasoning_tokens":2484}},"tokens_in":419,"tokens_out":2552,"duration_ms":20242,"temperature":1.0,"reasoning_tokens":2484,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T00:12:00.179340+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a two-agent grid world where one agent's sub-task is reachable by a shortcut that permanently blocks the other agent's path; train with the shaped reward and with the sparse team reward, and check whether the shaped policy converges to the same success probability as the sparse policy as γ→1. Alternatively, evaluate the term γ^T Φ(s_T) − Φ(s_0) under two policies with identical team-success probability but different completion times; if the shaped return differs, the shaping is not policy-invariant and Theorem 1 does not extend to the shaped reward.","supporting_citations":[],"review_version":1}