Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networks
- URL: http://arxiv.org/abs/2506.15693v1
- Date: Tue, 27 May 2025 18:12:50 GMT
- Title: Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networks
- Abstract summary: We introduce a verifiable model-free safety filter based on Hamilton-Jacobi reachability analysis.<n>Our proposed approach successfully synthesizes formally verified, model-free safety certificates across four standard safe-control benchmarks.
- Score: 8.042618833885168
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Recent learning-based safety filters have outperformed conventional methods, such as hand-crafted Control Barrier Functions (CBFs), by effectively adapting to complex constraints. However, these learning-based approaches lack formal safety guarantees. In this work, we introduce a verifiable model-free safety filter based on Hamilton-Jacobi reachability analysis. Our primary contributions include: 1) extending verifiable self-consistency properties for Q value functions, 2) proposing a multiplicative Q-network structure to mitigate zero-sublevel-set shrinkage issues, and 3) developing a verification pipeline capable of soundly verifying these self-consistency properties. Our proposed approach successfully synthesizes formally verified, model-free safety certificates across four standard safe-control benchmarks.
Related papers
- Selective Safety Steering via Value-Filtered Decoding [54.87935112120107]
Large language models (LLMs) are trained to align with human values, but their generations may still violate safety constraints.<n>Existing decoding-time steering methods often intervene unnecessarily, modifying generations that would have been safe under the base model.<n>We propose a new test-time steering method designed to reduce such unnecessary interventions while improving the safety of unsafe responses.
arXiv Detail & Related papers (2026-05-14T12:13:08Z) - CAPSULE: Control-Theoretic Action Perturbations for Safe Uncertainty-Aware Reinforcement Learning [2.28224729577679]
We propose a safe reinforcement learning framework that learns a probabilistic control-affine dynamics model in an offline setting.<n>Our approach achieves returns comparable to those of existing baselines while significantly reducing safety violations.
arXiv Detail & Related papers (2026-04-26T07:31:30Z) - SecPI: Secure Code Generation with Reasoning Models via Security Reasoning Internalization [50.71047638695205]
Reasoning language models (RLMs) are increasingly used in programming.<n>Yet, even state-of-the-art RLMs frequently introduce critical security vulnerabilities in generated code.<n>We present SecPI, a fine-tuning pipeline that teaches RLMs to internalize structured security reasoning.
arXiv Detail & Related papers (2026-04-04T04:29:11Z) - BarrierSteer: LLM Safety via Learning Barrier Steering [83.12893815611052]
BarrierSteer is a novel framework that formalizes safety by embedding learned non-linear safety constraints directly into the model's latent representation space.<n>We show that BarrierSteer substantially reduces adversarial success rates, decreases unsafe generations, and outperforms existing methods.
arXiv Detail & Related papers (2026-02-23T18:19:46Z) - Deep QP Safety Filter: Model-free Learning for Reachability-based Safety Filter [24.58681190669229]
We introduce Deep QP Safety Filter, a fully data-driven safety layer for black-box dynamical systems.<n>Our method learns a Quadratic-Program (QP) safety filter without model knowledge by combining Hamilton-Jacobi (HJ) reachability with model-free learning.
arXiv Detail & Related papers (2026-01-29T05:49:48Z) - LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems [0.8574682463936006]
Traditional formal verification tools fall short when faced with systems that embed both opaque black-box AI components and complex dynamics.<n>We introduce LUCID, a verification engine for certifying safety of black-box embedding dynamical systems.<n> LUCID is the first known tool capable of establishing quantified safety guarantees for such systems.
arXiv Detail & Related papers (2025-12-12T17:46:50Z) - How to Train Your Latent Control Barrier Function: Smooth Safety Filtering Under Hard-to-Model Constraints [21.03977709777739]
We show that reachability value functions can be adapted to be control barrier functions (CBFs) for smooth optimization-based filtering.<n>We propose the LatentCBF, which addresses both challenges through gradient penalties that lead to smooth margin functions without additional labeling.<n>Experiments on simulated benchmarks and hardware with a vision-based manipulation policy demonstrate that LatentCBF enables smooth safety filtering.
arXiv Detail & Related papers (2025-11-23T20:15:28Z) - A Physics-Informed Machine Learning Framework for Safe and Optimal Control of Autonomous Systems [8.347548017994178]
Safety and performance could be competing objectives, which makes their co-optimization difficult.<n>We propose a state-constrained optimal control problem, where performance objectives are encoded via a cost function and safety requirements are imposed as state constraints.<n>We demonstrate that the resultant value function satisfies a Hamilton-Jacobi-Bellman equation, which we approximate efficiently using a novel machine learning framework.
arXiv Detail & Related papers (2025-02-16T09:46:17Z) - Q-learning-based Model-free Safety Filter [6.391687991642366]
This paper proposes a simple, plugin-and-play, and effective model-free safety filter learning framework.<n>We introduce a novel reward formulation and use Q-learning to learn Q-value functions to safeguard arbitrary task specific nominal policies.
arXiv Detail & Related papers (2024-11-29T16:16:59Z) - Safety Filters for Black-Box Dynamical Systems by Learning Discriminating Hyperplanes [26.242421052632807]
Learning-based approaches are emerging as an effective approach for safety filters for black-box dynamical systems.
We present two strategies to learn the discriminating hyperplane: (a) a supervised learning approach, using pre-verified control invariant sets for labeling, and (b) a reinforcement learning (RL) approach, which does not require such labels.
arXiv Detail & Related papers (2024-02-07T21:49:51Z) - Safe Online Dynamics Learning with Initially Unknown Models and
Infeasible Safety Certificates [45.72598064481916]
This paper considers a learning-based setting with a robust safety certificate based on a control barrier function (CBF) second-order cone program.
If the control barrier function certificate is feasible, our approach leverages it to guarantee safety. Otherwise, our method explores the system dynamics to collect data and recover the feasibility of the control barrier function constraint.
arXiv Detail & Related papers (2023-11-03T14:23:57Z) - Evaluating Model-free Reinforcement Learning toward Safety-critical
Tasks [70.76757529955577]
This paper revisits prior work in this scope from the perspective of state-wise safe RL.
We propose Unrolling Safety Layer (USL), a joint method that combines safety optimization and safety projection.
To facilitate further research in this area, we reproduce related algorithms in a unified pipeline and incorporate them into SafeRL-Kit.
arXiv Detail & Related papers (2022-12-12T06:30:17Z) - Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers.
We then present the pointwise feasibility conditions of the resulting safety controller.
We use these conditions to devise an event-triggered online data collection strategy.
arXiv Detail & Related papers (2022-08-23T05:02:09Z) - Safe Reinforcement Learning via Confidence-Based Filters [78.39359694273575]
We develop a control-theoretic approach for certifying state safety constraints for nominal policies learned via standard reinforcement learning techniques.
We provide formal safety guarantees, and empirically demonstrate the effectiveness of our approach.
arXiv Detail & Related papers (2022-07-04T11:43:23Z) - Joint Differentiable Optimization and Verification for Certified
Reinforcement Learning [91.93635157885055]
In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties.
We propose a framework that jointly conducts reinforcement learning and formal verification.
arXiv Detail & Related papers (2022-01-28T16:53:56Z) - Pointwise Feasibility of Gaussian Process-based Safety-Critical Control
under Model Uncertainty [77.18483084440182]
Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs) are popular tools for enforcing safety and stability of a controlled system, respectively.
We present a Gaussian Process (GP)-based approach to tackle the problem of model uncertainty in safety-critical controllers that use CBFs and CLFs.
arXiv Detail & Related papers (2021-06-13T23:08:49Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.