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

TL;DR

This paper addresses falsification of cyber-physical systems by learning their dynamics with neural ODEs, enriching the model with prior structure, and translating the learned dynamics into an interpretable symbolic form. It then casts falsification as an optimal-control problem over the symbolic surrogate, using differentiable STL robustness to guide trajectory optimization, and validates counterexamples on the true SUT. The approach, FalConN, demonstrates substantially fewer required experiments on ARCH-COMP 2024 benchmarks compared to dynamics-agnostic methods, while maintaining robust verification through SUT validation. The work highlights the practical impact of combining continuous-time neural modeling, symbolic distillation, and gradient-based optimization for efficient and explainable falsification in complex CPS.

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.

Figures (5)

• Figure 1: The SUT is approximated using neural surrogates with every new trajectory available, before being distilled into a symbolic representation. Counterexamples are computed using optimal control of the symbolic surrogate but must always be verified on the SUT to avoid spurious counterexamples.
• Figure 2: Simulation of neural ODE surrogate trained on estimation data in the interval $t\in [0, 10]$ and extrapolated simulation on unseen data $t \in [10, 20]$. The trajectory is simulated from the NN-controller benchmark example khandait2024arch.
• Figure 3: Blue points indicate the MSE trajectory loss $\mathbf{L_{traj}}$, computed by simulating each candidate model along trajectories in $\mathcal{D}$. Red points represent the MSE loss in dynamics. Notably, a candidate model that minimizes the dynamics error in the sampled points does not necessarily achieve minimal error when used in trajectory simulation.
• Figure 4: Synthesized counterexample together with the corresponding SUT trajectory, symbolic and neural surrogates. The resulting SUT robustness is -2.014 and the robustness from the optimal control problem is -2.13.
• Figure 5: Results from two independent falsification executions per specification, using our framework. The SUT (blue) is executed using the candidate counterexample from the optimal control problem (red). The neural surrogate (yellow) is plotted for comparison. All results show a falsifying trace except the bottom leftmost. For specifications NN and NN$_{\beta = 0.04}$, the violation is achieved by frequently altering the reference value, preventing a convergence of the position to the reference.

Theorems & Definitions (4)

• definition 1: trace
• definition 2: Signal Temporal Logic maler2004
• definition 3: STL Semantics
• definition 4: Robustness Semantics