On Assessing The Safety of Reinforcement Learning algorithms Using Formal Methods

TL;DR

This paper addresses the safety of reinforcement learning agents in adversarial environments by generating adversarial agents, applying defense mechanisms like reward shaping, and using probabilistic model checking to evaluate safety guarantees.

Contribution

It introduces a framework combining adversarial agent generation, defense strategies, and formal probabilistic verification for RL safety assessment.

Findings

Reduced collisions in adversarial scenarios

Probabilistic bounds on agent safety

Effective defense mechanisms against adversarial perturbations

Abstract

The increasing adoption of Reinforcement Learning in safety-critical systems domains such as autonomous vehicles, health, and aviation raises the need for ensuring their safety. Existing safety mechanisms such as adversarial training, adversarial detection, and robust learning are not always adapted to all disturbances in which the agent is deployed. Those disturbances include moving adversaries whose behavior can be unpredictable by the agent, and as a matter of fact harmful to its learning. Ensuring the safety of critical systems also requires methods that give formal guarantees on the behaviour of the agent evolving in a perturbed environment. It is therefore necessary to propose new solutions adapted to the learning challenges faced by the agent. In this paper, first we generate adversarial agents that exhibit flaws in the agent's policy by presenting moving adversaries. Secondly, We use reward shaping and a modified Q-learning algorithm as defense mechanisms to improve the agent's policy when facing adversarial perturbations. Finally, probabilistic model checking is employed to evaluate the effectiveness of both mechanisms. We have conducted experiments on a discrete grid world with a single agent facing non-learning and learning adversaries. Our results show a diminution in the number of collisions between the agent and the adversaries. Probabilistic model checking provides lower and upper probabilistic bounds regarding the agent's safety in the adversarial environment.