Hamilton-Jacobi (HJ) reachability analysis offers formal safety guarantees for control systems, but training accurate neural certificates remains difficult, particularly when unsafe regions are hard to characterize. We propose a verification-guided training framework that addresses this by using probabilistic enumeration of safety constraints to detect forward-invariance violations, i.e., states where the learned certificate incorrectly classifies unsafe behavior. This produces a compact, targeted set of counterexamples that more precisely captures the failure boundary than inputs generated by standard adversarial attack methods. Crucially, using this representation to fine-tune a pretrained HJ value function yields larger certified regions and reduces certification time across all tested benchmarks. We further introduce a shielding mechanism based on the refined certificates to enforce safety constraints at deployment time. We evaluate the proposed safety filter in a realistic, physics-based Isaac Sim environment and through real-world autonomous racing experiments, achieving zero safety constraint violations compared to a nominal controller and a backup policy based on Linear Quadratic Regulation (LQR). These results demonstrate the effectiveness of the proposed shielding mechanism in ensuring safe operation under high-speed, safety-critical conditions.
Figures & tables
Figure 1: Overview of the proposed enumeration-guided training and online safety filter pipeline.
Figure 2: Comparison between PGD attack and approximate enumeration of unsafe regions (coverage c=95% ) for a pretrained V(x) on a toy example.
Figure 3: Block diagram of the safety filter via neural HJ certificates.
Task
State dimension
Control dimension
Dynamics
Constraint
Pendulum
2
1
Nonlinear
Linear
Unicycle
3
2
Nonlinear
Nonlinear
RoboRacer
4
1
Linear
Linear
Cart Pole
4
1
Nonlinear
Linear
Robot Arm
6
3
Linear
Nonlinear
Table 1: Overview of the considered benchmarks.
Figure 4: Comparison of best-seed certified regions for PGD+MILP and Enum+MILP on the CartPole task.
PGD+MILP [ 7 ]
Enum+MILP (Ours)
Task
TFR
#MILP Calls – Time (s)
Wall-clock time (s)
TFR
#MILP Calls – Time (s)
Wall-clock time (s)
Pendulum
96.94±0.15
1.0±0.0−4.2±0.1
219±39
97.39±0.35
1.0±0.0−2.6±0.5
108±32
Unicycle
94.26±1.15
1.3±0.6−77.0±18.8
5793±6569
94.59±0.73
1.0±0.0−52.1±3.5
1287±823
RoboRacer
N/A
–
Timeout
61.62±10.47
6.33±1.15−8.99±1.70
1729±21.34
Cart Pole
45.94±4.70
4.67±2.52−22.33±26.07
8326±1897
45.02±4.81
2.00±0.00−5.08±1.26
1970±1058
Robot Arm
49.02±8.29
9.0±10.4−47.0±14.2
7955±10340
69.87±2.21
7.0±2.6−69.5±17.4
1732±404
Table 2: PGD+MILP vs. Enum+MILP on Cersyve [ 7 ] and RobotRacer benchmarks. Results are averaged over three random seeds.
Random Sampling+MILP
Enum+MILP (Ours)
Task
TFR
Iterations
TFR
Iterations
Pendulum
96.75±0.30
1934±506
97.29±0.19
1563±111
Robot Arm
N/A
Timeout
69.14±0.60
2129±81
Table 3: Ablation on the source of counterexamples.
MILP
α,β -CROWN
Method
TFR
Iters.
TFR
Iters.
PGD
96.94±0.15
2014±141
97.04±0.21
1866±384
Enum
97.29±0.19
1563±111
97.25±0.58
1704±457
PGD
96.78±0.21
965±277
96.82±0.23
906±195
Enum
97.90±0.12
496±50
97.45±0.29
609±139
Table 4: Verification scalability on Pendulum Task with increasing value-network size 2x32 (first row), 2x64 (second row).
Collisions
Interventions (%)
Min. Clear. (m)
Nominal
5/5
0.0±0.0
−0.067±0.037
Backup
4/5
100±0.0
−0.041±0.056
Shield (Our)
0/5
58.2 ± 26.0
+0.679 ± 0.677
Table 5: RoboRacer simulation over 5 randomized obstacle placements (mean ± std). Min. Clear.: minimum distance kept to obstacle, negative on collision.
Figure 5: RoboRacer deployment of the proposed safety filter. (a) Trajectories showing an obstacle-free reference run and a run with six obstacles. The blue dashed curve denotes the planned path, while blue and green segments indicate nominal and safety-filter control, respectively. (b) Left- and right-passing maneuvers with camera views and corresponding local trajectories. The planner selects the passing side based on available room, while the safety filter checks steering commands. Negative room annotations indicate unavailable sides. Max V(x) denotes the maximum value Vθ(f(xt,ut)) of the nominal successors rejected by the filter.
Safety-critical control designs controllers that keep physical systems within hard safety constraints despite uncertainty, disturbances, and limited actuation.
Hamilton-Jacobi (HJ) reachability provides a principled framework for synthesizing safety certificates and robust controllers for safety-critical robotic systems. However, applying reachability analysis to high-dimensional nonlinear systems remains challenging: classical grid-based solvers suffer from the curse of dimensionality, continuous-time neural solvers require accurate spatial value gradients, and reinforcement-learning-based approaches often suffer from weak boundary anchoring and non-stationary adversarial policy optimization. We propose a discrete-time neural reachability framework for control-disturbance-affine systems that learns backward reachable tubes (BRTs) and backward reach-avoid tubes (BRATs) through Bellman-Isaacs value propagation. Our key idea is to combine equation-driven self-supervision with structured policy learning: rather than computing explicit PDE-gradients, we exploit the bang-bang structure of optimal safety interventions to construct approximate teacher actions from gradient-free value probes, converting adversarial actor learning into supervised policy learning. To stabilize long-horizon value propagation, we leverage the learned actor to train the value function backward from the terminal boundary using a windowed temporal curriculum, where each window is used as the boundary condition for the next window. Across benchmark problems up to 80 dimensions, our method learns accurate reachability value functions while improving stability over existing learning-based solvers. We further demonstrate observation-space scalability on F1-tenth racing with over 16,000-dimensional egocentric inputs. The learned safety filter generalizes zero-shot to unseen tracks and transfers to a physical RC car, achieving real-time robust collision avoidance.
Zeyuan Feng, Ali Fuat Sahin, Santiago Thorup +1
Department of Mechanical Engineering, École Polytechnique Fédérale de Lausanne, Switzerland
Hamilton-Jacobi reachability constructs safety certificates for specified dynamics and safety constraints, tying each certificate to the deployment context for which it is synthesized. We ask whether a single certificate can instead represent a family of context-dependent safety problems and be queried across deployment conditions without re-synthesis. We learn a backward reachable tube for an eight-state vehicle model conditioned on local boundary geometry, friction coefficient, and adversarial disturbance scale. Geometry enters through an ego-frame boundary observation that defines the local containment constraint, while friction and disturbance scale enter as explicit operating-condition variables. This allows the same value function to be queried across friction coefficients from 0.4 to 2.0 and on geometries absent from synthesis. On 11 held-out evaluation geometries, the certificate maintains containment across the full tested friction range, including simultaneous geometry and grip shifts, while remaining within 1.2 percentage points in intervention rate and 0.09 m/s in speed of certificates re-synthesized with knowledge of the test geometry. We then deploy the certificate as a sampled discrete-time control barrier function filter on a full-scale vehicle near the handling limit. Lateral containment holds in every hardware session under both adversarial driving and autonomous racing, with 99th-percentile acceleration magnitude reaching 0.99 g. Across three certificates evaluated under a fixed autonomous racing controller, lap time varies by only 3.1%, demonstrating that a context-conditioned reachability certificate can transfer to deployment geometries absent from synthesis with modest performance cost.
Ali Fuat Sahin, Yunus Yazoglu, John Talbot +3
Ecole Polytechnique Fédérale de Lausanne · Stanford University · Toyota Research Institute
Hamilton-Jacobi (HJ) reachability provides formal safety guarantees for dynamical systems, but solving high-dimensional HJ partial differential equations limits its use in real-time planning. This paper presents a contingency-aware multi-goal navigation framework that integrates learning-based reachability with sampling-based planning in unknown environments. We use Fourier Neural Operator (FNO) to approximate the solution operator of the Hamilton-Jacobi-Isaacs variational inequality under varying obstacle configurations. We first provide a theoretical under-approximation guarantee on the safe backward reach-avoid set, which enables formal safety certification of the learned reachable sets. Then, we integrate the certified reachable sets with an incremental multi-goal planner, which enforces reachable-set constraints and a recovery policy that guarantees finite-time return to a safe region. Overall, we demonstrate that the proposed framework achieves asymptotically optimal navigation with provable contingency behavior, and validate its performance through real-time deployment on KUKA's youBot in Webots simulation.
Kasidit Muenprasitivej, Derya Aksaray
Department of Electrical and Computer Engineering, Northeastern University, Boston, MA, USA, 02115