SMC-ES: Automated synthesis of formally verified control policies
Artificial IntelligenceMachine LearningNeural and Evolutionary Computing
Summary
The authors developed a new method to create control policies for autonomous systems that not only work well but also come with formal safety and reliability guarantees. Their approach uses simulation combined with a technique called Statistical Model Checking to ensure, with high confidence, that the chance of safety violations remains very low. They introduced an algorithm named SMC-ES that blends Evolutionary Strategies and these safety checks, and tested it on common control task environments. While it requires somewhat more computation, their method achieves good performance and strong safety assurances compared to existing reinforcement learning approaches.
Authors
Riccardo Curcio, Toni Mancini, Enrico Tronci
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.