Enumeration-Guided Training of Neural Hamilton-Jacobi Safety Certificates

Mihaela-Larisa Clement; Tosca Pierro; Ezio Bartocci; Luca Marzari

cs.ROOct 20, 2026

Enumeration-Guided Training of Neural Hamilton-Jacobi Safety Certificates

Authors: Mihaela-Larisa Clement, Tosca Pierro, Ezio Bartocci, Luca Marzari

Organizations: TU Wien, Vienna, Austria · AIT Austrian Institute of Technology, Vienna, Austria · Università Politecnica delle Marche, Italy

Abstract

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\pm 0.15$	$1.0\pm 0.0-4.2\pm 0.1$	$219\pm 39$	$\mathbf{97.39\pm 0.35}$	$\mathbf{1.0\pm 0.0-2.6\pm 0.5}$	$\mathbf{108\pm 32}$
Unicycle	$94.26\pm 1.15$	$1.3\pm 0.6-77.0\pm 18.8$	$5793\pm 6569$	$\mathbf{94.59\pm 0.73}$	$\mathbf{1.0\pm 0.0-52.1\pm 3.5}$	$\mathbf{1287\pm 823}$
RoboRacer	N/A	–	Timeout	$\mathbf{61.62\pm 10.47}$	$\mathbf{6.33\pm 1.15-8.99\pm 1.70}$	$\mathbf{1729\pm 21.34}$
Cart Pole	$\mathbf{45.94\pm 4.70}$	$4.67\pm 2.52-22.33\pm 26.07$	$8326\pm 1897$	$45.02\pm 4.81$	$\mathbf{2.00\pm 0.00-5.08\pm 1.26}$	$\mathbf{1970\pm 1058}$
Robot Arm	$49.02\pm 8.29$	$9.0\pm 10.4-47.0\pm 14.2$	$7955\pm 10340$	$\mathbf{69.87\pm 2.21}$	$\mathbf{7.0\pm 2.6-69.5\pm 17.4}$	$\mathbf{1732\pm 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\pm 0.30$	$1934\pm 506$	$\mathbf{97.29\pm 0.19}$	$\mathbf{1563\pm 111}$
Robot Arm	N/A	Timeout	$\mathbf{69.14\pm 0.60}$	$\mathbf{2129\pm 81}$

Table 3: Ablation on the source of counterexamples.

	MILP		$\alpha,\beta$ -CROWN
Method	TFR	Iters.	TFR	Iters.
PGD	$96.94\pm 0.15$	$2014\pm 141$	$97.04\pm 0.21$	$1866\pm 384$
Enum	$\mathbf{97.29\pm 0.19}$	$\mathbf{1563\pm 111}$	$\mathbf{97.25\pm 0.58}$	$\mathbf{1704\pm 457}$
PGD	$96.78\pm 0.21$	$965\pm 277$	$96.82\pm 0.23$	$906\pm 195$
Enum	$\mathbf{97.90\pm 0.12}$	$\mathbf{496\pm 50}$	$\mathbf{97.45\pm 0.29}$	$\mathbf{609\pm 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\pm 0.0$	$-0.067\pm 0.037$
Backup	4/5	$100\pm 0.0$	$-0.041\pm 0.056$
Shield (Our)	0/5	58.2 $\pm$ 26.0	+0.679 $\pm$ 0.677

Table 5: RoboRacer simulation over

5

randomized obstacle placements (mean

\pm

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_{\theta}(f(x_{t},u_{t}))$ of the nominal successors rejected by the filter.

Safety-Critical Control

Safety-critical control designs controllers that keep physical systems within hard safety constraints despite uncertainty, disturbances, and limited actuation.

See all 128 papers

Gradient-Free Neural Hamilton-Jacobi Reachability for Scalable Safety-Critical Control
Sep 12, 2026Zeyuan Feng, Ali Fuat Sahin, Santiago Thorup +1Reachability Analysis Robotic Control
Department of Mechanical Engineering, École Polytechnique Fédérale de Lausanne, Switzerland
Context-Conditioned Hamilton-Jacobi Reachability for Adaptive Safety Filtering
Oct 6, 2026Ali Fuat Sahin, Yunus Yazoglu, John Talbot +3Reachability Analysis Autonomous Driving Safety Evaluation
Ecole Polytechnique Fédérale de Lausanne · Stanford University · Toyota Research Institute
Contingency-Aware Planning via Certified Neural Hamilton-Jacobi Reachability
Mar 17, 2026Kasidit Muenprasitivej, Derya AksaraySafe Motion Planning Robot Navigation
Department of Electrical and Computer Engineering, Northeastern University, Boston, MA, USA, 02115

Sep 12, 2026J/K move · Enter open · S save

Gradient-Free Neural Hamilton-Jacobi Reachability for Scalable Safety-Critical Control

Zeyuan Feng, Ali Fuat Sahin, Santiago Thorup, Somil Bansal

Department of Mechanical Engineering, École Polytechnique Fédérale de Lausanne, Switzerland

Reachability Analysis Robotic Control Robust Control

Open paper AskPDF arXiv

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.

Abstract

Safety-Critical Control

Explore similar work

Gradient-Free Neural Hamilton-Jacobi Reachability for Scalable Safety-Critical Control

Context-Conditioned Hamilton-Jacobi Reachability for Adaptive Safety Filtering

Contingency-Aware Planning via Certified Neural Hamilton-Jacobi Reachability