SMC-ES: Automated synthesis of formally verified control policies

• URL: http://arxiv.org/abs/2607.15003v1
• Date: Thu, 16 Jul 2026 13:51:59 GMT
• Title: SMC-ES: Automated synthesis of formally verified control policies
• Abstract summary: 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.
• Score: 0.6117371161379209
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The deployment of autonomous cyber-physical systems in safety-critical environments requires closed-loop control strategies (i.e., policies) that are not only performant but also provably safe and robust. While learning-based methodologies such as Reinforcement Learning offer flexible and scalable approaches to automatically synthesize such controllers, they typically lack the formal guarantees necessary for safe deployment. To bridge this gap, we propose a novel simulation-based methodology to automatically synthesize policies with formal guarantees regarding performance, safety, and robustness specifications. Specifically, given a set of properties to verify, a confidence parameter $δ$ and an allowable failure probability $\varepsilon$, our method guarantees that the synthesized policy comes with a certificate: with confidence at least $1 - δ$, the probability of encountering a scenario where the given properties are violated is at most $\varepsilon$. We demonstrate the feasibility of our approach by developing SMC-ES, an algorithm that integrates Evolutionary Strategies with Statistical Model Checking-based verification. We evaluate SMC-ES on a suite of continuous control tasks using Gymnasium and Safety Gymnasium testbeds. Results show that, at the price of a sustainable increase in computational cost, our algorithm provides formal guarantees regarding performance, safety, and robustness specifications, while performing competitively against leading model-free Deep Reinforcement Learning (DRL) and Safe-DRL baselines.

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)
• Safe Reinforcement Learning using Ideas from Model Predictive Control [0.40831821256838124]
  Reinforcement learning enables the synthesis of control policies directly from data.<n>A persistent challenge is ensuring strict, hard safety constraints during the active learning phase.<n>We propose a framework that combines the adaptive, high-performance nature of deep reinforcement learning with the formal safety guarantees of model predictive control.
  arXiv  Detail & Related papers  (2026-07-08T10:35:04Z)
• 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)
• Wasserstein Auto-encoded MDPs: Formal Verification of Efficiently Distilled RL Policies with Many-sided Guarantees [0.0]
  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.
  arXiv  Detail & Related papers  (2023-03-22T13:41:42Z)
• ISAACS: Iterative Soft Adversarial Actor-Critic for Safety [0.9217021281095907]
  This work introduces a novel approach enabling scalable synthesis of robust safety-preserving controllers for robotic systems. A safety-seeking fallback policy is co-trained with an adversarial "disturbance" agent that aims to invoke the worst-case realization of model error. While the learned control policy does not intrinsically guarantee safety, it is used to construct a real-time safety filter.
  arXiv  Detail & Related papers  (2022-12-06T18:53:34Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• 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)
• 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)
• Pointwise Feasibility of Gaussian Process-based Safety-Critical Control under Model Uncertainty [77.18483084440182]
  Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs) are popular tools for enforcing safety and stability of a controlled system, respectively. We present a Gaussian Process (GP)-based approach to tackle the problem of model uncertainty in safety-critical controllers that use CBFs and CLFs.
  arXiv  Detail & Related papers  (2021-06-13T23:08:49Z)
• Closing the Closed-Loop Distribution Shift in Safe Imitation Learning [80.05727171757454]
  We treat safe optimization-based control strategies as experts in an imitation learning problem. We train a learned policy that can be cheaply evaluated at run-time and that provably satisfies the same safety guarantees as the expert.
  arXiv  Detail & Related papers  (2021-02-18T05:11:41Z)

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.