Wasserstein Auto-encoded MDPs: Formal Verification of Efficiently Distilled RL Policies with Many-sided Guarantees

• URL: http://arxiv.org/abs/2303.12558v2
• Date: Fri, 21 Apr 2023 13:54:19 GMT
• Title: Wasserstein Auto-encoded MDPs: Formal Verification of Efficiently Distilled RL Policies with Many-sided Guarantees
• Abstract summary: Variational Markov Decision Processes (VAE-MDPs) are discrete latent space models that provide a reliable framework for distilling verifiable controllers from any RL policy. We introduce the Wasserstein auto-encoded MDP (WAE-MDP), a latent space model that fixes those issues by minimizing a penalized form of the optimal transport between the behaviors of the agent executing the original policy and the distilled policy. Our experiments show that, besides distilling policies up to 10 times faster, the latent model quality is indeed better in general.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Although deep reinforcement learning (DRL) has many success stories, the large-scale deployment of policies learned through these advanced techniques in safety-critical scenarios is hindered by their lack of formal guarantees. Variational Markov Decision Processes (VAE-MDPs) are discrete latent space models that provide a reliable framework for distilling formally verifiable controllers from any RL policy. While the related guarantees address relevant practical aspects such as the satisfaction of performance and safety properties, the VAE approach suffers from several learning flaws (posterior collapse, slow learning speed, poor dynamics estimates), primarily due to the absence of abstraction and representation guarantees to support latent optimization. We introduce the Wasserstein auto-encoded MDP (WAE-MDP), a latent space model that fixes those issues by minimizing a penalized form of the optimal transport between the behaviors of the agent executing the original policy and the distilled policy, for which the formal guarantees apply. Our approach yields bisimulation guarantees while learning the distilled policy, allowing concrete optimization of the abstraction and representation model quality. Our experiments show that, besides distilling policies up to 10 times faster, the latent model quality is indeed better in general. Moreover, we present experiments from a simple time-to-failure verification algorithm on the latent space. The fact that our approach enables such simple verification techniques highlights its applicability.

Related papers

• Topological Feasibility Guarantees for Differentiable Predictive Control [0.8880611506199766]
  Differentiable predictive control (DPC) is a self-supervised learning approach for approximating explicit model predictive control (MPC) policies.<n> feasibility guarantees, a core requirement for safe control, are currently provided either probabilistically or via online safety filters.<n>This paper establishes deterministic feasibility guarantees for DPC using a novel topological analysis of the induced reachable safe set.
  arXiv  Detail & Related papers  (2026-08-11T00:27:50Z)
• SMC-ES: Automated synthesis of formally verified control policies [0.6117371161379209]
  We propose a simulation-based methodology to automatically synthesize policies with formal guarantees regarding performance, safety, and robustness specifications.<n>We demonstrate the feasibility of our approach by developing SMC-ES, an algorithm that integrates Evolutionary Strategies with Statistical Model Checking-based verification.<n>Results show that, at the price of a sustainable increase in computational cost, our algorithm provides formal guarantees regarding performance, safety, and robustness specifications.
  arXiv  Detail & Related papers  (2026-07-16T13:51:59Z)
• Safe Reinforcement Learning via Recovery-based Shielding with Gaussian Process Dynamics Models [57.006252510102506]
  Reinforcement learning (RL) is a powerful framework for optimal decision-making and control but often lacks provable guarantees for safety-critical applications.<n>We introduce a novel recovery-based shielding framework that enables safe RL with a provable safety lower bound for unknown and non-linear continuous dynamical systems.
  arXiv  Detail & Related papers  (2026-02-12T22:03:35Z)
• Stabilizing Policy Gradients for Sample-Efficient Reinforcement Learning in LLM Reasoning [77.92320830700797]
  Reinforcement Learning has played a central role in enabling reasoning capabilities of Large Language Models.<n>We propose a tractable computational framework that tracks and leverages curvature information during policy updates.<n>The algorithm, Curvature-Aware Policy Optimization (CAPO), identifies samples that contribute to unstable updates and masks them out.
  arXiv  Detail & Related papers  (2025-10-01T12:29:32Z)
• Rectified Robust Policy Optimization for Model-Uncertain Constrained Reinforcement Learning without Strong Duality [53.525547349715595]
  We propose a novel primal-only algorithm called Rectified Robust Policy Optimization (RRPO)<n>RRPO operates directly on the primal problem without relying on dual formulations.<n>We show convergence to an approximately optimal feasible policy with complexity matching the best-known lower bound.
  arXiv  Detail & Related papers  (2025-08-24T16:59:38Z)
• Efficient Solution and Learning of Robust Factored MDPs [57.2416302384766]
  Learning r-MDPs from interactions with an unknown environment enables the synthesis of robust policies with provable guarantees on performance.<n>We propose novel methods for solving and learning r-MDPs based on factored state representations.
  arXiv  Detail & Related papers  (2025-08-01T15:23:15Z)
• Representation-based Reward Modeling for Efficient Safety Alignment of Large Language Model [84.00480999255628]
  Reinforcement Learning algorithms for safety alignment of Large Language Models (LLMs) encounter the challenge of distribution shift. Current approaches typically address this issue through online sampling from the target policy. We propose a new framework that leverages the model's intrinsic safety judgment capability to extract reward signals.
  arXiv  Detail & Related papers  (2025-03-13T06:40:34Z)
• Certifiably Robust Policies for Uncertain Parametric Environments [57.2416302384766]
  We propose a framework based on parametric Markov decision processes (MDPs) with unknown distributions over parameters. We learn and analyse IMDPs for a set of unknown sample environments induced by parameters. We show that our approach produces tight bounds on a policy's performance with high confidence.
  arXiv  Detail & Related papers  (2024-08-06T10:48:15Z)
• Safe Policy Improvement in Constrained Markov Decision Processes [10.518340300810504]
  We present a solution to the synthesis problem by solving its two main challenges: reward-shaping from a set of formal requirements and safe policy update. For the former, we propose an automatic reward-shaping procedure, defining a scalar reward signal compliant with the task specification. For the latter, we introduce an algorithm ensuring that the policy is improved in a safe fashion with high-confidence guarantees.
  arXiv  Detail & Related papers  (2022-10-20T13:29:32Z)
• Log Barriers for Safe Black-box Optimization with Application to Safe Reinforcement Learning [72.97229770329214]
  We introduce a general approach for seeking high dimensional non-linear optimization problems in which maintaining safety during learning is crucial. Our approach called LBSGD is based on applying a logarithmic barrier approximation with a carefully chosen step size. We demonstrate the effectiveness of our approach on minimizing violation in policy tasks in safe reinforcement learning.
  arXiv  Detail & Related papers  (2022-07-21T11:14:47Z)
• Safe Reinforcement Learning via Confidence-Based Filters [78.39359694273575]
  We develop a control-theoretic approach for certifying state safety constraints for nominal policies learned via standard reinforcement learning techniques. We provide formal safety guarantees, and empirically demonstrate the effectiveness of our approach.
  arXiv  Detail & Related papers  (2022-07-04T11:43:23Z)
• Supported Policy Optimization for Offline Reinforcement Learning [74.1011309005488]
  Policy constraint methods to offline reinforcement learning (RL) typically utilize parameterization or regularization. Regularization methods reduce the divergence between the learned policy and the behavior policy. This paper presents Supported Policy OpTimization (SPOT), which is directly derived from the theoretical formalization of the density-based support constraint.
  arXiv  Detail & Related papers  (2022-02-13T07:38:36Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)
• Distillation of RL Policies with Formal Guarantees via Variational Abstraction of Markov Decision Processes (Technical Report) [0.0]
  We consider the challenge of policy simplification and verification in the context of policies learned through reinforcement learning (RL) We derive new bisimulation bounds between the unknown environment and a learned discrete latent model of it. We show how one can use a policy obtained via state-of-the-art RL to efficiently train a variational autoencoder that yields a discrete latent model with provably approximately correct bisimulation guarantees.
  arXiv  Detail & Related papers  (2021-12-17T17:57:32Z)
• Pessimistic Model Selection for Offline Deep Reinforcement Learning [56.282483586473816]
  Deep Reinforcement Learning (DRL) has demonstrated great potentials in solving sequential decision making problems in many applications. One main barrier is the over-fitting issue that leads to poor generalizability of the policy learned by DRL. We propose a pessimistic model selection (PMS) approach for offline DRL with a theoretical guarantee.
  arXiv  Detail & Related papers  (2021-11-29T06:29:49Z)
• Lyapunov-based uncertainty-aware safe reinforcement learning [0.0]
  InReinforcement learning (RL) has shown a promising performance in learning optimal policies for a variety of sequential decision-making tasks. In many real-world RL problems, besides optimizing the main objectives, the agent is expected to satisfy a certain level of safety. We propose a Lyapunov-based uncertainty-aware safe RL model to address these limitations.
  arXiv  Detail & Related papers  (2021-07-29T13:08:15Z)
• An Abstraction-based Method to Verify Multi-Agent Deep Reinforcement-Learning Behaviours [8.95294551927446]
  Multi-agent reinforcement learning (RL) often struggles to ensure the safe behaviours of the learning agents. We present a methodology that combines formal verification with (deep) RL algorithms to guarantee the satisfaction of formally-specified safety constraints.
  arXiv  Detail & Related papers  (2021-02-02T11:12:30Z)
• Robust Constrained-MDPs: Soft-Constrained Robust Policy Optimization under Model Uncertainty [9.246374019271935]
  We propose to merge the theory of constrained Markov decision process (CMDP) with the theory of robust Markov decision process (RMDP) This formulation allows us to design RL algorithms that are robust in performance, and provides constraint satisfaction guarantees. We first propose the general problem formulation under the concept of RCMDP, and then propose a Lagrangian formulation of the optimal problem, leading to a robust-constrained policy gradient RL algorithm.
  arXiv  Detail & Related papers  (2020-10-10T01:53:37Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.