策略迭代的平方和扩展

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

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

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

局部策略迭代的程序分析

Program Analysis with Local Policy Iteration

我们提出了一种新的算法，用于推导数值不变量，结合了最大策略迭代的精度与传统Kleene迭代的灵活性和可扩展性。它在可配置程序分析（CPA）框架中定义，因此允许分析间通信。它使用可调块编码来遍历无循环的程序部分，可能包含分支，而不引入额外的抽象。我们的技术操作在任何模板线性约束域，包括区间和八角形域;模板也可以从程序源代码中导出。的实施进行了评估，从软件验证比赛（SV-Comp）的一组基准。它可以与最先进的分析仪竞争。

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

An Inverse Method for Policy-Iteration Based Algorithms

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

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

Formally Verified Approximate Policy Iteration

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

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

Algorithms and Bounds for Rollout Sampling Approximate Policy Iteration

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

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…