Pith. sign in

REVIEW 3 major objections 4 minor 30 references

Deontically Constrained Policy Improvement in Reinforcement Learning Agents

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A PCTL-aware policy improvement algorithm provably converges to a feasible local maximizer of mission utility without leaving the allowed behavior set.

desk verdict Theorem 4.2 is unsound — the local action-filtering test does not guarantee global feasibility after later updates, so the paper's central guarantee is broken. read the letter →

arxiv 2506.06959 v1 pith:P3CUP4WA submitted 2025-06-08 cs.AI

Alena Makarova , Houssam Abbas This is my paper · ORCID
classification cs.AI
keywords deonticconstraintsexpectedactutilitarianismstitlogicPCTLconstrainedpolicyimprovementreinforcementlearningMarkovdecisionprocess
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tries to establish a practical way to keep a reinforcement-learning agent inside a normative constraint while it maximizes a separate mission reward. The constraint is written as a Probabilistic Computation Tree Logic (PCTL) formula of the form $P_{\ge\lambda}(\Phi U\Psi)$, and the authors treat it as the content of an Expected Act Utilitarianism obligation, a stit-logic notion in which duties come from expected-utility maximization. Their method is a constrained variant of policy improvement: at each state, only actions whose one-step satisfaction estimate stays above the threshold $\lambda$ are allowed, and the policy is then improved within that restricted action set. The central claim is Theorem 4.2: with greedy updates ($\varepsilon=0$) the procedure converges in finitely many steps to a feasible policy that locally maximizes the constrained utility. If true, this would let an agent optimize its mission without ever leaving the behavior class its deontic constraint permits, and without needing to encode the norm as a reward.

What carries the argument

The carrying mechanism is the admissible-action filter $C^{(t+1)}(s)=\{a\in A(s)\mid Y^{(t+1)}(s,a)\ge\lambda\}$, where $Y^{(t+1)}(s,a)$ is the probability of satisfying the reachability or constrained-reachability path formula after taking action $a$, evaluated with the previous policy's satisfaction vector. This filter is what distinguishes the algorithm from ordinary policy improvement: it removes the constraint from the objective by removing constraint-violating actions from consideration at each state. The proof combines this filter with two standard ingredients: value-function evaluation and greedy improvement from reinforcement learning, and PCTL model-checking procedures (the $\mathrm{Prob}_0$ and $\mathrm{Prob}_1$ sets) used to compute the satisfaction vector.

What would settle it

Construct a small MDP with an upstream state and a downstream state in which the utility-maximizing action at the upstream state changes the transition distribution into the downstream region, lowering the downstream satisfaction probability after a later update. Run Algorithm 1 with $\varepsilon=0$ from a feasible initial policy and model-check the returned policy against $P_{\ge\lambda}(\Phi U\Psi)$: if the final policy violates the formula, the step that claims feasibility is preserved by construction has failed.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is a policy-improvement step with a feasibility filter. At iteration $t+1$, the algorithm computes the satisfaction vector $x_s$ for the current policy $\pi_t$, then for every state and action forms $Y^{(t+1)}(s,a)=\sum_{s'} T(s,a,s')\, x_{s'}$, the probability that the PCTL path formula will hold after taking action $a$. Only actions with $Y^{(t+1)}(s,a)\ge\lambda$ enter the candidate set $C^{(t+1)}(s)$, so every accepted update is claimed to preserve feasibility of the overall policy. With $\varepsilon=0$, the paper proves that the value function never decreases, that termination follows from the finiteness of deterministic policy space, and that the terminal policy satisfies Bellman optimality restricted to the feasible action sets, hence is a local maximizer of the constrained problem. The same filter is also applied to general PCTL formulas through the standard recursive state-labeling method of PCTL model checking.

Load-bearing premise

The proof assumes that checking each updated action against the previous policy's satisfaction probabilities is enough to keep the whole policy feasible, even though later updates at other states can change those same satisfaction probabilities and push the true satisfaction probability below the threshold.

Editorial extensions

If this is right

  • With $\varepsilon=0$, Algorithm 1 terminates after finitely many updates and returns a policy satisfying the Bellman optimality condition restricted to the feasible action sets, i.e., a local maximizer of the constrained utility.
  • Every intermediate policy is claimed to be feasible for $P_{\ge\lambda}(\Phi U\Psi)$, so an agent trained this way never acts outside its normative constraint during learning.
  • For reachability formulas $P_{\ge\lambda}(FB)$ and constrained reachability formulas $P_{\ge\lambda}(\Phi U\Psi)$, no product automaton and no reward encoding of the norm is needed; the constraint enters only through the per-state filter.
  • With $\varepsilon>0$ the algorithm escaped local optima in the reported experiments, and in the infinite-iteration limit it would visit a global maximizer with probability 1, though the paper notes this limit is practically brute force.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural testable extension is to re-evaluate the full satisfaction vector after each epoch instead of only per-action estimates; this would make the feasibility-preservation claim directly checkable when later updates change downstream satisfaction probabilities.
  • The same filtering scheme could be applied to other probability-thresholded properties such as bounded until or probabilistic safety, because the method already relies on the recursive PCTL state-labeling construction; whether the convergence proof extends to those classes is open.
  • The reported sensitivity to $\varepsilon$ suggests a fixed exploration rate is a bottleneck; an annealed schedule that explores only while the policy is still changing would be a concrete alternative to benchmark.
  • Before deployment, a practitioner could verify the final policy with an independent PCTL model checker, since local optimality is proven with respect to the algorithm's own feasibility filter rather than the true satisfaction probability of the final policy.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper proposes Algorithm 1, a policy-improvement procedure for MDPs that must satisfy a PCTL constraint P≥λ(ΦUΨ), motivated by Expected Act Utilitarianism from stit logic. It claims (Theorem 4.2) that with ε=0 the algorithm converges to a feasible policy that is a local maximizer of the constrained utility maximization problem (2). The proof rests on four points: feasibility is preserved by a per-action reachability test in Step 5; value is non-decreasing; deterministic policy space is finite; and termination yields a Bellman-optimal policy within the feasible set. The paper also reports experiments on two small MDPs comparing the algorithm with brute-force global optima and studying ε-greedy exploration.

Significance. The problem—maximizing a scalar mission reward under a probabilistic temporal-logic constraint—is timely and the proposed local-search formulation is appealing. If Theorem 4.2 were correct, the algorithm would be a simple bridge between PCTL model checking and policy improvement, with no fitted parameters beyond the exploration rate. However, the central theorem is false: the feasibility test in Step 5 uses stale satisfaction probabilities and does not guarantee that the final policy satisfies the constraint. A concrete two-state counterexample yields an infeasible terminal policy. The claimed contribution therefore does not hold as stated.

major comments (3)
  1. [Theorem 4.2, proof item (1); Algorithm 1 Steps 4–7] The proof of Theorem 4.2 claims feasibility is preserved because Step 5 admits only actions with Y^{(t+1)}(s,a) ≥ λ. This test uses the satisfaction vector x^{(t)} of the policy at the time of the test. When downstream states are updated later, their satisfaction probabilities change, so an action that passed the test can become violating. Concretely, take λ=0.5 and target T, with state A having actions a1 (to T with probability 0.9) and a2 (to T with probability 0.5), and state S having actions b1 (to A with probability 1) and b2 (to A with probability 0.8, to losing sink with probability 0.2). Starting from π0={S:b1, A:a1}, x_A=0.9. If b2 is processed first and passes because 0.8·0.9=0.72≥0.5, and then a2 passes because 0.5≥0.5, the final policy has x_S=0.8·0.5=0.4<0.5. In the next sweep, b2 is invalid but b1 has lower utility, so the algorithm terminates with an infeasible policy. Hence Theorem 4.2's feasibility claim is false, and the algorithm does not solve (2).
  2. [Algorithm 1, Step 3] Step 3 defines x^{(t+1)}_s using x^{(t)}_{s'} on the right-hand side, which is a single Jacobi-like update rather than the solution of the reachability linear system described in the text. The vector x used in Step 4 is therefore not in general the actual satisfaction probability vector of the current policy, so the test Y^{(t+1)}(s,a) ≥ λ does not measure the candidate action's effect on the PCTL formula. This makes the feasibility guarantee in Theorem 4.2 even less supported: even within a single sweep, decisions are made on a stale or approximate x.
  3. [Section 4.1 and Algorithm 1 initialization] The algorithm box says 'Set an initial feasible policy π0 arbitrarily', while Section 4.1 states that a feasible policy is first found by computing Pmax(φ). These are inconsistent. If π0 is arbitrary, it need not be feasible, and the proof's first sentence ('the initial policy π0 is feasible by construction') has no basis. If π0 is found by Pmax, the paper does not specify how the corresponding policy is obtained or whether it can be constructed for the general ΦUΨ fragment. The theorem therefore lacks a precise, correct initialization.
minor comments (4)
  1. [Section 2, Section 4.1, Section 3.2] There are several typos: 'Marov chain' should be 'Markov chain', 'unocnstrained' should be 'unconstrained', and 'endogeneous' should be 'endogenous'.
  2. [Algorithm 1, Step 4] The notation Y^{(t+1)}(s,a) uses x_{s'} without a superscript; the authors should specify whether x is x^{(t)} or x^{(t+1)}, since the distinction is critical for the correctness of the algorithm.
  3. [After Theorem 4.2] The claim that 'If ε>0 then with probability 1, in the infinite iterations limit, the algorithm eventually visits a globally maximizing policy' is stated without proof. Since the paper explicitly calls this asymptotic result impractical, it should be either proved or removed.
  4. [Section 3.2] The passage discussing the circularity between 'best' and 'maximal utility' is a significant conceptual caveat; it should be explicitly linked to the algorithm's guarantees or clearly declared out of scope for this paper.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the policy-improvement derivation is self-contained and does not reduce to its inputs; the only self-citations are background and non-load-bearing.

full rationale

The paper's central claim (Theorem 4.2) is derived from the algorithm's update rule, the finite size of the policy space, and the Bellman optimality condition restricted to the set of valid actions; it does not derive its conclusion from the EAU/stit formalism. The stit material in Section 3 is explicitly non-load-bearing: 'The main theorem and its proof do not make use of the purely stit machinery.' The implicit deontic reward R_d is introduced only to explain the bi-level interpretation and is explicitly not used: 'This bi-level structure to the problem remains implicit in our approach since we do not actually have R_d.' No fitted parameter is renamed as a prediction: lambda is an input, the algorithm is evaluated against brute-force ground truth, and the experiments report local versus global optima rather than claiming a forced prediction. The self-citations to [25,26] provide background translation results and are not used in the proof of Theorem 4.2; the paper even flags the 'best -> maximal utility -> best' loop as a conceptual issue rather than importing it as support. The weakness identified by the reader in Step 5 of Algorithm 1 and in proof item (1) of Theorem 4.2 is a correctness/unsoundness concern, not circularity: the per-action test Y^{(t+1)}(s,a) >= lambda uses the previous policy's satisfaction vector, so global feasibility is not guaranteed to be preserved, but this is a failure of the stated invariant, not a reduction of the theorem to its own assumptions by construction. For these reasons, no circular step is exhibited, and the honest finding is no significant circularity.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

The central algorithm relies on standard MDP and PCTL machinery. The exploration rate epsilon is the only empirical free parameter. No new entities or fitted constants are introduced; the 'implicit reward' R_d is explicitly not used.

free parameters (1)
  • epsilon_exploration = 0.1-0.4 for experiments
    The exploration rate in Algorithm 1 is swept empirically in Section 5. For epsilon=0 the theorem holds, but the empirical success depends on this value.
assumptions (4)
  • standard math PCTL semantics and model checking algorithms are standard and correct.
    Used in Step 2 and Step 3 of Algorithm 1 to compute satisfaction probabilities.
  • domain assumption An initial feasible policy π0 exists and is provided.
    Algorithm 1 initializes with π0; if none exists the problem is infeasible.
  • standard math Reachability probabilities can be computed by solving a system of linear equations (or iterative approximation).
    Needed in Step 3 of Algorithm 1.
  • standard math The Bellman optimality condition restricted to the feasible action set defines a local optimum.
    Invoked in the proof of Theorem 4.2 item (4).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Deontically Constrained Policy Improvement in Reinforcement Learning Agents." pith.science (2026). https://pith.science/paper/P3CUP4WA

@misc{pith2026250606959,
  author       = {Pith},
  title        = {Pith review of: Deontically Constrained Policy Improvement in Reinforcement Learning Agents},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/P3CUP4WA}},
  note         = {Machine review of arXiv:2506.06959}
}
read the original abstract

Markov Decision Processes (MDPs) are the most common model for decision making under uncertainty in the Machine Learning community. An MDP captures non-determinism, probabilistic uncertainty, and an explicit model of action. A Reinforcement Learning (RL) agent learns to act in an MDP by maximizing a utility function. This paper considers the problem of learning a decision policy that maximizes utility subject to satisfying a constraint expressed in deontic logic. In this setup, the utility captures the agent's mission - such as going quickly from A to B. The deontic formula represents (ethical, social, situational) constraints on how the agent might achieve its mission by prohibiting classes of behaviors. We use the logic of Expected Act Utilitarianism, a probabilistic stit logic that can be interpreted over controlled MDPs. We develop a variation on policy improvement, and show that it reaches a constrained local maximum of the mission utility. Given that in stit logic, an agent's duty is derived from value maximization, this can be seen as a way of acting to simultaneously maximize two value functions, one of which is implicit, in a bi-level structure. We illustrate these results with experiments on sample MDPs.

Figures

Figures reproduced from arXiv: 2506.06959 by the authors.

Figure 1
Figure 1. MDP, an induced MC, and corresponding stit model translations. Only part [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Empirical convergence of Algorithm 1 over 100 trials for each [PITH_FULL_IMAGE:figures/full_fig_p015_2.png] view at source ↗
Figure 3
Figure 3. MDP2 from [17], which models a robot navigating a grid environment with probabilistic movement due to obstacles. The initial state is s0. The actions are labeled east, west, south, north, and stuck. Atomic propositions are shown in green and between curly braces next to the labeled states, e.g., L(s1) = hazard. The rewards (not shown) are, in order of states, 1, 2, 3, 20, 0, 0. Applying ϵ-greedy exploration again al… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Convergence results over 100 trials with varying [PITH_FULL_IMAGE:figures/full_fig_p016_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

30 extracted references · 29 canonical work pages

  1. [1]

    Abarca, A. I. R. and J. M. Broersen, A deontic stit logic based on beliefs and expected utility, in: J. Y. Halpern and A. Perea, editors, Proceedings Eighteenth Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2021, Beijing, China, June 25-27, 2021, EPTCS335, 2021, pp. 281–294. URLhttps://doi.org/10.4204/EPTCS.335.27

    work page doi:10.4204/eptcs.335.27 2021

  2. [2]

    MacGlashan and M

    Abel, D., J. MacGlashan and M. L. Littman, Reinforcement learning as a framework for ethical decision making, in: AAAI Workshop: AI, Ethics, and Society, 2016. URLhttps://api.semanticscholar.org/CorpusID:14717578

    work page 2016

  3. [3]

    Achiam, J., D. Held, A. Tamar and P. Abbeel, Constrained policy optimization, ICML (2017)

    work page 2017

  4. [4]

    CONSTRAINED MARKOV DECISION PROCESSES,

    ALTMAN, E., editor, “CONSTRAINED MARKOV DECISION PROCESSES,” Taylor & Francis, 2004

    work page 2004

  5. [5]

    A Framework for Transforming Specifications in Reinforcement Learning,

    Alur, R., S. Bansal, O. Bastani and K. Jothimurugan, “A Framework for Transforming Specifications in Reinforcement Learning,” Springer Nature Switzerland, Cham, 2022 pp. 604–624. URLhttps://doi.org/10.1007/978-3-031-22337-2_29

    work page doi:10.1007/978-3-031-22337-2_29 2022

  6. [6]

    Principles of model checking,

    Baier, C. and J.-P. Katoen, “Principles of model checking,” MIT press, 2008

    work page 2008

  7. [7]

    467–477, eleventh European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU 2011)

    Broersen, J., Probabilistic stit logic and its decomposition, International Journal of Approximate Reasoning54(2013), pp. 467–477, eleventh European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU 2011). URLhttps://www.sciencedirect.com/science/article/pii/S0888613X1200148X

    work page 2013

  8. [8]

    Herzig and N

    Broersen, J., A. Herzig and N. Troquard, From coalition logic to stit, Electronic Notes in Theoretical Computer Science157(2006), pp. 23–35, proceedings of the Third International Workshop on Logic and Communication in Multi-Agent Systems (LCMAS 2005). URLhttps://www.sciencedirect.com/science/article/pii/S1571066106003197

    work page 2006

Show all 30 references
  1. [9]

    Herzig and N

    Broersen, J., A. Herzig and N. Troquard,A stit-extension of atl, in: M. Fisher, W. van der Hoek, B. Konev and A. Lisitsa, editors, Logics in Artificial Intelligence (2006), pp. 69–81

    2006

  2. [10]

    Christiano, P. F., J. Leike, T. B. Brown, M. Martic, S. Legg and D. Amodei, Deep reinforcement learning from human preferences, in: Proceedings of the 31st International Conference on Neural Information Processing Systems, NIPS’17 (2017), p. 4302–4310

    2017

  3. [11]

    Ellis, M

    Djeumou, F., C. Ellis, M. Cubuktepe, C. Lennon and U. Topcu, Task-guided irl in pomdps that scales, Artificial Intelligence317(2023), p. 103856. URLhttps://www.sciencedirect.com/science/article/pii/S0004370223000024

    2023

  4. [12]

    Agency and Deontic Logic,

    Horty, J., “Agency and Deontic Logic,” Cambridge University Press, 2001

    2001

  5. [13]

    Horty, J., Epistemic oughts in stit semantics, Ergo6(2019)

    2019

  6. [14]

    Horty, J. and E. Pacuit, Action types in stit semantics, The Review of Symbolic Logic 10(2017), pp. 617–637

    2017

  7. [15]

    Piterman and D

    Huth, M., N. Piterman and D. Wagner, p-automata: New foundations for discrete-time probabilistic verification, in: 2010 Seventh International Conference on the Quantitative Evaluation of Systems, 2010, pp. 161–170

    2010

  8. [16]

    Kasenberg, D. and M. Scheutz, Norm conflict resolution in stochastic domains, Proceedings of the AAAI Conference on Artificial Intelligence32(2018). URLhttps://ojs.aaai.org/index.php/AAAI/article/view/11295

    2018

  9. [17]

    Kwiatkowska, M. and D. Parker, Automated verification and strategy synthesis for probabilistic systems, in: Proceedings of the International Symposium on Automated Technology for Verification and Analysis (ATV A) (2013), pp. 5–22

    2013

  10. [18]

    Lahijanian, M., S. B. Andersson and C. Belta, Temporal logic motion planning and control with probabilistic satisfaction guarantees, IEEE Transactions on Robotics (2012)

    2012

  11. [19]

    Jansen and U

    Lindemann, L., N. Jansen and U. Topcu, Optimizing rewards while meeting omega-regular constraints, in: Proceedings of the 38th AAAI Conference on Artificial Intelligence, 2024. 18 Deontically Constrained Policy Improvement in Reinforcement Learning Agents

    2024

  12. [20]

    URLhttp://www.lsv.fr/ ~markey/Teaching/ESSLLI06/ESSLLI-proc.pdf

    Markey, N., Expressiveness of temporal logics (2006). URLhttp://www.lsv.fr/ ~markey/Teaching/ESSLLI06/ESSLLI-proc.pdf

    2006

  13. [21]

    Neary, C., Z. Xu, B. Wu and U. Topcu, Reward machines for cooperative multi-agent reinforcement learning, in: Proceedings of the 20th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS ’21 (2021), p. 934–942

    2021

  14. [22]

    Chan and S

    Ngo, R., L. Chan and S. Mindermann, The alignment problem from a deep learning perspective (2022), v4. URLhttps://arxiv.org/pdf/2209.00626.pdf

    2022 arXiv

  15. [23]

    Bhatia and J

    Pan, A., K. Bhatia and J. Steinhardt, The effects of reward misspecification: Mapping and mitigating misaligned models, in: International Conference on Learning Representations, 2022. URLhttps://openreview.net/forum?id=JYtwGwIL7ye

    2022

  16. [24]

    Reymond, P

    R¨ opke, W., M. Reymond, P. Mannion, D. M. Roijers, A. Nowe and R. R˘ adulescu,Divide and conquer: Provably unveiling the pareto front with multi-objective reinforcement learning, in: Seventeenth European Workshop on Reinforcement Learning, 2024. URLhttps://openreview.net/foru...

    2024

  17. [25]

    Shea-Blymyer, C. and H. Abbas, Generating deontic obligations from utility-maximizing systems, in: Proceedings of the 2022 AAAI/ACM Conference on AI, Ethics, and Society, 2022, pp. 653–663

    2022

  18. [26]

    Shea-Blymyer, C. and H. Abbas, Formal ethical obligations in reinforcement learning agents: Verification and policy updates, Proceedings of the AAAI/ACM Conference on AI, Ethics, and Society7(2024), pp. 1368–1378. URLhttps://ojs.aaai.org/index.php/AIES/article/view/31730

    2024

  19. [27]

    Skalse, J. and A. Abate, The reward hypothesis is false, NeurIPS (2022)

    2022

  20. [28]

    Reinforcement Learning: An Introduction,

    Sutton, R. S. and A. G. Barto, “Reinforcement Learning: An Introduction,” MIT Press, 2018, 2nd edition

    2018

  21. [29]

    van Berkel, K. and T. Lyon, A neutral temporal deontic stit logic, in: Logic, Rationality, and Interaction: 7th International Workshop, LORI 2019, Chongqing, China, October 18–21, 2019, Proceedings (2019), p. 340–354. URLhttps://doi.org/10.1007/978-3-662-60292-8_25

    2019 doi

  22. [30]

    Littman and M

    Yang, C., M. Littman and M. Carbin, Reinforcement learning with general LTL objectives is intractable, in: Combining Learning and Reasoning: Programming Languages, Formalisms, and Representations, 2022. Appendix A Computing Prob0 and Prob1 in Algorithm 1 AlgorithmProb0(Sat(Φ),...

    2022

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.