Data-Driven Formal Methods for Complex Dynamical Systems: A Survey

What the math gives to ML

The survey identifies data-driven formal verification mechanisms that construct finite abstractions, functional certificates, and compositional guarantees from finite trajectory data rather than an explicit dynamical model. The most transferable mechanism is an interval Markov decision process (IMDP): partition a neural hidden-state space, estimate transition probabilities from data, attach statistically valid confidence intervals, and verify properties using worst-case Bellman recursion. This can turn an RNN, world model, or neural controller into a formally monitored finite-state dynamical system with an explicit confidence level and a measurable certificate boundary. The strongest initial experiment is to train an RNN together with an IMDP safety constraint and test whether certified reachability improves monotonically as transition-count uncertainty shrinks.