arXiv:2506.15693cs.LG2025-06被引 4

提出可验证的安全过滤器,让机器学习控制更安全可靠。

Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networks

  • 用哈密顿-雅可比可达性分析构建可验证的安全滤波机制
  • 在4个标准控制任务中实现形式化安全保证
  • 适合需要高可靠性安全控制的机器人和自动驾驶场景

基于学习的安全滤波器已超越传统手写控制屏障函数(CBFs)在复杂约束下的表现,但缺乏形式化安全保证。本文提出一种基于哈密顿-雅可比可达性分析的可验证、无模型安全滤波器。主要贡献包括:1)扩展了对Q值函数自洽性质的形式化验证方法;2)提出乘法结构的Q网络以缓解零水平集收缩问题;3)开发出能够严格验证自洽性质的验证流程。所提方法在四个标准安全控制基准上成功合成出形式化验证的无模型安全证书。

原文摘要 · Abstract (English)

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.

安全控制强化学习形式化验证

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。