Safe Leraning Problems

How do we make decision making agents abide by safety requirement at runtime? Given \(T\) and spec \(\phi\), find optimal \(\pi^{*}\) to solve \(T\) such that \(\pi^{*} \text{ SAT } \phi\) using some notion of satisfaction.

• What is the notion of safety?
• what are the requirements in temporal logic?
• How do we enforce compliance?
• How do we prove compliance?

why not just apply formal methods to AI?

• environments change…
• notion of safety for stochastic systems are random
• neural networks are not easily probable since they are approximations of what we are trying to model

MASA Library

MASA uses shielding as the key technique for ensuring safety.

CMDP

Constrained MDP. Similarly to before, we want to maximize discounted returns while not exceeding cost:

\begin{equation} \max_{\pi} \mathbb{E}_{\pi}\qty [\sum_{t=0}^{\infty} y^{t}R_{t}] \end{equation}

subject to: \(\mathbb{E}_{\pi}\qty [\sum_{t=0}^{\infty} y^{t} C_{t}] < d\)

Shielding

We take only actions that are safe, as in:

\begin{equation} \max_{\infty}\mathbb{E}_{\infty} \qty [\sum_{t=0}^{\infty} y^{t}R_{t}] \end{equation}

subject to shield: \(A_{t} \in \mathcal{U}_{\text{safe}}\). Intuitively, we run the main policy and if its action does not lie in the safe set we run the backup policy.

assumption

• strong correctness grantees
• but safety definitions are required a priori
• solving this shield can be computationally expensive

solution

Train a world model learned from the latest space, to roll out future actions to see if its safe/action is complied.

This does not assume access to some abstraction representing safety.