Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Certified Approximate Reachability (CARe): Formal Error Bounds on Deep Learning of Reachable Sets

Prashant Solanki, Nikolaus Vertovec, Yannik Schnitzer, Jasper Van Beers, Coen de Visser, Alessandro Abate

TL;DR

CARe delivers formal guarantees for neural reachability by tying the neural PDE residuals to ε-accurate bounds on the true backward reachability set/tube. It combines a PDE-consistent neural objective with SMT/dReal verification and a CEGIS loop to iteratively tighten the neural surrogate $V_{\theta}$ until certificates are obtained. The core result shows $V_{\theta}$ is bounded by ε-modified viscosity solutions $\overline{V}$ and $\underline{V}$, yielding concrete over-/under-approximations of BRS/BRT for continuous-time systems. A double integrator case study demonstrates practical curriculum-based training and formal verification, illustrating how CARe can provide sound, scalable certificates for higher-dimensional reachability problems.

Abstract

Recent approaches to leveraging deep learning for computing reachable sets of continuous-time dynamical systems have gained popularity over traditional level-set methods, as they overcome the curse of dimensionality. However, as with level-set methods, considerable care needs to be taken in limiting approximation errors, particularly since no guarantees are provided during training on the accuracy of the learned reachable set. To address this limitation, we introduce an epsilon-approximate Hamilton-Jacobi Partial Differential Equation (HJ-PDE), which establishes a relationship between training loss and accuracy of the true reachable set. To formally certify this approximation, we leverage Satisfiability Modulo Theories (SMT) solvers to bound the residual error of the HJ-based loss function across the domain of interest. Leveraging Counter Example Guided Inductive Synthesis (CEGIS), we close the loop around learning and verification, by fine-tuning the neural network on counterexamples found by the SMT solver, thus improving the accuracy of the learned reachable set. To the best of our knowledge, Certified Approximate Reachability (CARe) is the first approach to provide soundness guarantees on learned reachable sets of continuous dynamical systems.

Certified Approximate Reachability (CARe): Formal Error Bounds on Deep Learning of Reachable Sets

TL;DR

CARe delivers formal guarantees for neural reachability by tying the neural PDE residuals to ε-accurate bounds on the true backward reachability set/tube. It combines a PDE-consistent neural objective with SMT/dReal verification and a CEGIS loop to iteratively tighten the neural surrogate until certificates are obtained. The core result shows is bounded by ε-modified viscosity solutions and , yielding concrete over-/under-approximations of BRS/BRT for continuous-time systems. A double integrator case study demonstrates practical curriculum-based training and formal verification, illustrating how CARe can provide sound, scalable certificates for higher-dimensional reachability problems.

Abstract

Recent approaches to leveraging deep learning for computing reachable sets of continuous-time dynamical systems have gained popularity over traditional level-set methods, as they overcome the curse of dimensionality. However, as with level-set methods, considerable care needs to be taken in limiting approximation errors, particularly since no guarantees are provided during training on the accuracy of the learned reachable set. To address this limitation, we introduce an epsilon-approximate Hamilton-Jacobi Partial Differential Equation (HJ-PDE), which establishes a relationship between training loss and accuracy of the true reachable set. To formally certify this approximation, we leverage Satisfiability Modulo Theories (SMT) solvers to bound the residual error of the HJ-based loss function across the domain of interest. Leveraging Counter Example Guided Inductive Synthesis (CEGIS), we close the loop around learning and verification, by fine-tuning the neural network on counterexamples found by the SMT solver, thus improving the accuracy of the learned reachable set. To the best of our knowledge, Certified Approximate Reachability (CARe) is the first approach to provide soundness guarantees on learned reachable sets of continuous dynamical systems.

Paper Structure

This paper contains 15 sections, 7 theorems, 135 equations, 2 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Problem Setup
  3. Deep Learning Approach to HJ Reachability
  4. Formal Synthesis of Neural Value Functions
  5. ε-Accurate Value Functions
  6. Bounding the True Value Function
  7. Relating Bounds to the Neural Value Function
  8. Case Studies
  9. Training of $V_{\theta}(t,x)$
  10. Formal Verification
  11. Conclusions
  12. Bellman Optimality
  13. Monotonicity of the value function
  14. Existence and Uniqueness
  15. Proof of Theorem \ref{['theorem_viscosity_sol_hjiPde']}

Key Result

Theorem 1

The function $\overline{V}(t,x)$ is the unique viscosity solution of the $\epsilon$-modified HJ-PDE: with the Hamiltonian defined as and the terminal condition Similarly, $\underline{V}(t,x)$ is the unique viscosity solution of the $\epsilon$-modified HJ-PDE: with the Hamiltonian and the terminal condition

Figures (2)

  • Figure 1: Flowchart of the training and verification Procedure
  • Figure 2: The over-approximated reachable set is shown in red, while the learned reachable set is depicted in blue. The initial set at time $t_0 = 0$ is a circle around the centre of radius $0.25$, the time horizon is $T=1$.

Theorems & Definitions (13)

  • Theorem 1
  • Theorem 2
  • proof
  • Lemma 1
  • proof
  • Corollary 1
  • Lemma 2
  • proof
  • Lemma 3
  • proof
  • ...and 3 more