用神经网络为连续时间随机系统提供可证明的概率验证边界。
Neural Continuous-Time Supermartingale Certificates
- 结合机器学习与符号推理，生成连续时间系统的概率验证证书。
- 能给出非线性系统满足可达、避让、持续等规范的概率上界。
- 适用于物理世界自主系统，适合关注安全验证的研究者。
我们首次提出针对连续时间随机动力系统的神经证书框架。现实世界的自主学习系统需要连续时间推理，但现有可学习的验证证书均基于时间离散化。受神经李雅普诺夫证书在确定性连续系统及神经上鞅证书在随机离散系统中成功应用的启发，我们提出一个连接连续时间与概率神经验证的框架。该方法融合机器学习与符号推理，生成非线性系统满足可达性、避让性与持久性规范的概率上界。我们提供了理论依据与算法实现，并在多个经典基准上验证了其有效性。
原文摘要 · Abstract (English)
We introduce for the first time a neural-certificate framework for continuous-time stochastic dynamical systems. Autonomous learning systems in the physical world demand continuous-time reasoning, yet existing learnable certificates for probabilistic verification assume discretization of the time continuum. Inspired by the success of training neural Lyapunov certificates for deterministic continuous-time systems and neural supermartingale certificates for stochastic discrete-time systems, we propose a framework that bridges the gap between continuous-time and probabilistic neural certification for dynamical systems under complex requirements. Our method combines machine learning and symbolic reasoning to produce formally certified bounds on the probabilities that a nonlinear system satisfies specifications of reachability, avoidance, and persistence. We present both the theoretical justification and the algorithmic implementation of our framework and showcase its efficacy on popular benchmarks.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。