这篇论文提出了SMC-ES，把进化策略和统计模型检查结合起来，能生成带形式安全证明的控制策略。比普通RL更靠谱。
SMC-ES是一种结合进化策略与统计模型检查的新算法，用于自动综合具有形式保证的控制策略。该方法以置信度1-δ和允许故障概率ε为参数，确保证书表明违规概率不超过ε。在Gymnasium和Safety Gymnasium的连续控制任务上评估，计算成本可持续增加，但性能与领先的无模型深度强化学习（DRL）和安全DRL基线相当。该算法为性能、安全性和鲁棒性规格提供了形式保证。
SMC-ES: Automated synthesis of formally verified control policies
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.