Enumeration-Guided Training: Building Reliable Neural Hamilton-Jacobi Safety Certificates

Why Are Neural Safety Certificates Hard to Train?

Hamilton-Jacobi (HJ) reachability analysis can provide formal safety guarantees for control systems, but training accurate neural certificates is challenging. The core difficulty is that unsafe regions are often hard to characterize precisely, causing learned certificates to misjudge near boundaries. Although traditional adversarial attack methods can generate counterexamples, these counterexamples are often insufficiently precise and fail to effectively capture the failure boundary.

A recent paper proposes a verification-guided training framework that detects forward invariance violations by probabilistically enumerating safety constraints, thereby generating a compact and targeted set of counterexamples. This method not only enlarges the certified region of the certificate but also reduces certification time, and it achieves zero safety violations in real-world scenarios.

Hamilton-Jacobi (HJ) reachability analysis is a formal verification method based on optimal control theory for dynamical systems. Its core idea is to solve a partial differential equation—the HJ equation—whose value function characterizes the set of states reachable within a finite time from a given initial state (i.e., the reachable set). If the reachable set is disjoint from the set of unsafe states, then the system is safe from that initial state. However, the HJ equation has no analytical solution for general nonlinear systems, and numerical solving faces the curse of dimensionality. Therefore, recent research has turned to approximating the HJ value function with neural networks, the so-called "neural certificates." The training objective of a neural certificate is to make the network output approximate the true HJ value function, thereby providing provable safety guarantees in continuous state spaces. Understanding this helps grasp the precise meaning of terms such as "certificate" and "certified region" in this article.

Forward invariance is a fundamental concept in safety control: if, starting from any state within a set, the system's subsequent trajectory never leaves that set, the set is called a forward invariant set. For safety certificates, we expect the safe region defined by the certificate to be forward invariant—that is, once entered, safety constraints are never violated. A forward invariance violation means there exists some state that the certificate judges to be safe, but the system's trajectory starting from that state enters an unsafe region. The phrase "probabilistically enumerating safety constraints to detect forward invariance violations" in this article refers to finding such counterexample states through sampling and enumeration, thereby exposing the certificate's defects near the boundary.

How Does the Enumeration-Guided Training Framework Work?

The core of the framework is the "probabilistic enumeration" strategy. Instead of relying on standard adversarial attacks to generate counterexamples, it identifies states that are misclassified by the certificate—i.e., forward invariance violations—by enumerating safety constraints. These states form a compact set of counterexamples that more precisely delineate the failure boundary.

Fine-tuning a pretrained HJ value function with this counterexample set can significantly enlarge the certified region while reducing the time required for certification. The method shows consistent improvements across multiple benchmarks. This "detect-then-fine-tune" loop makes the certificate more reliable in critical regions.

Comparison with Traditional Adversarial Attacks

Standard adversarial attacks typically generate scattered counterexamples that struggle to cover the full extent of the failure boundary. In contrast, enumeration-guided methods produce counterexamples that are more concentrated and representative, so the fine-tuned certificate has a markedly lower misjudgment rate near the boundary. The paper points out that this representation captures the failure boundary more precisely than inputs generated by standard adversarial attacks.

Adversarial attacks in machine learning generally refer to applying small perturbations to inputs to induce erroneous model outputs. In the context of neural certificates, adversarial attacks are used to find states that the certificate misjudges: gradient optimization searches the state space for points where the certificate value is close to the safety threshold but is actually unsafe, serving as counterexamples for fine-tuning the certificate. However, standard adversarial attacks typically perturb only individual samples, and the generated counterexamples are independent and scattered, making it difficult to systematically cover the failure boundary. Enumeration-guided methods differ: by enumerating combinations of safety constraints or systematically sampling the state space, they can more comprehensively characterize the regions where the certificate fails, resulting in a more compact and representative set of counterexamples.

Safety Shielding Mechanism During Deployment

Based on the refined certificate, the authors introduce a shielding mechanism that enforces safety constraints during deployment. This mechanism monitors the system state in real time and switches to a safe policy once a potential violation is predicted.

In the Isaac Sim physics simulation environment, the safety filter was evaluated under high-speed, safety-critical conditions. Compared with a nominal controller and a backup strategy based on a linear quadratic regulator (LQR), the method achieved zero safety constraint violations.

Validation on a Real-World Autonomous Racing Car

In addition to simulation, the research team validated the mechanism in real-world autonomous racing car experiments. In high-speed racing scenarios, the safety filter successfully avoided all safety violations, whereas baseline methods exhibited violations. This demonstrates the method's effectiveness in real-world dynamic environments.

Safety shielding is a runtime assurance technique: during system deployment, a monitoring module continuously observes the system state, and when it detects an imminent unsafe behavior, the shielding mechanism overrides the nominal controller's output and switches to a verified safe fallback policy. In this article, the shielding mechanism relies on the refined neural certificate to judge in real time whether the current state is safe, triggering a switch if a potential violation is predicted. Unlike offline verification, shielding provides an online fallback, so even if the certificate has small errors outside the training distribution, actual violations can be avoided during deployment. Isaac Sim is a robotics simulation platform developed by NVIDIA that provides high-fidelity physics simulation and is often used for closed-loop testing of safety-critical algorithms.

Significance for Safety-Critical Systems

The contribution of this work lies in combining formal verification with deep learning to improve the reliability of neural certificates through enumeration-guided training. For safety-critical domains such as autonomous driving and robotics, methods that can provide provable safety guarantees are of significant value.

In the future, the framework is expected to scale to more complex systems and further reduce the computational cost of certification. As neural certificates see increasing industrial adoption, such verification-guided training methods may become standard practice.

One-line Summary

An enumeration-guided training framework generates compact counterexamples by probabilistically enumerating safety constraints, fine-tuning neural certificates to improve safety certification and achieve zero-violation deployment.

Paragraph Summary

To address the difficulty of precisely characterizing unsafe regions and the imprecision of adversarial-attack counterexamples in neural safety certificate training, this article introduces a verification-guided training framework. The framework employs a probabilistic enumeration strategy to detect forward invariance violations, generating a compact and targeted set of counterexamples used to fine-tune a pretrained Hamilton-Jacobi value function, thereby enlarging the certified region and reducing certification time. Based on the refined certificate, the authors design a deployment-time safety shielding mechanism that monitors the state in real time and switches to a safe policy when a violation is predicted. In both Isaac Sim simulation and real-world autonomous racing car experiments, the method achieves zero safety violations, outperforming a nominal controller and an LQR backup strategy. This work combines formal verification with deep learning to provide provable safety guarantees for safety-critical systems.