Acknowledgements

Motivation

• Learning-enabled components are becoming increasingly intertwined with our day-to-day lives
• There are little formal guarantees of safe operation, which is dangerous when applied in safety-critical domains

Robustness Analysis of Neural Networks in the Loop

• Problem setting: Continuous-time system in feedback with neural network
• Efficient and scalable certification of neural network controlled systems
• Trainable conditions: backpropogate information to improve robustness

Reachable Set Computation

Existing Methods

Crucial Tradeoffs: how to balance accuracy, efficiency, and guarantees?

In This Talk

Simple theoretical modifications \(\implies\) accuracy benefits for little computational cost

The Linear Systems Case: Supporting Hyperplanes

The Linear Systems Case: H-Polytopes

The Linear Systems Case: Nonlinear Supports

The Linear Systems Case: Ellipsoids as \(\ell_2\) Normotopes

Nonlinear Systems: Templated H-Polytopes

Connection: Parametric Embedding System

Summary: \(x(t)\in\{x : \alpha(t)(x - {\mathring{x}}(t)) \leq y(t)\}\) if

Our Idea:

• Combine \(\alpha\) evolution with offset bounding for nonlinear systems
• Generalize to any constraint-based set representation

A Quick Preview

We can define a new class of sets as the intersection of \(\alpha\)-parameterized sublevel sets: \[ \{x : g(\alpha,x - {\mathring{x}}) \leq y\} = \bigcap_{k=1}^{{n_y}} \{x : g_k(\alpha,x - {\mathring{x}}) \leq y_k\}, \] for centering point \({\mathring{x}}\in\mathbb{R}^{n_x}\), parameters \(\alpha\in\mathbb{R}^{n_\alpha}\), offsets \(y\in\mathbb{R}^{n_y}\), and nonlinearity \(g:\mathbb{R}^{n_\alpha}\times\mathbb{R}^{n_x}\to\mathbb{R}^{n_y}\).

We will define dynamics on \({\mathring{x}},\alpha,y\) \[ \dot{{\mathring{x}}} = f({\mathring{x}}), \quad \dot{\alpha} = ??, \quad \dot{y} = ??, \] such that every trajectory of the system was contained in the trajectory of this embedding system as \[ x_0\in \{x : g(\alpha(t_0),x - {\mathring{x}}(t_0)) \leq y(t_0)\} \implies x(t) \in \{x : g(\alpha(t),x - {\mathring{x}}(t)) \leq y(t)\}. \]

Parametopes: General Constraint-Based Set Representation

Theory: Reachable Sets via Controlled Parametric Embeddings

Theorem Intuition: Geometric Interpretation of Terms

\[ \begin{gathered} \forall k, \quad x \in \left(\!\left( {\mathring{x}},\alpha,y \right)\!\right)_g^k = \{x\in\mathbb{R}^{n_x}: g(\alpha,x - {\mathring{x}}) \leq y,\, g_k(\alpha,x - {\mathring{x}}) = y_k\}, \quad w\in \mathcal{W}\implies \\ \dot{y}_k = E_k(t,{\mathring{x}},\alpha,y) \geq \frac{\partial g_k}{\partial \alpha}(\alpha,x - {\mathring{x}}) [U(t,{\mathring{x}},\alpha,y)] + \frac{\partial g_k}{\partial x} (\alpha,x - {\mathring{x}}) [f(x,w) - f({\mathring{x}},{\mathring{w}})] \end{gathered} \]

Theorem Intuition: Bound on Facets

Our inequality is reminiscent of some standard results \[ \begin{gathered} \forall k, \quad x \in \left(\!\left( {\mathring{x}},\alpha,y \right)\!\right)_g^k = \{x\in\mathbb{R}^{n_x}: g(\alpha,x - {\mathring{x}}) \leq y,\, g_k(\alpha,x - {\mathring{x}}) = y_k\}, \quad w\in \mathcal{W}\implies \\ \dot{y}_k = E_k(t,{\mathring{x}},\alpha,y) \geq \frac{\partial g_k}{\partial \alpha}(\alpha,x - {\mathring{x}}) [U(t,{\mathring{x}},\alpha,y)] + \frac{\partial g_k}{\partial x} (\alpha,x - {\mathring{x}}) [f(x,w) - f({\mathring{x}},{\mathring{w}})] \end{gathered} \]

1. Nagumo’s theorem: \(\mathcal{S}\) is invariant if \(f(x)\) points inside \(\mathcal{S}\) for every \(x\in\partial\mathcal{S}\) (\(\partial\mathcal{S}\) is analogous to \(\left(\!\left( {\mathring{x}},\alpha,y \right)\!\right)_g^k\))
2. Kamke condition: monotone if \(a\leq b\), \(a_k = b_k\) implies \(f_k(a) \leq f_k(b)\) (analogous to \(g_k(\alpha,x - {\mathring{x}}) = y_k\))

Statements about the flow become boundary conditions on the system vector field \(f\) in continuous-time

Technical assumption: Require transverse facet intersections, meaning \[ \left\{\frac{\partial g_k}{\partial x}(\alpha,x - {\mathring{x}}) : \forall k \text{ s.t. } g_k(\alpha,x - {\mathring{x}}) = y_k\right\} \] is a linearly independent subset of \((\mathbb{R}^{n_x})^*\).

Theorem Inequality: Computational Bounds

\[ \begin{gathered} % x \in \param{\ox,\alpha,y}_g^k, \quad w\in \calW \implies \\ \dot{y}_k = E_k(t,{\mathring{x}},\alpha,y) \geq \sup_{ x\in\left(\!\left( {\mathring{x}},\alpha,y \right)\!\right)_g^k,\, w\in \mathcal{W}} \left[\frac{\partial g_k}{\partial \alpha}(\alpha,x - {\mathring{x}}) [U(t,{\mathring{x}},\alpha,y)] + \frac{\partial g_k}{\partial x} (\alpha,x - {\mathring{x}}) [f(x,w) - f({\mathring{x}},{\mathring{w}})] \right] \end{gathered} \] How can we obtain comuptationally efficient and guaranteed bounds of this inequality?

• Use interval analysis as an efficient function bounding tool
• In many special cases (intervals, polytopes, normotopes), there are simple and accurate forms
• Linear differential inclusions for first-order dynamics abstraction

Interval Analysis

• Automatable through composition: \(\mathsf{F}= \mathsf{F}_1 \circ \mathsf{F}_2\) is an inclusion function for \(f = f_1\circ f_2\)

Inclusion Primitives

Basics of JAX: A Numerical Computation Library for Python

• These transformations are arbitrarily composable.

Basics of JAX: A Numerical Computation Library for Python

import jax
import jax.numpy as jnp

def f (x) :
  return jnp.sin(x**2)

f_grad = jax.grad(f)
print(f_grad(.5), 2*.5*jnp.cos(.5**2))

• These transformations are arbitrarily composable.

immrax.natif: JAX Transformation for Interval Analysis

{ lambda ; a:f32[5]. let
    b:f32[5] = integer_pow[y=2] a
    c:f32[5] = sin b
  in (c,) }

{ lambda ; a:f32[5]. let
    b:f32[5] = integer_pow[y=2] a
    c:f32[5] = sin b
  in (c,) }

{ lambda ; a:f32[5]. let
    b:f32[5] = integer_pow[y=2] a
    c:f32[5] = sin b
  in (c,) }

immrax.natif: JAX Transformation for Interval Analysis

import jax
import jax.numpy as jnp
from immrax import natif, interval

def f (x) :
  return jnp.sin(x**2)

F = natif(f)
print(F(interval(-0.5, 0.5)))

A Basic Prototype to Bound Theorem’s Inequality

\[ \begin{gathered} % x \in \param{\ox,\alpha,y}_g^k, \quad w\in \calW \implies \\ \dot{y}_k = E_k(t,{\mathring{x}},\alpha,y) \geq \sup_{ x\in\left(\!\left( {\mathring{x}},\alpha,y \right)\!\right)_g^k,\, w\in \mathcal{W}} \underbrace{\left[\frac{\partial g_k}{\partial \alpha}(\alpha,x - {\mathring{x}}) [U(t,{\mathring{x}},\alpha,y)] + \frac{\partial g_k}{\partial x} (\alpha,x - {\mathring{x}}) [f(x,w) - f({\mathring{x}},{\mathring{w}})] \right]}_{=:\xi_k(x,w)} \end{gathered} \]

Example: Control Nudging Using Differentiable Verification

• Controlled by a feed-forward trajectory \(u(t)\) from MPC on nominal trajectory
• Input curve \(u(t)\) is differentiable with respect to safety violation

Dynamics Abstraction: Mixed Jacobian Linear Differential Inclusion

Special Cases Addressed in Our Work

Each of the following set representations have been implemented in immrax using the mixed Jacobian linear differential inclusion.

Neural Networks in the Loop

Use CROWN [14] to obtain the linear bounds \[ Cx + \underline{d}\leq \pi(x) \leq Cx + \overline{d}. \] Combine with mixed Jacobian LDI [15] to get \[ f(x,\pi(x)) - f({\mathring{x}},\pi({\mathring{x}})) \in \underbrace{([\mathcal{M}^x] + [\mathcal{M}^u]C)}_{\text{first-order interactions}}(x - {\mathring{x}}) + \underbrace{R}_{\text{remainder}} \]

GPU Parallelizable Verification

Training Robustly Forward Invariant Neural Networks

Training Robust Neural Networks: Polytope Forward Invariance

• Embedding output \(E\) is differentiable with respect to neural network parameters \(\pi\)

Training Robust Neural Networks: Polytope Forward Invariance

• Embedding output \(E\) is differentiable with respect to neural network parameters \(\pi\)

Injecting Parameter Dynamics: Adjoint of the Linearization

In the previous slides, we only considered the \(\dot{\alpha} = 0\) case.

Recall for the linear system \(\dot{x} = Ax\), the \[ \dot{\alpha} = -\alpha A \] resulted in a cancellation leading to \(\dot{y} = 0\), and optimal constraints supporting the true reachable set.

For nonlinear systems \(\dot{x} = f(x)\), we consider the following as a good guess for “good” parameter dynamics. \[ \dot{\alpha} = -\alpha \frac{\partial f}{\partial x} ({\mathring{x}}) \]

• We can incorporate this “feedback” term directly into the previously discussed embedding systems.

ARCH-COMP AINNCS Benchmarks: Efficiency and Accuracy

Example: Large-Scale Vehicle Platoon

• Second-order vehicle platoon, 4 states for each vehicle
• Lead vehicle feed-forward MPC to navigate around obstacle, followers use nonlinear feedback to track displacement from leading agent

Example: Robot Arm

Example: Reach-iLQR for Van der Pol Oscillator

Reachable Sets via Lie Algebra

Reachable Sets via Lie Algebra (examples)

Contraction Theory on Homogeneous Manifolds

Contraction Theory on Homogeneous Manifolds (examples)

Conclusion

1. Controlled parametric embeddings allow for efficient reachable set computations with a hypercontrol dynamically shaping the set
2. Simple theoretical modifications (e.g., adding \(\dot{\alpha} = -\alpha \frac{\partial f}{\partial x}({\mathring{x}})\)) can drastically improve reachable set estimates for little computational cost
3. immrax is our implementation of interval analysis using JAX for Python, supporting JIT compilation, automatic differentiation, and GPU parallelization.
4. [output] is differentiable with respect to [input]—allows for safety filtering, training robust neural network controllers, and directly optimizing the reachable set volume

Example: Jacobian-based Inclusion Function

import jax
import jax.numpy as jnp
from immrax import natif

def jacif (f) :
  J = natif(jax.jacfwd(f))
  def F (ix, xc) :
    return J(ix)@(ix-xc) + f(xc)

Special Case 1: Intervals (mixed monotonicity)

Let \(g(\alpha,x - {\mathring{x}}) = \alpha (x - {\mathring{x}})\), and \(\alpha = \left[\begin{smallmatrix} -\mathbf{I} \\ \mathbf{I} \end{smallmatrix}\right]\). Then \[ \left(\!\left( {\mathring{x}},\left[\begin{smallmatrix} -\mathbf{I} \\ \mathbf{I} \end{smallmatrix}\right],\left[\begin{smallmatrix} -\underline{y} \\ \overline{y} \end{smallmatrix}\right] \right)\!\right)_g = \{x : \underline{y}\leq x - {\mathring{x}}\leq \overline{y}\} = [{\mathring{x}}+ \underline{y},{\mathring{x}}+ \overline{y}] . \] If we set \(\dot{\alpha} = 0\), Theorem’s inequality reduces to (for an upper \(k\)-th face) \[ \sup_{\substack{x\in[{\mathring{x}}+ \underline{y},{\mathring{x}}+ \overline{y}] \\ e_k^T(x - {\mathring{x}}) = \overline{y}_k}} e_k^T (f(x) - f({\mathring{x}})) = \sup_{\substack{x\in[{\mathring{x}}+ \underline{y},{\mathring{x}}+ \overline{y}] \\ x_k = {\mathring{x}}_k + \overline{y}_k}} (f_k(x) - f_k({\mathring{x}})) \leq \overline{\mathsf{F}}_k ([{\mathring{x}}+ \underline{y}_{k\leftarrow\overline{y}_k},{\mathring{x}}+ \overline{y}]) - f_k({\mathring{x}}) =: \dot{\overline{y}}_k \]

Special Case 2: H-Polytopes (lifting + refinement)

Let \(g(\alpha,x - {\mathring{x}}) = \alpha(x - {\mathring{x}})\), for \(\alpha = \left[\begin{smallmatrix} -H \\ H \end{smallmatrix}\right]\), where \(H\) is a tall full rank matrix. Then \[ % \param{\ox,[-H^T\ H^T]^T,[-\uly^T\ \oly^T]^T}_g = \{x : \uly \leq H(x - \ox) \leq \oly\}. \left(\!\left( {\mathring{x}},\left[\begin{smallmatrix} -H \\ H \end{smallmatrix}\right],\left[\begin{smallmatrix} -\underline{y} \\ \overline{y} \end{smallmatrix}\right] \right)\!\right)_g = \{x : \underline{y}\leq H(x - {\mathring{x}}) \leq \overline{y}\}. \] If we let \(\dot{\alpha} = 0\), \(H^+\) be a left inverse of \(H\), and \(\mathcal{H}= \{Hx\}\), Theorem’s inequality reduces to (for an upper face) \[ \sup_{\substack{x : H(x - {\mathring{x}})\in[\underline{y},\overline{y}] \\ H_k(x - {\mathring{x}}) = \overline{y}_k}} H_k (f(x) - f({\mathring{x}})) = \sup_{\substack{z\in\mathcal{H}\cap[\underline{y},\overline{y}] \\ z_k = \overline{y}_k}} H_k (f(H^+z + {\mathring{x}}) - f({\mathring{x}})) \leq \overline{\mathsf{G}}_k (\mathcal{I}_\mathcal{H}(H{\mathring{x}}+ [\underline{y}_{k\leftarrow\overline{y}_k},\overline{y}])) - H_k f({\mathring{x}}) =: \dot{\overline{y}}_k \]

Special Case 3: Norms (contraction theory)