用自编码器降维后在低维空间验证高维动态系统，保证结果可映射回原系统。
Verification of Unknown Dynamical Systems via Autoencoder Latent Space
- 通过凸自编码器将高维系统降维，用核方法学习低维动力学
- 构建的抽象模型能覆盖原始系统的全部真实行为
- 适用于神经网络控制的高维系统，验证效率大幅提升
形式化验证为证明动态系统满足规范提供了强大框架，但在高维场景下面临可扩展性挑战，因常依赖随维度指数增长的状态空间离散化。基于学习的降维方法，如神经网络和自编码器，展现出缓解此问题的潜力。然而，如何确保低维空间验证结果的正确性仍是开放问题。本文提出一种形式化方法：通过凸自编码器降低系统维度，并利用核方法在潜在空间中学习动力学。随后，从学习到的模型构建有限抽象，确保其包含原始系统的全部真实行为。我们证明了潜在空间中的验证结果可映射回原系统。在多个系统上进行了验证，包括一个由神经网络控制的26维系统，展示了显著的可扩展性提升。
原文摘要 · Abstract (English)
Formal verification provides a powerful framework for proving that dynamical systems satisfy their specifications. However, these techniques face scalability challenges in high-dimensional settings, as they often rely on state-space discretization which grows exponentially with dimension. Learning-based approaches to dimensionality reduction, utilizing neural networks and autoencoders, have shown great potential to alleviate this problem. However, ensuring correctness of latent space verification results remains an open question. In this work, we provide a formal approach to reduce the dimensionality of systems via convex autoencoders and learn the dynamics in the latent space through a kernel-based method. We then construct a finite abstraction from the learned model in the latent space and guarantee that the abstraction contains the true behaviors of the original system. We show that the verification results in the latent space can be mapped back to the original system. Finally, we demonstrate the approach on multiple systems, including a 26D system controlled by a neural network, showing significant scalability improvements.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。