Bridging Dimensions: Confident Reachability for High-Dimensional Controllers

A talk presented by Yuang Geng at the International Symposium on Formal Methods (FM) 2024 in Milano, Italy.

Abstract:
Autonomous systems are increasingly implemented using end-to-end learning-based controllers. Such controllers make decisions that are executed on the real system, with images as one of the primary sensing modalities. Deep neural networks form a fundamental building block of such controllers. Unfortunately, the existing neural-network verification tools do not scale to inputs with thousands of dimensions -- especially when the individual inputs (such as pixels) are devoid of clear physical meaning. This paper takes a step towards connecting exhaustive closed-loop verification with high-dimensional controllers. Our key insight is that the behavior of a high-dimensional controller can be approximated with several low-dimensional controllers. To balance the approximation accuracy and verifiability of our low-dimensional controllers, we leverage the latest verification-aware knowledge distillation. Then, we inflate low-dimensional reachability results with statistical approximation errors, yielding a high-confidence reachability guarantee for the high-dimensional controller. We investigate two inflation techniques -- based on trajectories and control actions -- both of which show convincing performance in three OpenAI gym benchmarks.

1. Bridging Dimensions:
Confident Reachability for
High-Dimensional Controllers
Yuang Geng, Jake Baldauf,
Souradeep Dutta, Chao Huang, Ivan Ruchkin

Department of Electrical and Computer Engineering
Trustworthy Engineered Autonomy (TEA) Lab

September 11, 2024



TEA

2. Agenda









2
•Motivation and background
•Deep neural control in autonomy
•Existing verification techniques
•Approach to high-dimensional verification
•Results on three case studies

3. Motivation
•End-to-end deep neural networks (DNNs) are routinely used in autonomy
•DNNs with high-dimensional inputs (images, lidar scans, ...) control the system,
•We call these high-dimensional controllers (HDC)
•DNNs with low-dimensional inputs (position, velocity, ...) control the system,
•We call these low-dimensional controllers (LDC)



3

4. Autonomous control
4 Safety guarantee?
Dynamics
HDC
Action
Update
image
Online control with HDC
Current State:
,
LDC
Dynamics
Action
Update
states
Online control with LDC

5. Verification techniques for LDC
5
Why we pick
up POLAR
Current State:
,
LDC
Dynamics Action
Update
states
Reachability techniques:
●Taylor Model
●Berstein Polynomal
●Zonotope-based

Offline
verificaiton
Verification techniques:
●Satisfiability Solvers (SAT)
●Barrier Certificates
●Probabilistic Verification
●Reachability Analysis


State set:
[0, 1] x [1, 2]
Approximation of LDC
Approximation of dynamics
Action set
Update
sets
Reachability toolbox:
●NNV
●POLAR
●Sherlock
●Verisig
●CORA

6. Why verification failes for HDC?
Position
Velocity
Steering
angle

• Small neural network
• Clear relationship between states
• Complex neural network
• Vague relationship between images
6
Safe set: |cross track error| < 1m ∩
|heading error| < 10 degree
LDC-controlled system
Pixel 1
Pixel 4096
Steering
angle

Pixel 2
set of
states
over-approximate
dynamics
next set of
states
set of
images
over-approximate
dynamics
next set of
images
Impractical to model
HDC-controlled system

7. Agenda










7
•Motivation and background
•Approach to high-dimensional verification
•High-level overview
•State-image mapping assumptions
•Details of each step
•Results on three case studies

8. Overarching approach: 5 steps
8
•Our approach provide the guarantee that the high-dimensional system reaches
the goal set ?????? from an initial set within specified time steps.
Physical
platform
Sensor
data
HDC
Control action
Safety guarantee
for HDC system
Inflated LDC
verification
(Step 4)
Retrain LDC
(optional)
(Step 5)
Verification
result #1
Low-dimensional
controller (LDC) #1
Low-dimensional
controller (LDC) #N
Verification
result #N
Reachability analysis
(Step 2)
Knowledge distillation
(Step 1)
… …
Conformal
regression
Approximation error bounds
(Step 3)

9. Image-state assumptions on data collection
•Given a well-trained HDC, obtain LDC training dataset under either assumption:
•Deterministic mapping: each state is deterministically mapped to one image (unknown function)
•Noisy mapping: deterministic mapping + zero-mean Gaussian noise

9
Camera
Image z₀
HDC
Action u₀
Camera
Image z₁
HDC
Action u₂
Initial state
Dynamics
State Action u
n
… …
Dynamics
State
Dynamics
State
Noise
Noise
Noise
Determ. mapping
training dataset
Noisy mapping
training dataset

10. Step 1: LDC training and loss function
•Knowledge distillation
•The HDC is trained by the original image-based training dataset (DDPG)
•The LDC is trained by the predictions from HDC







10
HDC Control action State s
i
Image z
i
Two-objective
gradient descent
LDC
MSE loss Learning performance
Lipschitz constant Verification performance
Training dataset for LDC
[(s
1
, ), (s
2
, ),..., (s
n
, )]
2. Lipschitz constant
Control action
1. MSE loss

11. Step 2: LDC Reachability Analysis





Position
Velocity
0
11





LDC Dynamics Safety property
Input set
Reachability analysis
Reachability analysis of LDC
≠
Reachability analysis of HDC

12. Step 3: Build statistical discrepancies

Obtaining the exact discrepancy
function is impractical

Obtain the statistical discrepancy
with conformal prediction
Advantages of conformal prediction:
1.Distribution-free statistical technique to provide valid uncertainty regions
2.Do not require strong assumptions about models

12
Conformal prediction procedure:
1.Define score function s(x, y) ∊ R
2.Compute as the X as quantile of the calibration scores:
3.Use this quantile to be the prediction sets:

4.We could guarantee
1. Exact: finite-sample coverage guarantee
2. Distribution-free: for any data distribution
3. Model-free: for any predictive model y=f(x)

Given dataset [(x1, y1), (x2, y2), …] ~ D (X, Y), conformal prediction provides a
prediction interval that guarantees that any output will be within
the with high probability, namely,

13. Paired trajectories
Step 3a: Trajectory-based discrepancy
Statistical upper bound on L1 distance between two trajectories inside the initial set










Position 20
Velocity
-2
Initial state space
1.Sample n initial points i.i.d in initial set
2.Generate two trajectories for one initial point
3.Define non-conformity score: the maximum distance ∆
between each two trajectories
4.Obtain n non-conformity scores ∆₁ … ∆ₙ
5.The r-th non-conformity score (r = ceiling((k+1)(1-α)) ) in
∆₁ … ∆ₙ₊₁ is the statistical trajectory discrepancy

13




Camera
Image z₀
HDC
Action u₀
Camera
Image z₁
HDC
Action u₂
LDC
Action u₀
LDC
Action u₂
LDC
Action u₁
LDC
Action u
n
State
… …
Initial state
Dynamics
State Action u
n
… …
Dynamics
State
Dynamics
State
Dynamics
State
Dynamics
State
Maximum difference
Sample
initial states
Conformal prediction
Statistical discrepancy

14. Step 3b: Action-based discrepancy










Position 2
Velocity
-2
Initial state space
0
1.Sample n initial points i.i.d in each initial cell
2.Generate two sequences of control actions
3.Define non-conformity score: L1 distance ∆ between
these two sequences of control actions.
4.Obtain n non-conformity scores ∆₁ … ∆ₙ
5.The r-th non-conformity score (r = ceil((k+1)(1-α))) in
∆₁ … ∆ₙ₊₁ is the statistical action-based discrepancy
14
Image z₀
HDC
Action u₀
Image z₁
HDC
Action u₁
LDC
Action u₀
LDCAction u₂
LDC
Action u₁
Initial state
Dynamics
State
Dynamics
State
Dynamics
State
Dynamics
State
Maximum difference Paired control actions
Dynamics
State Action u
n
… …
LDC
Action u
n
State
… …
Sample
initial states
Statistical upper bound on the L1 distance between two sequences of actions for initial set
Conformal prediction
Statistical discrepancy

15. Step 4: Inflate the LDC verification
•Step 3 provides the trajectory- and action-based discrepancies
•Next combine these discrepancies into the LDC verification






…
0.10.1
…
0.20.2
………


Position 2
Velocity
0
-2
Initial state space
…
0.040.05
…
0.030.08
………


Velocity
-2
0
Verification toolbox
Inflated reachability
analysis
LDC
15
Position 2
Confident safety
verification
Initial state space
Trajectory discrepancy table Action discrepancy table
alignment, elbows, thicker arros
“The inflated LDC reachable set contains the HDC reachable set with high probability”

16. Step 5: Iterative training
•Research challenge: One LDC cannot mimic HDC well
•High discrepancies cause large over-approximation error
•Large Lipchitz constants cause large over-approximation error







… 0.60.9
… 0.50.8
… 0.070.04
… 0.060.05
Position 2
Velocity
-2
Action-based
discrepancy table
0
Retrain another LDC with
lower MSE threshold
16
No need to retrain the
LDC
elbows, thicker arrows, same next
slide
High Lipschitz
constant


Retrain LDC with same
MSE but a lower
Lipschitz constant

17. Agenda










17
•Background and motivation
•Approach
•Results
•Overapproximate reachability
•Robustness to image-state noise

18. Comprehensive results
18
Will our inflated reachable set stay in the target set with 95% chance?

●All the approaches satisfy the specified
95% confidence
●Multi-LDC approaches always match or
outperform the one-LDC approaches
TB: Trajectory-based discrepancy; AB: Action-based discrepancy

19. Result for robustness
19
Can our approach be robust with noise involved in the mapping process?
Conclusion:
●Our approaches perform
similarly to noise-free when
under low noise variance
●Noised mapping results display
robustness of our approach



STD: standard deviation

20. Summary
20
1.Verify the safety of high-dimensional controller by combining the reachability
analysis and statistical method conformal prediction
2.Provide a iterative neural network approximation to obtain multiple LDCs mimic the
performance of HDC and reduce the overapproximation error in reachability analysis
3.Implement and evaluate our approach on three case studies: inverted pendulum,
mountain car, and cartpole
Any questions ?