Table of Contents
Fetching ...

Repairing Learning-Enabled Controllers While Preserving What Works

Pengyuan Lu, Matthew Cleaveland, Oleg Sokolsky, Insup Lee, Ivan Ruchkin

TL;DR

The Incremental Simulated Annealing Repair (ISAR) algorithm is designed, which leverages simulated annealing on a barriered energy function to safeguard the already-correct initial states while repairing as many additional ones as possible.

Abstract

Learning-enabled controllers have been adopted in various cyber-physical systems (CPS). When a learning-enabled controller fails to accomplish its task from a set of initial states, researchers leverage repair algorithms to fine-tune the controller's parameters. However, existing repair techniques do not preserve previously correct behaviors. Specifically, when modifying the parameters to repair trajectories from a subset of initial states, another subset may be compromised. Therefore, the repair may break previously correct scenarios, introducing new risks that may not be accounted for. Due to this issue, repairing the entire initial state space may be hard or even infeasible. As a response, we formulate the Repair with Preservation (RwP) problem, which calls for preserving the already-correct scenarios during repair. To tackle this problem, we design the Incremental Simulated Annealing Repair (ISAR) algorithm, which leverages simulated annealing on a barriered energy function to safeguard the already-correct initial states while repairing as many additional ones as possible. Moreover, formal verification is utilized to guarantee the repair results. Case studies on an Unmanned Underwater Vehicle (UUV) and OpenAI Gym Mountain Car (MC) show that ISAR not only preserves correct behaviors from previously verified initial state regions, but also repairs 81.4% and 23.5% of broken state spaces in the two benchmarks. Moreover, the average signal temporal logic (STL) robustnesses of the ISAR repaired controllers are larger than those of the controllers repaired using baseline methods.

Repairing Learning-Enabled Controllers While Preserving What Works

TL;DR

The Incremental Simulated Annealing Repair (ISAR) algorithm is designed, which leverages simulated annealing on a barriered energy function to safeguard the already-correct initial states while repairing as many additional ones as possible.

Abstract

Learning-enabled controllers have been adopted in various cyber-physical systems (CPS). When a learning-enabled controller fails to accomplish its task from a set of initial states, researchers leverage repair algorithms to fine-tune the controller's parameters. However, existing repair techniques do not preserve previously correct behaviors. Specifically, when modifying the parameters to repair trajectories from a subset of initial states, another subset may be compromised. Therefore, the repair may break previously correct scenarios, introducing new risks that may not be accounted for. Due to this issue, repairing the entire initial state space may be hard or even infeasible. As a response, we formulate the Repair with Preservation (RwP) problem, which calls for preserving the already-correct scenarios during repair. To tackle this problem, we design the Incremental Simulated Annealing Repair (ISAR) algorithm, which leverages simulated annealing on a barriered energy function to safeguard the already-correct initial states while repairing as many additional ones as possible. Moreover, formal verification is utilized to guarantee the repair results. Case studies on an Unmanned Underwater Vehicle (UUV) and OpenAI Gym Mountain Car (MC) show that ISAR not only preserves correct behaviors from previously verified initial state regions, but also repairs 81.4% and 23.5% of broken state spaces in the two benchmarks. Moreover, the average signal temporal logic (STL) robustnesses of the ISAR repaired controllers are larger than those of the controllers repaired using baseline methods.
Paper Structure (18 sections, 1 theorem, 20 equations, 2 figures, 4 tables, 2 algorithms)

This paper contains 18 sections, 1 theorem, 20 equations, 2 figures, 4 tables, 2 algorithms.

Key Result

Proposition 1

The energy functions $\hat{e}(\theta)$ in Equation eq:energy_3 and $e(\theta)$ in Equation eq:energy_2 satisfy Here, $\text{Var}_{\hat{X}}[g]$ denotes the variance of a function $g$ on a finite set of inputs $\hat{X}$.

Figures (2)

  • Figure 1: Unmanned Underwater Vehicle
  • Figure 2: Repair results on initial state spaces of UUV (left column) and MC (right column). Solid green: regions in $\mathcal{S}_{\pi'}^{\mathsf{s}}$; green hatches: regions in $\mathcal{S}_{\pi'}^{\mathsf{s}'}$; red: regions in $\mathcal{S}_{\pi'}^{\mathsf{f}}$.

Theorems & Definitions (6)

  • Definition 1: Robustness Computing Subroutine
  • Definition 2: Initial State Partition
  • Definition 3: Repair with Preservation (RwP) Problem
  • Definition 4: Sound but Incomplete Verifier
  • Proposition 1: Error in Monte Carlo Integrated Energy Function
  • proof