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

摘要

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.