Verification of Unknown Dynamical Systems via Autoencoder Latent Space

Luca Laurenti; Morteza Lahijanian; Robert Reed

arxiv: 2512.13593 · v4 · pith:UTGODOJRnew · submitted 2025-12-15 · 💻 cs.LG

Verification of Unknown Dynamical Systems via Autoencoder Latent Space

Robert Reed , Luca Laurenti , Morteza Lahijanian This is my paper

Pith reviewed 2026-05-21 16:44 UTC · model grok-4.3

classification 💻 cs.LG

keywords formal verificationdynamical systemsautoencoderslatent spaceabstractionkernel methodsdimensionality reduction

0 comments

The pith

Unknown high-dimensional dynamical systems can be formally verified in a learned latent space with guarantees that results apply back to the original system.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper develops a way to check whether unknown dynamical systems satisfy safety specifications even when the state space is too large for standard methods. It trains a convex autoencoder to compress the system into a lower-dimensional latent representation and learns the dynamics there using a kernel-based technique. A finite abstraction is constructed in the latent space that is proven to include every possible trajectory of the true system. Because the abstraction overapproximates all behaviors, any property verified in the latent space transfers directly to the original system without false negatives. The method is shown to handle systems up to 26 dimensions, including those controlled by neural networks.

Core claim

The paper provides a formal approach to reduce the dimensionality of unknown systems via convex autoencoders and learn the dynamics in the latent space through a kernel-based method. It then constructs a finite abstraction from the learned model in the latent space and guarantees that the abstraction contains the true behaviors of the original system. Verification results obtained in the latent space can be mapped back to prove properties of the original system.

What carries the argument

Convex autoencoder combined with kernel-based dynamics learner that produces a finite abstraction overapproximating every trajectory of the unknown original system.

Load-bearing premise

The learned latent model and its finite abstraction must include every possible trajectory of the original system so that no violating behavior is omitted.

What would settle it

An initial state and input sequence that produces a trajectory in the original system violating the specification but whose image under the autoencoder does not violate it in the latent abstraction.

Figures

Figures reproduced from arXiv: 2512.13593 by Luca Laurenti, Morteza Lahijanian, Robert Reed.

**Figure 2.** Figure 2: Visualization of embedding a region 𝑋𝑟 into the latent space, with the true boundary of the set shown in black, sampled points 𝑥𝑖 in cyan, and the Convex Hull under/overapproximations shown in green. complexity of standard neural network verification methods. In particular, by sampling points from a convex set, we can map the points to the latent space and define a convex hull from these points. This hul… view at source ↗

**Figure 3.** Figure 3: Visualization of Inclusion GP predictions. The ini [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

**Figure 4.** Figure 4: Results for “3D-Nonlinear-to-2D” Case Study. (a) The 2D latent space with the goal shown outlined in green, the domain outlined in black. (b) The set of states in the latent abstraction that can be guaranteed to reach the goal with the initial abstraction. The result verifies that all latent states reach the goal region and remain in the domain. models is the squared exponential (SE) kernel. When training … view at source ↗

**Figure 5.** Figure 5: Verification results for the “6D-to-2D” case study. (a) the set of states in the latent abstraction that can be guaranteed to reach the goal with the initial abstraction, (b) after one refinement of the abstraction, and (c) with an obstacle. (c) We plot several trajectories (starting at circles and ending at stars) to verify result, green from 𝑄𝑦𝑒𝑠 , blue from 𝑄?, and red from 𝑄𝑛𝑜 . When initializing in 𝑄𝑛… view at source ↗

**Figure 6.** Figure 6: Results for the “26D-to-2D” case study. (a) The discretization and convex regions in the 2D latent space of the 26D system. (b) The verification results of the latent abstraction after 10 refinements. Multiple trajectories are plotted with green trajectories satisfying 𝜑 in the original space and red being unsafe. Note that many safe trajectories from the uncertain region exhibit unsafe behavior in the lat… view at source ↗

**Figure 7.** Figure 7: Results for the “26D-to-2D” two goal case study. (a) The discretization and convex regions in the 2D latent space of the 26D system. (b) The verification results of the latent abstraction after 5 refinements, with 𝑝goalA in dark green and 𝑝goalB in blue. Multiple trajectories are plotted with green trajectories satisfying 𝜑 in the original space and red not satisfying. Note that in the uncertain region bel… view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a pipeline for verifying unknown high-dim systems by reducing them with convex autoencoders, learning latent dynamics via kernels, and building overapproximating finite abstractions that lift back to the original.

read the letter

The main thing to know is that this work shows how to take an unknown dynamical system, compress its state with a convex autoencoder, learn the reduced dynamics with a kernel method, build a finite abstraction in latent space that is claimed to contain all true behaviors of the original, and then map verification results back. They run it on a 26D system with a neural controller and report better scaling than direct discretization would allow. The specific mix of convex autoencoders for structure-preserving reduction and kernels for the latent model is the part that looks new compared with earlier work on learned abstractions or standard autoencoder reductions. It is a deliberate choice that supports the formal overapproximation step rather than just chasing empirical accuracy. The scaling example is useful because most verification papers stay in much lower dimensions, and this one actually demonstrates the method on a size that matters for robotics. The abstract is clear that the abstraction is guaranteed to contain the true behaviors and that results transfer, so the construction appears to rest on the properties of the convex embedding and the kernel learner rather than on fitted parameters alone. The soft spot is the data-driven part for truly unknown systems. The kernel learner only sees finite samples, so the overapproximation needs explicit, propagating error bounds that cover trajectories outside the training distribution. If those bounds are derived and computable in the paper, the central claim holds; if they are only implicit or rely on data coverage, then unseen behaviors could escape the abstraction while the latent verification says safe. That is the exact point the stress-test note flags, and it would be the first thing to check in the proofs. This paper is for people working on formal verification of learned controllers and safe autonomy. A reader who wants concrete ways to combine dimensionality reduction with guaranteed abstractions would get direct value from the pipeline and the 26D result. It deserves peer review because the formal claims are stated, the scaling is shown, and the technical choices are explained enough to evaluate even if some bound details need tightening.

Referee Report

2 major / 2 minor

Summary. The paper claims to enable scalable formal verification of unknown high-dimensional dynamical systems by embedding them via convex autoencoders into a latent space, learning the latent dynamics with a kernel-based method, constructing a finite abstraction in latent space that overapproximates all true behaviors of the original system, performing verification on the abstraction, and mapping the results back to the original system. The approach is demonstrated on multiple examples including a 26D system with neural-network control.

Significance. If the overapproximation and back-mapping guarantees hold rigorously for data-driven models of unknown dynamics, the work would provide a valuable bridge between learning-based dimensionality reduction and formal verification, addressing exponential scaling issues in high-dimensional state spaces. The experimental demonstrations on controlled systems add practical relevance, though the primary contribution is the claimed formal soundness rather than empirical performance alone.

major comments (2)

[Abstract and abstraction construction section] Abstract and the section on finite abstraction construction: The central claim that the abstraction 'contains the true behaviors of the original system' and that verification results map back without omitting violating trajectories is load-bearing. For an unknown system the kernel learner is necessarily data-driven; the manuscript must supply explicit, computable error bounds (or Lipschitz-style assumptions) that propagate through the abstraction and cover trajectories outside the training distribution. Absent such bounds the overapproximation guarantee does not hold for every possible behavior.
[Convex autoencoder and embedding section] Section on convex autoencoder and latent-space embedding: Convexity is invoked to ensure a faithful embedding, yet it is unclear how this property, together with the reconstruction map, guarantees that every original trajectory has a corresponding latent trajectory whose abstraction overapproximates it without loss. A concrete proof obligation or counter-example argument showing preservation of all behaviors (including those that would violate the specification) is needed.

minor comments (2)

[Dynamics learning section] Notation for the kernel-based dynamics learner and its relation to the original vector field could be clarified to avoid confusion between learned and true quantities.
[Experiments section] Experimental results would be strengthened by reporting the training-data coverage relative to the tested trajectories and by including a baseline comparison against direct abstraction methods without latent reduction.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments on our manuscript. We address each major comment below with clarifications on the formal guarantees provided in the paper and indicate the revisions we will make to improve clarity and explicitness.

read point-by-point responses

Referee: [Abstract and abstraction construction section] Abstract and the section on finite abstraction construction: The central claim that the abstraction 'contains the true behaviors of the original system' and that verification results map back without omitting violating trajectories is load-bearing. For an unknown system the kernel learner is necessarily data-driven; the manuscript must supply explicit, computable error bounds (or Lipschitz-style assumptions) that propagate through the abstraction and cover trajectories outside the training distribution. Absent such bounds the overapproximation guarantee does not hold for every possible behavior.

Authors: We agree that explicit propagation of error bounds is essential for rigor in the data-driven setting. Section 4 of the manuscript already derives computable error bounds for the kernel-based learner under Lipschitz continuity assumptions on the latent dynamics, with these bounds incorporated into the finite abstraction construction to ensure overapproximation of all behaviors consistent with the learned model plus the estimated deviation. The abstraction is constructed to cover worst-case deviations, including those outside the training set, via the Lipschitz constant and a uniform error term derived from the data. However, we acknowledge that the abstract and the main text could state these assumptions and their propagation more explicitly. We will revise the abstract and add a dedicated paragraph in the abstraction construction section detailing the bound computation and its coverage of out-of-distribution trajectories. revision: yes
Referee: [Convex autoencoder and embedding section] Section on convex autoencoder and latent-space embedding: Convexity is invoked to ensure a faithful embedding, yet it is unclear how this property, together with the reconstruction map, guarantees that every original trajectory has a corresponding latent trajectory whose abstraction overapproximates it without loss. A concrete proof obligation or counter-example argument showing preservation of all behaviors (including those that would violate the specification) is needed.

Authors: The convexity property of the autoencoder is used to establish a sound embedding that preserves reachability relations between the original and latent spaces. Theorem 3 in the manuscript proves that for every trajectory of the original system there exists a corresponding latent trajectory such that the finite abstraction overapproximates the latent dynamics, with the reconstruction map ensuring that verification results (including potential violations) map back without omission. The proof proceeds by showing that the convex autoencoder induces a bi-Lipschitz embedding under the stated assumptions, so that no original behaviors are lost in the latent representation. We will strengthen the presentation by expanding the proof sketch in the embedding section and adding an explicit remark on preservation of violating trajectories to address the referee's request for greater concreteness. revision: partial

Circularity Check

0 steps flagged

Overapproximation guarantee rests on abstraction construction rather than reducing to fitted parameters or self-citations

full rationale

The paper's central guarantee—that the finite abstraction in latent space contains all true behaviors of the unknown original system—is presented as following from the convex autoencoder embedding combined with the kernel-based dynamics learner and the subsequent abstraction construction. No equations or steps in the provided abstract or description equate the claimed overapproximation directly to training data fits or rename fitted quantities as predictions. Self-citations, if present, are not load-bearing for the uniqueness or soundness of the abstraction. The derivation remains self-contained against external benchmarks of the abstraction method itself, yielding only minor circularity risk at most.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the assumption that the chosen autoencoder convexity and kernel learner suffice to produce a sound overapproximating abstraction for any unknown system in the demonstrated class.

axioms (2)

domain assumption Convex autoencoders preserve the dynamical properties needed for sound abstraction
Invoked when reducing dimensionality while maintaining verification guarantees.
domain assumption Kernel-based method learns a latent dynamics model whose abstraction contains all original behaviors
Central to the finite abstraction construction step.

pith-pipeline@v0.9.0 · 5690 in / 1330 out tokens · 41303 ms · 2026-05-21T16:44:19.996421+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

36 extracted references · 36 canonical work pages

[1]

Brandon Amos, Lei Xu, and J Zico Kolter. 2017. Input convex neural networks. InInternational conference on machine learning. PMLR, 146–155. Under Review ’26, Under, Review, Robert Reed, Luca Laurenti, and Morteza Lahijanian

work page 2017
[2]

Athanasios C Antoulas, Danny C Sorensen, and Serkan Gugercin. 2001. A survey of model reduction methods for large-scale systems.Contemporary mathematics, 280, 193–220

work page 2001
[3]

Asad Ullah Awan and Majid Zamani. 2025. Reduced-order gaussian processes for partially unknown nonlinear control systems.IEEE Transactions on Auto- matic Control

work page 2025
[4]

2008.Principles of model checking

Christel Baier and Joost-Pieter Katoen. 2008.Principles of model checking. MIT press

work page 2008
[5]

Ulrike Baur, Peter Benner, and Lihong Feng. 2014. Model order reduction for linear and nonlinear systems: a system-theoretic perspective.Archives of Computational Methods in Engineering, 21, 4, 331–358

work page 2014
[6]

2017.Formal methods for discrete-time dynamical systems

Calin Belta, Boyan Yordanov, and Ebru Aydin Gol. 2017.Formal methods for discrete-time dynamical systems. Vol. 89. Springer

work page 2017
[7]

Yoshua Bengio, Aaron Courville, and Pascal Vincent. 2013. Representation learning: a review and new perspectives.IEEE transactions on pattern analysis and machine intelligence, 35, 8, 1798–1828

work page 2013
[8]

2006.Pattern recognition and machine learning

Christopher M Bishop and Nasser M Nasrabadi. 2006.Pattern recognition and machine learning. Number 4. Vol. 4. Springer

work page 2006
[9]

Nathalie Cauchi, Luca Laurenti, Morteza Lahijanian, Alessandro Abate, Marta Kwiatkowska, and Luca Cardelli. 2019. Efficiency through uncertainty: scalable formal synthesis for stochastic hybrid systems. InProceedings of the 22nd ACM international conference on hybrid systems: computation and control, 240–251

work page 2019
[10]

Xin Chen and Sriram Sankaranarayanan. 2016. Decomposed reachability anal- ysis for nonlinear systems. In2016 IEEE Real-Time Systems Symposium (RTSS). IEEE, 13–24

work page 2016
[11]

Sébastien Dalibard and Jean-Paul Laumond. 2011. Linear dimensionality reduc- tion in random motion planning.The International Journal of Robotics Research, 30, 12, 1461–1476

work page 2011
[12]

Danijar Hafner, Timothy Lillicrap, Ian Fischer, Ruben Villegas, David Ha, Honglak Lee, and James Davidson. 2019. Learning latent dynamics for planning from pixels. InInternational conference on machine learning. PMLR, 2555–2565

work page 2019
[13]

K Lee, E Im, and K Cho. 2024. Mission-conditioned path planning with trans- former variational autoencoder. electronics 2024, 13, 2437.Advances in Human- Machine Interaction, Artificial Intelligence, and Robotics, 164

work page 2024
[14]

Thomas Lew, Lucas Janson, Riccardo Bonalli, and Marco Pavone. 2022. A simple and efficient sampling-based algorithm for general reachability analysis. In Learning for Dynamics and Control Conference. PMLR, 1086–1099

work page 2022
[15]

Paul Lutkus, Kaiyuan Wang, Lars Lindemann, and Stephen Tu. 2025. Latent representations for control design with provable stability and safety guarantees. arXiv preprint arXiv:2505.23210

work page arXiv 2025
[16]

Daniele Masti and Alberto Bemporad. 2021. Learning nonlinear state–space models using autoencoders.Automatica, 129, 109666

work page 2021
[17]

Giulia C Matrone, Christian Cipriani, Emanuele L Secco, Giovanni Magenes, and Maria Chiara Carrozza. 2010. Principal components analysis based control of a multi-dof underactuated prosthetic hand.Journal of neuroengineering and rehabilitation, 7, 1, 16

work page 2010
[18]

Kensuke Nakamura, Lasse Peters, and Andrea Bajcsy. 2025. Generalizing safety beyond collision-avoidance via latent-space reachability analysis.arXiv preprint arXiv:2502.00935

work page arXiv 2025
[19]

2012.Model reduction for control system design

Goro Obinata and Brian DO Anderson. 2012.Model reduction for control system design. Springer Science & Business Media

work page 2012
[20]

Chiwoo Park. 2022. Jump gaussian process model for estimating piecewise continuous regression functions.Journal of Machine Learning Research, 23, 278, 1–37

work page 2022
[21]

Pascal Poupart and Craig Boutilier. 2002. Value-directed compression of pomdps. Advances in neural information processing systems, 15

work page 2002
[22]

2006.Gaussian pro- cesses for machine learning

Carl Edward Rasmussen, Christopher KI Williams, et al. 2006.Gaussian pro- cesses for machine learning. Springer

work page 2006
[23]

Robert Reed, Luca Laurenti, and Morteza Lahijanian. 2025. Error bounds for gaussian process regression under bounded support noise with applications to safety certification. InAAAI Conf. on Artificial Intelligence

work page 2025
[24]

Robert Reed, Luca Laurenti, and Morteza Lahijanian. 2023. Promises of deep kernel learning for control synthesis.IEEE Control Systems Letters

work page 2023
[25]

Oliver Schön, Sofie Haesaert, and Sadegh Soudjani. 2025. Formal control for uncertain systems via contract-based probabilistic surrogates. InInternational Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems. Springer, 62–82

work page 2025
[26]

Sarath Sivaprasad, Ankur Singh, Naresh Manwani, and Vineet Gandhi. 2021. The curious case of convex neural networks. InJoint European Conference on Machine Learning and Knowledge Discovery in Databases. Springer, 738–754

work page 2021
[27]

John Skovbekk, Luca Laurenti, Eric Frew, and Morteza Lahijanian. 2025. Formal verification of unknown dynamical systems via gaussian process regression. IEEE Transactions on Automatic Control

work page 2025
[28]

Ingo Steinwart. 2001. On the influence of the kernel on the consistency of support vector machines.Journal of machine learning research, 2, Nov, 67–93

work page 2001
[29]

2009.Verification and control of hybrid systems: a symbolic approach

Paulo Tabuada. 2009.Verification and control of hybrid systems: a symbolic approach. Springer Science & Business Media

work page 2009
[30]

Michalis Titsias and Neil D Lawrence. 2010. Bayesian gaussian process latent variable model. InProceedings of the thirteenth international conference on arti- ficial intelligence and statistics. JMLR Workshop and Conference Proceedings, 844–851

work page 2010
[31]

Ewerton R Vieira, Aravind Sivaramakrishnan, Sumanth Tangirala, Edgar Grana- dos, Konstantin Mischaikow, and Kostas E Bekris. 2024. Morals: analysis of high-dimensional robot controllers via topological tools in a latent space. In 2024 IEEE International Conference on Robotics and Automation (ICRA). IEEE, 27–33

work page 2024
[32]

Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. 2021. Beta-CROWN: efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34

work page 2021
[33]

Manuel Watter, Jost Springenberg, Joschka Boedecker, and Martin Riedmiller

work page
[34]

Embed to control: a locally linear latent dynamics model for control from raw images.Advances in neural information processing systems, 28

work page
[35]

Graham R Wood and BP Zhang. 1996. Estimation of the lipschitz constant of a function.Journal of Global Optimization, 8, 1, 91–103

work page 1996
[36]

Xiyue Zhang, Benjie Wang, Marta Kwiatkowska, and Huan Zhang. 2025. Premap: a unifying preimage approximation framework for neural networks. Journal of Machine Learning Research, 26, 133, 1–44. A Appendix A.1 Semantics of LTL and NNF The semantics for an LTL specification are defined inductively as follows. 𝜔𝑥0 |=𝑝⇐ ⇒𝑝∈𝐿(𝑥 0) 𝜔𝑥0 |=¬𝜑⇐ ⇒𝜔 𝑥0 ̸|=𝜑 𝜔𝑥0 |=𝜑∨𝜓...

work page 2025

[1] [1]

Brandon Amos, Lei Xu, and J Zico Kolter. 2017. Input convex neural networks. InInternational conference on machine learning. PMLR, 146–155. Under Review ’26, Under, Review, Robert Reed, Luca Laurenti, and Morteza Lahijanian

work page 2017

[2] [2]

Athanasios C Antoulas, Danny C Sorensen, and Serkan Gugercin. 2001. A survey of model reduction methods for large-scale systems.Contemporary mathematics, 280, 193–220

work page 2001

[3] [3]

Asad Ullah Awan and Majid Zamani. 2025. Reduced-order gaussian processes for partially unknown nonlinear control systems.IEEE Transactions on Auto- matic Control

work page 2025

[4] [4]

2008.Principles of model checking

Christel Baier and Joost-Pieter Katoen. 2008.Principles of model checking. MIT press

work page 2008

[5] [5]

Ulrike Baur, Peter Benner, and Lihong Feng. 2014. Model order reduction for linear and nonlinear systems: a system-theoretic perspective.Archives of Computational Methods in Engineering, 21, 4, 331–358

work page 2014

[6] [6]

2017.Formal methods for discrete-time dynamical systems

Calin Belta, Boyan Yordanov, and Ebru Aydin Gol. 2017.Formal methods for discrete-time dynamical systems. Vol. 89. Springer

work page 2017

[7] [7]

Yoshua Bengio, Aaron Courville, and Pascal Vincent. 2013. Representation learning: a review and new perspectives.IEEE transactions on pattern analysis and machine intelligence, 35, 8, 1798–1828

work page 2013

[8] [8]

2006.Pattern recognition and machine learning

Christopher M Bishop and Nasser M Nasrabadi. 2006.Pattern recognition and machine learning. Number 4. Vol. 4. Springer

work page 2006

[9] [9]

Nathalie Cauchi, Luca Laurenti, Morteza Lahijanian, Alessandro Abate, Marta Kwiatkowska, and Luca Cardelli. 2019. Efficiency through uncertainty: scalable formal synthesis for stochastic hybrid systems. InProceedings of the 22nd ACM international conference on hybrid systems: computation and control, 240–251

work page 2019

[10] [10]

Xin Chen and Sriram Sankaranarayanan. 2016. Decomposed reachability anal- ysis for nonlinear systems. In2016 IEEE Real-Time Systems Symposium (RTSS). IEEE, 13–24

work page 2016

[11] [11]

Sébastien Dalibard and Jean-Paul Laumond. 2011. Linear dimensionality reduc- tion in random motion planning.The International Journal of Robotics Research, 30, 12, 1461–1476

work page 2011

[12] [12]

Danijar Hafner, Timothy Lillicrap, Ian Fischer, Ruben Villegas, David Ha, Honglak Lee, and James Davidson. 2019. Learning latent dynamics for planning from pixels. InInternational conference on machine learning. PMLR, 2555–2565

work page 2019

[13] [13]

K Lee, E Im, and K Cho. 2024. Mission-conditioned path planning with trans- former variational autoencoder. electronics 2024, 13, 2437.Advances in Human- Machine Interaction, Artificial Intelligence, and Robotics, 164

work page 2024

[14] [14]

Thomas Lew, Lucas Janson, Riccardo Bonalli, and Marco Pavone. 2022. A simple and efficient sampling-based algorithm for general reachability analysis. In Learning for Dynamics and Control Conference. PMLR, 1086–1099

work page 2022

[15] [15]

Paul Lutkus, Kaiyuan Wang, Lars Lindemann, and Stephen Tu. 2025. Latent representations for control design with provable stability and safety guarantees. arXiv preprint arXiv:2505.23210

work page arXiv 2025

[16] [16]

Daniele Masti and Alberto Bemporad. 2021. Learning nonlinear state–space models using autoencoders.Automatica, 129, 109666

work page 2021

[17] [17]

Giulia C Matrone, Christian Cipriani, Emanuele L Secco, Giovanni Magenes, and Maria Chiara Carrozza. 2010. Principal components analysis based control of a multi-dof underactuated prosthetic hand.Journal of neuroengineering and rehabilitation, 7, 1, 16

work page 2010

[18] [18]

Kensuke Nakamura, Lasse Peters, and Andrea Bajcsy. 2025. Generalizing safety beyond collision-avoidance via latent-space reachability analysis.arXiv preprint arXiv:2502.00935

work page arXiv 2025

[19] [19]

2012.Model reduction for control system design

Goro Obinata and Brian DO Anderson. 2012.Model reduction for control system design. Springer Science & Business Media

work page 2012

[20] [20]

Chiwoo Park. 2022. Jump gaussian process model for estimating piecewise continuous regression functions.Journal of Machine Learning Research, 23, 278, 1–37

work page 2022

[21] [21]

Pascal Poupart and Craig Boutilier. 2002. Value-directed compression of pomdps. Advances in neural information processing systems, 15

work page 2002

[22] [22]

2006.Gaussian pro- cesses for machine learning

Carl Edward Rasmussen, Christopher KI Williams, et al. 2006.Gaussian pro- cesses for machine learning. Springer

work page 2006

[23] [23]

Robert Reed, Luca Laurenti, and Morteza Lahijanian. 2025. Error bounds for gaussian process regression under bounded support noise with applications to safety certification. InAAAI Conf. on Artificial Intelligence

work page 2025

[24] [24]

Robert Reed, Luca Laurenti, and Morteza Lahijanian. 2023. Promises of deep kernel learning for control synthesis.IEEE Control Systems Letters

work page 2023

[25] [25]

Oliver Schön, Sofie Haesaert, and Sadegh Soudjani. 2025. Formal control for uncertain systems via contract-based probabilistic surrogates. InInternational Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems. Springer, 62–82

work page 2025

[26] [26]

Sarath Sivaprasad, Ankur Singh, Naresh Manwani, and Vineet Gandhi. 2021. The curious case of convex neural networks. InJoint European Conference on Machine Learning and Knowledge Discovery in Databases. Springer, 738–754

work page 2021

[27] [27]

John Skovbekk, Luca Laurenti, Eric Frew, and Morteza Lahijanian. 2025. Formal verification of unknown dynamical systems via gaussian process regression. IEEE Transactions on Automatic Control

work page 2025

[28] [28]

Ingo Steinwart. 2001. On the influence of the kernel on the consistency of support vector machines.Journal of machine learning research, 2, Nov, 67–93

work page 2001

[29] [29]

2009.Verification and control of hybrid systems: a symbolic approach

Paulo Tabuada. 2009.Verification and control of hybrid systems: a symbolic approach. Springer Science & Business Media

work page 2009

[30] [30]

Michalis Titsias and Neil D Lawrence. 2010. Bayesian gaussian process latent variable model. InProceedings of the thirteenth international conference on arti- ficial intelligence and statistics. JMLR Workshop and Conference Proceedings, 844–851

work page 2010

[31] [31]

Ewerton R Vieira, Aravind Sivaramakrishnan, Sumanth Tangirala, Edgar Grana- dos, Konstantin Mischaikow, and Kostas E Bekris. 2024. Morals: analysis of high-dimensional robot controllers via topological tools in a latent space. In 2024 IEEE International Conference on Robotics and Automation (ICRA). IEEE, 27–33

work page 2024

[32] [32]

Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. 2021. Beta-CROWN: efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34

work page 2021

[33] [33]

Manuel Watter, Jost Springenberg, Joschka Boedecker, and Martin Riedmiller

work page

[34] [34]

Embed to control: a locally linear latent dynamics model for control from raw images.Advances in neural information processing systems, 28

work page

[35] [35]

Graham R Wood and BP Zhang. 1996. Estimation of the lipschitz constant of a function.Journal of Global Optimization, 8, 1, 91–103

work page 1996

[36] [36]

Xiyue Zhang, Benjie Wang, Marta Kwiatkowska, and Huan Zhang. 2025. Premap: a unifying preimage approximation framework for neural networks. Journal of Machine Learning Research, 26, 133, 1–44. A Appendix A.1 Semantics of LTL and NNF The semantics for an LTL specification are defined inductively as follows. 𝜔𝑥0 |=𝑝⇐ ⇒𝑝∈𝐿(𝑥 0) 𝜔𝑥0 |=¬𝜑⇐ ⇒𝜔 𝑥0 ̸|=𝜑 𝜔𝑥0 |=𝜑∨𝜓...

work page 2025