SMC-ES: Automated synthesis of formally verified control policies

📄 arXiv: 2607.15003v1 📥 PDF

作者: Riccardo Curcio, Toni Mancini, Enrico Tronci

分类: cs.AI, cs.LG, cs.NE

发布日期: 2026-07-16

💡 一句话要点

提出SMC-ES以自动合成形式验证的控制策略

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)

关键词: 形式验证 控制策略 进化策略 统计模型检查 安全关键系统 深度强化学习 稳健性

📋 核心要点

  1. 现有的学习方法如强化学习缺乏形式验证，无法保证控制策略在安全关键环境中的可靠性。
  2. 本文提出SMC-ES算法，通过结合进化策略与统计模型检查，实现了控制策略的自动合成与形式验证。
  3. 实验结果表明，SMC-ES在性能、安全性和稳健性方面提供了形式保证，并在计算成本可接受的情况下与现有基线竞争。

📝 摘要（中文）

在安全关键环境中部署自主网络物理系统需要既高效又可证明安全和稳健的闭环控制策略。尽管基于学习的方法如强化学习提供了灵活的控制器合成方式，但通常缺乏必要的形式保证。为此，本文提出了一种新的基于仿真的方法，自动合成具有性能、安全性和稳健性保证的控制策略。具体而言，给定一组待验证的属性、置信参数δ和可接受的失败概率ε，我们的方法保证合成的策略附带证书：在置信度至少为1-δ的情况下，遇到违反给定属性的场景的概率最多为ε。通过开发SMC-ES算法，我们将进化策略与基于统计模型检查的验证相结合，评估结果表明，尽管计算成本有所增加，但我们的算法在性能、安全性和稳健性保证方面表现出色，并且与领先的无模型深度强化学习和安全深度强化学习基线相比具有竞争力。

🔬 方法详解

问题定义：本文旨在解决在安全关键环境中，现有基于学习的控制策略缺乏形式验证的问题。现有方法通常无法提供必要的安全性和稳健性保证，限制了其在实际应用中的有效性。

核心思路：论文提出了一种基于仿真的自动合成方法，结合进化策略与统计模型检查，确保合成的控制策略不仅高效且具备形式验证的安全性和稳健性。通过设定置信参数和失败概率，提供了合成策略的形式保证。

技术框架：整体框架包括三个主要模块：首先，定义待验证的属性和性能指标；其次，利用进化策略进行控制策略的合成；最后，通过统计模型检查对合成的策略进行验证，确保其满足给定的安全和稳健性要求。

关键创新：最重要的创新在于将进化策略与统计模型检查相结合，形成了一种新的合成方法。这种方法不仅提高了控制策略的性能，还提供了形式验证的保证，解决了传统强化学习方法的不足。

关键设计：在设计中，设置了置信参数δ和允许的失败概率ε，以确保合成策略的安全性。此外，采用了适应性损失函数和特定的网络结构，以优化策略合成的效率和效果。通过这些设计，SMC-ES能够在保证形式验证的同时，保持良好的性能。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，SMC-ES在多个连续控制任务中表现出色，尽管计算成本有所增加，但在性能、安全性和稳健性方面提供了形式保证。与领先的无模型深度强化学习和安全深度强化学习基线相比，SMC-ES在多个任务中均表现出竞争力，验证了其有效性。

🎯 应用场景

该研究的潜在应用领域包括自动驾驶、无人机控制和工业自动化等安全关键系统。通过提供形式验证的控制策略，SMC-ES能够显著提高这些系统的安全性和可靠性，降低事故风险，推动自主系统在实际环境中的广泛应用。

📄 摘要（原文）

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.