Optimal Control-Based Falsification of Learnt Dynamics via Neural ODEs and Symbolic Regression

TL;DR

This paper introduces a novel falsification framework combining neural ODEs and symbolic regression to efficiently generate counterexamples for cyber-physical systems, significantly reducing the number of experiments needed.

Contribution

It integrates learned surrogate dynamics with optimal control and symbolic regression for fast, interpretable falsification of systems specified in STL.

Findings

Requires fewer experiments than traditional methods

Provides interpretable models via symbolic regression

Successfully validated on ARCH-COMP 2024 benchmarks

Abstract

We present a falsification framework that integrates learned surrogate dynamics with optimal control to efficiently generate counterexamples for cyber-physical systems specified in signal temporal logic (STL). The unknown system dynamics are identified using neural ODEs, while known a-priori structure is embedded directly into the model, reducing data requirements. The learned neural ODE is converted into an analytical form via symbolic regression, enabling fast and interpretable trajectory optimization. Falsification is cast as minimizing STL robustness over input trajectories; negative robustness yields candidate counterexamples, which are validated on the original system. Spurious traces are iteratively used to refine the surrogate, while true counterexamples are returned as final results. Experiments on ARCH-COMP 2024 benchmarks show that this method requires orders of magnitude fewer experiments of the system under test than optimization-based approaches that do not model system dynamics.