在安全关键环境中部署自主网络物理系统需要闭环控制策略（即控制政策），这些策略不仅要具备良好的性能，还必须在理论上安全且稳健。虽然基于学习的方法（如强化学习）提供了灵活且可扩展的自动合成控制器的方式，但它们通常缺乏安全部署所需的形式化保证。为了解决这一问题，我们提出了一种新颖的基于仿真的方法论，能够自动合成在性能、安全和稳健性方面具有形式保证的策略。
具体而言，给定一组待验证的属性、置信参数 $\delta$ 和可接受的失败概率 $\varepsilon$，我们的方法保证所合成的策略带有证书：以至少 $1 - \delta$ 的置信度，遭遇违反给定属性的场景的概率至多为 $\varepsilon$。我们通过开发 SM-ES 算法来证明我们方法的可行性，该算法将进化策略与基于统计模型检查的验证相结合。
我们在使用 Gymnasium 和 Safety Gymnasium 测试平台的一系列连续控制任务上评估了 SMC-ES。结果表明，虽然计算成本可持续增加，但我们的算法在性能、安全和稳健性方面提供了形式保证，同时在与领先的无模型深度强化学习（DRL）和安全DRL基线的对比中表现出竞争力。
博主点评： SMC-ES 的提出为控制策略的自动合成带来了新的视角，尤其是在安全关键应用中。其结合了进化策略与统计模型检查的创新方法，能够有效解决传统强化学习方法的保证不足问题，值得在更多实际应用中探索与推广。