Abstract: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.
| Comments: | 25 pages, 6 figures, under review |
| Subjects: | Machine Learning (cs.LG) |
| Cite as: | arXiv:2512.13593 [cs.LG] |
| (or arXiv:2512.13593v4 [cs.LG] for this version) | |
| https://doi.org/10.48550/arXiv.2512.13593 arXiv-issued DOI via DataCite |
From: Robert Reed [view email]
[v1]
Mon, 15 Dec 2025 17:48:07 UTC (5,054 KB)
[v2]
Tue, 16 Dec 2025 16:58:02 UTC (5,054 KB)
[v3]
Mon, 9 Feb 2026 21:15:39 UTC (5,278 KB)
[v4]
Tue, 19 May 2026 18:12:40 UTC (2,714 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。