Pith. sign in

REVIEW 2 major objections 5 minor 52 references

Data-Efficient Safe Policy Improvement Using Parametric Structure

T0 review · 2 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Pith's one-line read Safe offline reinforcement learning can reuse samples from transitions that share the same probability law, cutting the data required by orders of magnitude while preserving the same safety guarantee.

desk verdict The pSPIBB idea and experiments are solid, but the pruning contribution's headline data-efficiency claim rests on an unproven interaction with the behavior policy. read the letter →

arxiv 2507.15532 v2 pith:KKGH2MXA submitted 2025-07-21 cs.AI

classification cs.AI
keywords safepolicyimprovementofflinereinforcementlearningparametricMarkovdecisionprocessesSPIBBdataefficiencygame-basedabstractionSMTsolvingparametertying
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

Safe policy improvement asks for a policy that, with high confidence, is at least as good as a known behavior policy, using only a fixed dataset and no new interaction with the environment. This paper's central claim is that when the environment is given as a parametric MDP — a Markov decision process whose transitions are labelled by shared polynomials over unknown parameters — samples from state-action pairs with identical labels can be pooled, multiplying the effective amount of data without weakening the safety guarantee. To go further, the paper adds two preprocessing methods that delete provably suboptimal actions before learning: one using cooperative and antagonistic game bounds that need no data, and one using exact satisfiability-modulo-theory reasoning over the parametric value functions. Experiments on five benchmarks suggest that pooling and game-based pruning reduce the number of trajectories required by more than two orders of magnitude on several environments, while the exact SMT method remains too slow on current solvers.

What carries the argument

The load-bearing device is the equivalence relation over transitions induced by polynomial labels. For a pMDP, $[s,a]_P$ collects every state-action pair whose successor transitions carry exactly the same set of polynomials, and $[s,a,s']_P$ refines this by matching individual successor labels; pooling counts over these classes is parameter tying, and it replaces the MLE and the uncertainty set by their pooled versions (Equations 6 and 7). A second mechanism is the game view: the antagonistic value $aVal$ is the worst reward an adversary can force and the cooperative value $cVal$ the best reward a cooperative nature can give, both independent of the concrete parameter valuation; comparing $aVal(s)$ with $cVal$-based or $Q$-based upper bounds on an action's value yields the pruning theorems. The third mechanism is an SMT encoding of the Bellman equations over the rational-function value functions, with existentially quantified real parameters, used to decide whether an action can ever be optimal.

What would settle it

Construct a pMDP with two state-action pairs that share a polynomial label but are instantiated with different true probabilities, generate datasets at the threshold size, run pSPIBB, and count how often the returned policy violates $V^{\pi_I}(\iota) \ge V^{\pi_B}(\iota) - \zeta$; if the violation rate exceeds $\delta$, the pooling step is biased and the guarantee collapses.

Watch

Extended reading notes

Core claim

The paper claims that the parametric structure of a pMDP is, in effect, free data. State-action pairs whose transition polynomials coincide are independent draws of the same unknown probability distribution, so pSPIBB merges their samples in the maximum-likelihood estimate (its Equation 6) and applies the SPIBB uncertainty threshold to the merged counts (its Equation 7). Since this only lumps identical experiments, the original SPIBB correctness proof transfers unchanged, and the paper states that pSPIBB is guaranteed to perform equally well or better than standard SPIBB under the same improvement guarantee. The pruning theorems give valuation-independent conditions — an action is dominated when its cooperative or actual Q-value is below the antagonistic value of its state — under which an optimal policy never selects that action, so removing it is harmless for every parameter setting. The reported consequence is that these mechanisms reduce the data needed to reach a given performance level by more than two orders of magnitude on several benchmarks, with pSPIBB combined with game-based pruning giving the largest gain.

Load-bearing premise

The parametric MDP must be faithful: if two transitions carry the same symbolic label but their true probabilities differ under the actual parameter setting, pooling their samples biases the estimate and the improvement guarantee can fail.

Editorial extensions

If this is right

  • pSPIBB attains the same $(\zeta,\delta)$ guarantee as standard SPIBB while needing more than two orders of magnitude fewer trajectories on Gridworld and Rock-Paper-Scissors at $N^\wedge = 200$.
  • Game-based pruning removes actions without any dataset at all, because the antagonistic and cooperative bounds hold for every graph-preserving valuation; in Taxi it improves SPIBB's data efficiency by two orders of magnitude.
  • Combined, pSPIBB and game-based pruning deliver the largest data-efficiency gain of all tested configurations.
  • SMT-based pruning is exact and can in principle remove more actions than game-based abstraction, but on a single Gridworld query one SMT solver needed six hours and another exceeded a twelve-hour timeout, so it is not practically usable at present.
  • Bad-seed performance, measured by the 10% and 1% conditional value at risk, can dip below the behavior policy, but all observed dips stay within the allowed loss $\zeta$, and raising the threshold $N^\wedge$ suppresses them without erasing the data-efficiency gains.

Reading between the lines

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

  • The pooling idea is not tied to polynomial labels: any known equivalence structure over transition distributions — factored MDPs, symmetries, or graph connectivity — could be used to define the classes in Equation (6) and multiply effective sample sizes.
  • Because game-based pruning is data-independent, the same pruned pMDP can be reused across many datasets, behavior policies, or SPI algorithms; the paper does not explore these downstream reuses.
  • The SMT infeasibility result points to a tractable middle path: replacing exact polynomial reasoning with interval or robust-MDP over-approximations could prune more actions than game bounds at a fraction of the computational cost (the paper lists this as future work).
  • pSPIBB concentrates estimation error: a single bad maximum-likelihood draw worsens many pooled state-action pairs at once, so practitioners should watch tail risk and prefer larger thresholds than the bare guarantee requires; the paper's CVaR curves illustrate this trade-off.
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

2 major / 5 minor

Summary. This paper addresses data efficiency in safe policy improvement (SPI) by exploiting parametric structure in Markov decision processes (pMDPs). It proposes three contributions: parametric SPIBB (pSPIBB), which pools samples across state-action pairs with identical transition polynomials to form a maximum-likelihood MDP and a reduced uncertainty set; game-based pruning, which uses support-only antagonistic and cooperative value bounds to remove state-action pairs that no optimal policy can choose; and SMT-based pruning, an exact but computationally expensive variant. The authors prove several value-bound theorems (Lemma 1, Theorems 1-4), report an ablation study on five benchmarks with 1024 seeds and CVaR metrics, and find data-efficiency gains up to two orders of magnitude. SMT-based pruning is found to be practically infeasible on the tested instance.

Significance. The core ideas are attractive: parameter tying is a natural way to multiply effective sample sizes in offline RL, and the support-only bounds used for pruning are valuation-independent and dataset-independent. The empirical methodology is a strength: 1024 seeds, explicit CVaR tails, an ablation separating the contributions, and released code. If the two theoretical gaps identified below are closed, the paper would constitute a solid and useful contribution to safe offline RL. As it stands, the advertised reliability guarantees for the pSPIBB and pruned-SPIBB pipelines are not yet established.

major comments (2)
  1. [Section 3, Eqs. (6)-(7)] The paragraph after Eq. (7) asserts that "this modification does not change the underlying correctness proof of SPIBB as we are simply merging two identical Bernoulli experiments into one," and concludes that pSPIBB "is guaranteed to perform equally well or better compared to standard SPIBB while achieving the same improvement guarantee." This is the central theoretical claim of Contribution 1, but no theorem or proof is provided. The SPIBB guarantee in Section 2.1 is built on per-state-action concentration bounds (Eq. (5) and the N∧ formula); replacing the MLE-MDP and the uncertainty set with the pooled versions in Eqs. (6)-(7) requires a new proof that the same N∧ still yields Eq. (3) for the pSPIBB policy. Moreover, U_pSPIBB ⊆ U_SPIBB does not imply that the resulting policy has value at least that of standard SPIBB, because the MLE-MDP itself changes; the CVaR curves in Section 6.2.1 (e.g., Figures 5a and 5e) actually show pSPIBB with worse 1%-CVaR than SPIBB in several environments. The sentence as written is therefore either false or needs a precise probabilistic reformulation and proof.
  2. [Section 4 and Figure 1] The paper presents game-based pruning as a preprocessing step that feeds the pruned pMDP, the original dataset, and the original behavior policy into existing SPI(BB) methods, and claims the same reliability guarantees are maintained. However, no algorithm is given for running SPIBB on a pruned MDP when the behavior policy puts positive mass on a pruned action. The SPIBB update in Section 2.1 assigns πB(a|s) to every ⟨s,a⟩ in U and sums πB(a'|s) over the non-bootstrapped actions Ā(s); if an action is pruned, these expressions are undefined unless πB is renormalized or otherwise modified. Any such modification changes the baseline policy, so the guarantee in Eq. (3) relative to the original πB is lost. Theorem 2 only establishes that a pruned action is never chosen by an optimal policy of the true MDP; it does not show that the value of the behavior policy is preserved, nor that the SPIBB policy computed on the pruned MDP satisfies VπI ≥ VπB − ζ. The authors need to specify the exact algorithm and prove a transfer theorem for the pruned pipeline.
minor comments (5)
  1. [Section 3, Eq. (7)] Equation (7) uses the symbol [s,a]_L, which is not defined; Section 3 defines [s,a]_P. This should be fixed.
  2. [Section 6.2.1] The text states that pSPIBB and pruning improve data efficiency by "two orders of magnitude" but does not define the data-efficiency metric; it would be clearer to report the number of trajectories needed to reach a fixed performance target for each method.
  3. [Section 6.1] The conclusion that SMT-based pruning is "practically infeasible" rests on a single Gridworld instance; a small set of instances would make the negative claim more robust, or the claim should be qualified accordingly.
  4. [Sections 3-5] The paper should explicitly state that the guarantees are conditional on the parametric model being faithful: if two state-action pairs share a polynomial label but their true transition probabilities differ, the pooled estimator in Eq. (6) is biased and the improvement guarantee may fail.
  5. [Section 6.2.1] The assertion that "all curves are well within the range of the behavior policy's performance ±ζ" is imprecise because Eq. (3) is a probabilistic guarantee; reporting the fraction of seeds violating the bound across the 1024 seeds would be more informative.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the parametric estimator, pruning theorems, and empirical evaluations are each derived or measured independently of the claims they support.

full rationale

The paper's central claims are not circular. pSPIBB's pooled MLE (Eq. 6) and uncertainty set (Eq. 7) are constructed directly from syntactic polynomial-label equivalence classes; the improvement guarantee is inherited from the external SPIBB correctness argument [25] (with tighter ζ bounds from [47]), not from the paper's own definitions. The game-based pruning results (Lemma 1, Theorems 1-2) are proved from the Bellman equations and the definitions of aVal/cVal, and the SMT-based counterparts (Theorems 3-4) are proved in the appendix from the same first principles; no theorem has as its conclusion the assumption that defines it. The empirical data-efficiency improvements are measured comparisons against fixed SPIBB baselines, not fitted quantities relabeled as predictions. Some self-citations exist ([7], [12], [47]), but they supply standard support-only reachability facts, game-abstraction context, and known ζ bounds, none of which is load-bearing for the paper's new derivation chain. The main risks in the paper are correctness and model-misspecification concerns (e.g., how the behavior policy is renormalized after pruning, and the faithfulness of the parametric model), not circularity.

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

The method relies on the given pMDP structure and standard statistical assumptions; no new entities are introduced, and the method adds no fitted parameters beyond the problem's free parameters.

assumptions (4)
  • domain assumption The environment is faithfully modeled as a pMDP: all state-action pairs with identical polynomial label sets share the same true transition probabilities under the unknown valuation.
    The pSPIBB MLE (Equation 6) pools samples across these pairs; if the labels are shared incorrectly, the estimator is biased and the guarantee breaks.
  • domain assumption Graph-preserving valuations only (Definition 2): all valuations share the same support and satisfy probability axioms.
    Theorems 1 and 2 and the pruning conditions rely on support being fixed and independent of parameter values.
  • ad hoc to paper No state-action distribution labels two different successors with the same polynomial (Section 3, stated without loss of generality).
    This simplifies the equivalence class definition; the proposed reduction to fresh intermediate states is not fully elaborated.
  • domain assumption The SPIBB correctness proof extends to pooled sample counts without modification (Section 3, 'this modification does not change the underlying correctness proof').
    This is asserted rather than proven; it is load-bearing for the pSPIBB guarantee.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Data-Efficient Safe Policy Improvement Using Parametric Structure." pith.science (2026). https://pith.science/paper/KKGH2MXA

@misc{pith2026250715532,
  author       = {Pith},
  title        = {Pith review of: Data-Efficient Safe Policy Improvement Using Parametric Structure},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/KKGH2MXA}},
  note         = {Machine review of arXiv:2507.15532}
}
read the original abstract

Safe policy improvement (SPI) is an offline reinforcement learning problem in which a new policy that reliably outperforms the behavior policy with high confidence needs to be computed using only a dataset and the behavior policy. Markov decision processes (MDPs) are the standard formalism for modeling environments in SPI. In many applications, additional information in the form of parametric dependencies between distributions in the transition dynamics is available. We make SPI more data-efficient by leveraging these dependencies through three contributions: (1) a parametric SPI algorithm that exploits known correlations between distributions to more accurately estimate the transition dynamics using the same amount of data; (2) a preprocessing technique that prunes redundant actions from the environment through a game-based abstraction; and (3) a more advanced preprocessing technique, based on satisfiability modulo theory (SMT) solving, that can identify more actions to prune. Empirical results and an ablation study show that our techniques increase the data efficiency of SPI by multiple orders of magnitude while maintaining the same reliability guarantees.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

52 extracted references · 48 canonical work pages

  1. [1]

    Alshiekh, R

    M. Alshiekh, R. Bloem, R. Ehlers, B. Könighofer, S. Niekum, and U. Topcu. Safe reinforcement learning via shielding. In AAAI, pages 2669–2678. AAAI Press, 2018

  2. [2]

    Baier and J

    C. Baier and J. Katoen. Principles of model checking. MIT Press, 2008

  3. [3]

    Baier, C

    C. Baier, C. Hensel, L. Hutschenreiter, S. Junges, J. Katoen, and J. Klein. Parametric Markov chains: PCTL complexity and fraction- free gaussian elimination. Inf. Comput., 272:104504, 2020

  4. [4]

    Barbosa, C

    H. Barbosa, C. W. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, A. Ozdemir, M. Preiner, A. Reynolds, Y . Sheng, C. Tinelli, and Y . Zohar. cvc5: A versatile and industrial-strength SMT solver. In TACAS (1), volume 13243 of LNCS, pages 415–442. Springer, 2022

  5. [5]

    C. W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability modulo theories. In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability - Second Edition , volume 336 of Frontiers in Artificial Intelligence and Applications, pages 1267–1329. IOS Press, 2021

  6. [6]

    Barrett and S

    L. Barrett and S. Narayanan. Learning all optimal policies with mul- tiple criteria. In ICML, volume 307 of ACM International Conference Proceeding Series, pages 41–47. ACM, 2008

  7. [7]

    Bharadwaj, S

    S. Bharadwaj, S. L. Roux, G. A. Pérez, and U. Topcu. Reduction tech- niques for model checking and learning in mdps. In C. Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Ar- tificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 4273–4279. ijcai.org, 2017

  8. [8]

    Bianchi, E

    F. Bianchi, E. Zorzi, A. Castellini, T. D. Simão, M. T. J. Spaan, and A. Farinelli. Scalable safe policy improvement for factored multi-agent MDPs. In R. Salakhutdinov, Z. Kolter, K. Heller, A. Weller, N. Oliver, J. Scarlett, and F. Berkenkamp, editors, Proceedings of the 41st Inter- national Conference on Machine Learning, volume 235 of Proceedings of Ma...

Show all 52 references
  1. [9]

    Brockbank and E

    E. Brockbank and E. Vul. Repeated rock, paper, scissors play re- veals limits in adaptive sequential behavior.Cognitive Psychology, 151: 101654, 2024. ISSN 0010-0285

  2. [10]

    Castellini, F

    A. Castellini, F. Bianchi, E. Zorzi, T. D. Simão, A. Farinelli, and M. T. J. Spaan. Scalable safe policy improvement via monte carlo tree search. In ICML, volume 202 of Proceedings of Machine Learning Research , pages 3732–3756. PMLR, 2023

  3. [11]

    Chandak, S

    Y . Chandak, S. M. Jordan, G. Theocharous, M. White, and P. S. Thomas. Towards safe policy improvement for non-stationary mdps. InNeurIPS, 2020

  4. [12]

    Chatterjee, P

    K. Chatterjee, P. Novotný, G. A. Pérez, J. Raskin, and D. Zikelic. Op- timizing expectation with guarantees in POMDPs. In S. Singh and S. Markovitch, editors, Proceedings of the Thirty-First AAAI Confer- ence on Artificial Intelligence, February 4-9, 2017, San Francisco, Cal- ...

  5. [13]

    Chatterjee, A

    K. Chatterjee, A. Elgyütt, P. Novotný, and O. Rouillé. Expectation op- timization with probabilistic guarantees in POMDPs with discounted- sum objectives. In J. Lang, editor, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 201...

  6. [14]

    C. Daws. Symbolic and parametric model checking of discrete-time Markov chains. In Z. Liu and K. Araki, editors, Theoretical Aspects of Computing - ICTAC 2004, First International Colloquium, Guiyang, China, September 20-24, 2004, Revised Selected Papers , volume 3407 of LNCS,...

  7. [15]

    L. M. de Moura and N. S. Bjørner. Z3: an efficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008

  8. [16]

    T. G. Dietterich. Hierarchical reinforcement learning with the MAXQ value function decomposition. J. Artif. Intell. Res., 13:227–303, 2000

  9. [17]

    data-efficient safe policy improvement using parametric structure

    K. Engelen, G. Perez, and M. Suilen. Code for "data-efficient safe policy improvement using parametric structure", Aug. 2025. URL https://doi.org/10.5281/zenodo.16884207

  10. [18]

    García and F

    J. García and F. Fernández. A comprehensive survey on safe reinforce- ment learning. J. Mach. Learn. Res., 16:1437–1480, 2015

  11. [19]

    Gopalan and S

    A. Gopalan and S. Mannor. Thompson sampling for learning parameter- ized Markov decision processes. In COLT, volume 40 of JMLR Work- shop and Conference Proceedings, pages 861–898. JMLR.org, 2015

  12. [20]

    Jansen, B

    N. Jansen, B. Könighofer, S. Junges, A. Serban, and R. Bloem. Safe reinforcement learning using probabilistic shields (invited paper). In CONCUR, volume 171 of LIPIcs, pages 3:1–3:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020

  13. [21]

    Jansen, S

    N. Jansen, S. Junges, and J. Katoen. Parameter synthesis in Markov models: A gentle survey. In Principles of Systems Design , volume 13660 of LNCS, pages 407–437. Springer, 2022

  14. [22]

    Kober and J

    J. Kober and J. Peters. Reinforcement learning in robotics: A survey. In Reinforcement Learning, volume 12 of Adaptation, Learning, and Optimization, pages 579–610. Springer, 2012

  15. [23]

    Lange, T

    S. Lange, T. Gabel, and M. A. Riedmiller. Batch reinforcement learning. In Reinforcement Learning, volume 12 of Adaptation, Learning, and Optimization, pages 45–73. Springer, 2012

  16. [24]

    Lanotte, A

    R. Lanotte, A. Maggiolo-Schettini, and A. Troina. Parametric proba- bilistic transition systems for system design and analysis. Formal As- pects Comput., 19(1):93–109, 2007

  17. [25]

    Laroche, P

    R. Laroche, P. Trichelair, and R. T. des Combes. Safe policy improve- ment with baseline bootstrapping. In ICML, volume 97 of Proceedings of Machine Learning Research, pages 3652–3661. PMLR, 2019

  18. [26]

    Lauri, D

    M. Lauri, D. Hsu, and J. Pajarinen. Partially observable Markov de- cision processes in robotics: A survey. IEEE Trans. Robotics , 39(1): 21–40, 2023

  19. [27]

    Levine, A

    S. Levine, A. Kumar, G. Tucker, and J. Fu. Offline reinforcement learning: Tutorial, review, and perspectives on open problems. CoRR, abs/2005.01643, 2020

  20. [28]

    Meggendorfer, M

    T. Meggendorfer, M. Weininger, and P. Wienhöft. What are the odds? improving the foundations of statistical model checking. CoRR, abs/2404.05424, 2024

  21. [29]

    C. H. Papadimitriou. Games against nature. J. Comput. Syst. Sci. , 31 (2):288–301, 1985

  22. [30]

    Petrik, M

    M. Petrik, M. Ghavamzadeh, and Y . Chow. Safe policy improvement by minimizing robust baseline regret. In NIPS, pages 2298–2306, 2016

  23. [31]

    Polgreen, V

    E. Polgreen, V . B. Wijesuriya, S. Haesaert, and A. Abate. Data-efficient bayesian verification of parametric markov chains. In QEST, volume 9826 of LNCS, pages 35–51. Springer, 2016

  24. [32]

    Poupart, N

    P. Poupart, N. Vlassis, J. Hoey, and K. Regan. An analytic solution to discrete bayesian reinforcement learning. In ICML, volume 148 of ACM International Conference Proceeding Series , pages 697–704. ACM, 2006

  25. [33]

    M. L. Puterman. Markov Decision Processes: Discrete Stochastic Dy- namic Programming. Wiley Series in Probability and Statistics. Wiley, 1994

  26. [34]

    R. T. Rockafellar, S. Uryasev, et al. Optimization of conditional value- at-risk. Journal of risk, 2:21–42, 2000

  27. [35]

    Satija, P

    H. Satija, P. S. Thomas, J. Pineau, and R. Laroche. Multi-objective SPIBB: seldonian offline policy improvement with safety constraints in finite mdps. In NeurIPS, pages 2004–2017, 2021

  28. [36]

    Schaefer, J

    M. Schaefer, J. Cardinal, and T. Miltzow. The existential theory of the reals as a complexity class: A compendium. CoRR, abs/2407.18006, 2024

  29. [37]

    Schnitzer, A

    Y . Schnitzer, A. Abate, and D. Parker. Certifiably robust policies for uncertain parametric environments. In A. Gurfinkel and M. Heule, ed- itors, Tools and Algorithms for the Construction and Analysis of Sys- tems, pages 63–83, Cham, 2025. Springer Nature Switzerland. ISBN 9...

  30. [38]

    Scholl, F

    P. Scholl, F. Dietrich, C. Otte, and S. Udluft. Safe policy improve- ment approaches on discrete Markov decision processes. In ICAART (2), pages 142–151. SCITEPRESS, 2022

  31. [39]

    T. D. Simão and M. T. J. Spaan. Safe policy improvement with baseline bootstrapping in factored environments. In AAAI, pages 4967–4974. AAAI Press, 2019

  32. [40]

    T. D. Simão and M. T. J. Spaan. Structure learning for safe policy improvement. In IJCAI, pages 3453–3459. ijcai.org, 2019

  33. [41]

    T. D. Simão, M. Suilen, and N. Jansen. Safe policy improvement for POMDPs via finite-state controllers. In AAAI, pages 15109–15117. AAAI Press, 2023

  34. [42]

    Suilen, T

    M. Suilen, T. S. Badings, E. M. Bovy, D. Parker, and N. Jansen. Robust markov decision processes: A place where AI and formal methods meet. In Principles of Verification (3) , volume 15262 of LNCS, pages 126–

  35. [43]

    R. S. Sutton and A. G. Barto. Reinforcement learning - an introduction. Adaptive computation and machine learning. MIT Press, 1998

  36. [44]

    N. M. Temme. Asymptotic inversion of the incomplete beta function. Journal of computational and applied mathematics , 41(1-2):145–157, 1992

  37. [45]

    P. S. Thomas, G. Theocharous, and M. Ghavamzadeh. High confidence policy improvement. In ICML, volume 37 ofJMLR Workshop and Con- ference Proceedings, pages 2380–2388. JMLR.org, 2015

  38. [46]

    Towers, A

    M. Towers, A. Kwiatkowski, J. K. Terry, J. U. Balis, G. D. Cola, T. Deleu, M. Goulão, A. Kallinteris, M. Krimmel, A. KG, R. Perez- Vicente, A. Pierré, S. Schulhoff, J. J. Tai, H. Tan, and O. G. Younis. Gymnasium: A standard interface for reinforcement learning environ- ments. ...

  39. [47]

    Wienhöft, M

    P. Wienhöft, M. Suilen, T. D. Simão, C. Dubslaff, C. Baier, and N. Jansen. More for less: Safe policy improvement with stronger per- formance guarantees. In IJCAI, pages 4406–4415. ijcai.org, 2023

  40. [48]

    Wiesemann, D

    W. Wiesemann, D. Kuhn, and B. Rustem. Robust markov decision pro- cesses. Math. Oper. Res., 38(1):153–183, 2013

  41. [49]

    Q. Yang, T. D. Simão, S. H. Tindemans, and M. T. J. Spaan. WCSAC: worst-case soft actor critic for safety-constrained reinforcement learn- ing. In AAAI, pages 10639–10646. AAAI Press, 2021

  42. [50]

    ∞X t=0 γtR(st, at) # ≤ E[cV alπ(s)] = cV alπ(s). Finally, since π was arbitrary, then by definition of supremum, we obtain: sup π aV alπ(s) ≤ sup π E

    U. Zwick and M. Paterson. The complexity of mean payoff games on graphs. Theor. Comput. Sci., 158(1&2):343–359, 1996. A Proof of Lemma 1 Consider a pMDP ⟨S, ι, A, P, X, R, γ⟩. Let s ∈ S and θ ∈ Θgp be arbitrary. We will now prove that the following inequalities hold: aV al(s) ...

  43. [51]

    Remove all state-action pairs ⟨s, a⟩ for which we have aV al(s) > mins′∈supp(s,a) R(s, a) + γaV al(s′)

  44. [52]

    paper” and in the previous round the player chose “rock

    In the resulting pMDP, use Algorithm 45 for almost-sure reachability from [2]. Termination of the algorithm is trivial since Algorithm 45 also terminates. It remains for us to establish correctness. We proceed by establishing partial correctness and completeness. D.1 Partial c...

Pith tools

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