形式验证神经值函数的可扩展合成用于 Hamilton-Jacobi 可达性分析
系统与控制
2025-08-01 v2 系统与控制
摘要
Hamilton-Jacobi (HJ) 可达性分析提供了一种形式化方法，用于保证受约束控制问题中的安全性。它合成一个价值函数以表示称为可行区域的长期安全集合。早期基于状态空间离散化的合成方法无法扩展到高维问题，而最近基于神经网络近似价值函数的方法结果导致不可验证的可行区域。为实现可扩展性和可验证性，我们提出了一个用于 HJ 可达性分析的经验证神经价值函数合成框架。我们的框架包含三个阶段：预训练、对抗训练和验证导向训练。我们设计了三项技术来分别解决提高可扩展性的三个挑战：边界引导的回溯 (BGB) 以提高反例搜索效率，进入状态正则化 (ESR) 以扩大可行区域，激活模式对齐 (APA) 以加速神经网络验证。我们还提供了一个神经安全证书合成和验证基准，称为 Cersyve-9，包含九个常用安全控制任务，并补充了现有神经网络验证基准。我们的框架在所有任务上成功合成了经验证的神经价值函数，我们提出的三项技术在可扩展性和效率方面优于现有方法。
引用
@article{arxiv.2407.20532,
title = {Scalable Synthesis of Formally Verified Neural Value Function for Hamilton-Jacobi Reachability Analysis},
author = {Yujie Yang and Hanjiang Hu and Tianhao Wei and Shengbo Eben Li and Changliu Liu},
journal= {arXiv preprint arXiv:2407.20532},
year = {2025}
}