Table of Contents
Fetching ...

Promises of Deep Kernel Learning for Control Synthesis

Robert Reed, Luca Laurenti, Morteza Lahijanian

TL;DR

The paper addresses safe control of unknown, stochastic dynamical systems under complex temporal logic specifications by learning dynamics with Deep Kernel Learning and translating the learned model into an Interval Markov Decision Process for formal synthesis. The approach combines neural priors with Gaussian process uncertainty to produce scalable, accurate abstractions and leverages existing IMDP/LTLf tools to synthesize robust controllers with guarantees. Key contributions include (i) a scalable data-driven framework for control synthesis with hard guarantees, (ii) an efficient IMDP abstraction technique for DKL models, (iii) an architecture design for fast and accurate abstraction, and (iv) demonstration on benchmarks up to 5 dimensions showing substantial improvements over state-of-the-art methods. The work advances data-driven verification and control by enabling high-dimensional, uncertain systems to be controlled with provable performance under complex specifications, with practical implications for safety-critical autonomous systems.

Abstract

Deep Kernel Learning (DKL) combines the representational power of neural networks with the uncertainty quantification of Gaussian Processes. Hence, it is potentially a promising tool to learn and control complex dynamical systems. In this work, we develop a scalable abstraction-based framework that enables the use of DKL for control synthesis of stochastic dynamical systems against complex specifications. Specifically, we consider temporal logic specifications and create an end-to-end framework that uses DKL to learn an unknown system from data and formally abstracts the DKL model into an Interval Markov Decision Process (IMDP) to perform control synthesis with correctness guarantees. Furthermore, we identify a deep architecture that enables accurate learning and efficient abstraction computation. The effectiveness of our approach is illustrated on various benchmarks, including a 5-D nonlinear stochastic system, showing how control synthesis with DKL can substantially outperform state-of-the-art competitive methods.

Promises of Deep Kernel Learning for Control Synthesis

TL;DR

The paper addresses safe control of unknown, stochastic dynamical systems under complex temporal logic specifications by learning dynamics with Deep Kernel Learning and translating the learned model into an Interval Markov Decision Process for formal synthesis. The approach combines neural priors with Gaussian process uncertainty to produce scalable, accurate abstractions and leverages existing IMDP/LTLf tools to synthesize robust controllers with guarantees. Key contributions include (i) a scalable data-driven framework for control synthesis with hard guarantees, (ii) an efficient IMDP abstraction technique for DKL models, (iii) an architecture design for fast and accurate abstraction, and (iv) demonstration on benchmarks up to 5 dimensions showing substantial improvements over state-of-the-art methods. The work advances data-driven verification and control by enabling high-dimensional, uncertain systems to be controlled with provable performance under complex specifications, with practical implications for safety-critical autonomous systems.

Abstract

Deep Kernel Learning (DKL) combines the representational power of neural networks with the uncertainty quantification of Gaussian Processes. Hence, it is potentially a promising tool to learn and control complex dynamical systems. In this work, we develop a scalable abstraction-based framework that enables the use of DKL for control synthesis of stochastic dynamical systems against complex specifications. Specifically, we consider temporal logic specifications and create an end-to-end framework that uses DKL to learn an unknown system from data and formally abstracts the DKL model into an Interval Markov Decision Process (IMDP) to perform control synthesis with correctness guarantees. Furthermore, we identify a deep architecture that enables accurate learning and efficient abstraction computation. The effectiveness of our approach is illustrated on various benchmarks, including a 5-D nonlinear stochastic system, showing how control synthesis with DKL can substantially outperform state-of-the-art competitive methods.
Paper Structure (18 sections, 2 theorems, 22 equations, 4 figures, 3 tables)

This paper contains 18 sections, 2 theorems, 22 equations, 4 figures, 3 tables.

Key Result

Theorem 1

For $\mu \in \mathbb{R}$ and $\sigma \in \mathbb{R}_{\geq 0}$ and closed interval $\theta= [\underline{\theta}, \overline{\theta}] \subset \mathbb{R}$, define function Further, given region $q \in \bar{Q}$, let $[\underline{M}_{q,a}, \overline{M}_{q,a}]$ and $[\underline{\Sigma}_{q,a}, \overline{\Sigma}_{q,a}]$ be the poster mean and variance of DKL as reported in eqn:RangesMean-eqn:RangesVarianc

Figures (4)

  • Figure 1: Results on learning a 2D vector field with (left) DKL and (right) GP. Top: the true vector field in green, the model predictive posteriors in red, and 95% confidence intervals shaded in grey. Bottom: scaled correlation function for the first dimension at one point. 1000 samples were used to pre-train the NN. Both methods use 100 samples for predictions.
  • Figure 2: Illustration of deep kernel models. Red: NN input layer, Green: hidden layers, Grey: NN output layer, Blue: base kernel. Left: DKL$^\texttt{S}$ provides single dimensional input to the kernel $k$. Right: DKL$^\texttt{F}$ provides all outputs of the NN to each kernel.
  • Figure 3: Region labeling and lower bound satisfaction probabilities $\check{p}(q)$ for experiment 1. Left: DKL$^\texttt{S}$, middle: DKL$^\texttt{F}$, and right: GP. Top: the initial abstraction, Bottom: after two refinements. Green: $Q^{yes}$, yellow: $Q^?$, red: $Q^{no}$.
  • Figure 4: Region labeling and lower bound satisfaction probabilities $\check{p}(q)$ for experiments 2 and 3. Left: 2D system under $\varphi_2$ and right: 5D system. Top: the initial abstraction, Bottom: after two refinements.

Theorems & Definitions (7)

  • Definition 1: LTLf
  • Remark 1
  • Definition 2: IMDP
  • Theorem 1: Efficient Computation for Tran. Prob. Bounds
  • proof
  • Theorem 2: Correctness
  • proof