使用对数神经证书的随机动态系统策略验证
机器学习
2025-07-21 v4 系统与控制
系统与控制
摘要
我们考虑针对离散时间随机系统的神经网络策略关于可达-规避规范的验证问题。我们采用一个学习器-验证器过程，学习一个表示为神经网络的规范证书。验证该神经网络证书是一个所谓的可达-规避鞅(RASM)即可证明满足可达-规避规范。此类验证任务的现有方法依赖于计算神经网络的Lipschitz常数。这些方法在处理大的Lipschitz常数时存在困难，尤其是对于高阈值概率的可达-规避规范。我们提出了两项关键贡献以获得比现有方法更小的Lipschitz常数。首先，我们引入了对数RASM(logRASM)，其取值比RASM指数级小，因此具有更低的Lipschitz理论常数。其次，我们提出了一种基于加权范数的快速方法来计算Lipschitz常数更紧的上界。我们的实证评估表明，我们能够一致地验证概率高达99.9999%的可达-规避规范的满足性。
引用
@article{arxiv.2406.00826,
title = {Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates},
author = {Thom Badings and Wietze Koops and Sebastian Junges and Nils Jansen},
journal= {arXiv preprint arXiv:2406.00826},
year = {2025}
}
备注
Extended version (with appendix) of the paper presented at CAV 2025