局部策略迭代的程序分析

基于策略迭代算法的逆方法

An Inverse Method for Policy-Iteration Based Algorithms

我们提出了一个扩展的两个策略迭代算法的加权图（即，马尔可夫决策问题和最大加代数）。这种扩展允许我们解决以下逆问题：考虑图的权重是未知的常数或参数，我们假设这些权重的参考实例，我们的目标是计算参数的约束，在该约束下，参考实例的最优策略仍然是最优的。因此，保证原始算法在引用实例化周围表现良好，这为我们提供了一些鲁棒性标准。我们将这两种方法应用于简单的示例。原型实现已经完成。

CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq

Reinforcement learning algorithms solve sequential decision-making problems in probabilistic environments by optimizing for long-term reward. The desire to use reinforcement learning in safety-critical settings inspires a recent line of work on formally constrained reinforcement learning; however, these methods place the implementation of the learning algorithm in their Trusted Computing Base. The crucial correctness property of these implementations is a guarantee that the learning algorithm converges to an optimal policy. This paper begins the work of closing this gap by developing a Coq for…

经过形式化验证的近似策略迭代

Formally Verified Approximate Policy Iteration

本文用 Isabelle/HOL 形式化验证因子 MDP 上的近似策略迭代算法，并将其精化为可执行实现，同时开发线性规划解认证软件以验证其实用性。

滚动抽样近似策略迭代的算法和界

Algorithms and Bounds for Rollout Sampling Approximate Policy Iteration

近年来，一些不带值函数的近似策略迭代方案被提出来，这些方案侧重于使用分类器的策略表示，并将策略学习作为一个监督学习问题来解决。使用这种方法找到好的策略不仅需要适当的分类器，还需要可靠的最佳动作示例，充分覆盖状态空间。到目前为止，很少有工作已经做了适当的覆盖计划和方法，以减少样本的复杂性，这种方法，特别是在连续状态空间。本文重点介绍了最简单的覆盖方案（状态空间上的离散网格），并在最简单的（以前常用的）卷展采样分配策略（在考虑中的每个状态下均匀分配样本）和几乎同样简单的方法（仅根据需要分配样本，需要的样本数量明显较少）之间进行了样本复杂性比较。

静态分析中耦合策略迭代与半定松弛计算精确数值不变量

Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis

我们引入了一个新的域，通过抽象解释来寻找程序的精确数值不变量。该域由非线性函数的水平集组成，推广了Manna，Sankaranarayanan和Sipma引入的线性“模板”域。在二次模板的情况下，我们使用Shor的半定松弛推导出可计算的但精确的抽象的语义泛函，我们表明，抽象的不动点方程可以精确地解决耦合策略迭代和半定规划。我们证明了我们的方法的一系列例子（过滤器，集成计划），包括一个退化的（辛计划）的兴趣。

策略迭代的平方和扩展

A Sums-of-Squares Extension of Policy Iterations

为了解决静态分析中加宽算子带来的不精确性，基于最小计算的策略迭代将程序可达值集的特征化看作是从一个后定点开始的策略迭代计算.计算每个策略和相关的不变量依赖于一系列数值优化。虽然早期的研究工作依赖于线性规划（LP）来解决线性规划的线性特性，但目前的技术水平仍然限于分析最多具有二次不变量的线性规划，依赖于半定规划（SDP）求解器来计算策略，以及LP求解器来细化不变量。我们建议在这里扩展类的程序考虑通过使用平方和（SOS）为基础的优化。我们的方法使切换系统的多项式更新和警卫的精确分析。所提出的分析已在Matlab中实现，并应用于现有的程序来自系统控制文献，提高了可分析系统的范围和以前处理的精度。