Combining Neural Networks and Symbolic Regression for Analytical Lyapunov Function Discovery

TL;DR

CoNSAL introduces a two-loop framework that learns a neural Lyapunov function and then distills it into an analytical form via symbolic regression, enabling rigorous stability certification for nonlinear dynamics. The outer loop uses root-based counterexample generation around $V(x)$ and $L_fV(x)$ to iteratively refine candidates, terminating when a valid analytical Lyapunov function is obtained. A compositional extension enables scalable certification for networked systems by combining local and pairwise Lyapunov components. Compared with SMT-based verification, CoNSAL achieves competitive or superior success rates with faster counterexample generation and yields interpretable, globally or locally valid Lyapunov functions. The approach is demonstrated on a spectrum of systems up to 6-D and is supported by public code, highlighting practical impact for safety-critical nonlinear control.

Abstract

We propose CoNSAL (Combining Neural networks and Symbolic regression for Analytical Lyapunov function) to construct analytical Lyapunov functions for nonlinear dynamic systems. This framework contains a neural Lyapunov function and a symbolic regression component, where symbolic regression is applied to distill the neural network to precise analytical forms. Our approach utilizes symbolic regression not only as a tool for translation but also as a means to uncover counterexamples. This procedure terminates when no counterexamples are found in the analytical formulation. Compared with previous results, CoNSAL directly produces an analytical form of the Lyapunov function with improved interpretability in both the learning process and the final results. We apply CoNSAL to 2-D inverted pendulum, path following, Van Der Pol Oscillator, 3-D trig dynamics, 4-D rotating wheel pendulum, 6-D 3-bus power system, and demonstrate that our algorithm successfully finds their valid Lyapunov functions. Code examples are available at https://github.com/HaohanZou/CoNSAL.

Figures (5)

• Figure 1: Diagram illustrating the proposed framework applied to an inverted pendulum. The analytical form (invalid intermediate result) enables root identification for both the candidate Lyapunov function and the Lie derivative. Counterexamples are sought around the roots. The process concludes when no counterexamples are detectable.
• Figure 2: Diagram illustrating the proposed compositional structure for a three-node network. Each subsystem's states are fed to the neural network $V_\theta(\cdot)$, and the connected subsystems' states are fed to $V_{\psi}(\cdot, \cdot)$. These neural networks are shared across edges and subsystems, and the joint Lyapunov function for the entire system is obtained by summation.
• Figure 3: Lie Derivative of the Neural Lyapunov Function under linear path following dynamics, updated with the proposed algorithm. Showing the result of the first two epochs.
• Figure 4: SMT Counter Examples, Roots, and Root finding Counter Examples Visualization using the same checkpoint at epoch 1 for Lie derivative of the neural Lyapunov functions under linear path-following dynamics. The same number of counterexamples are generated. The zoomed-in region shows the counterexamples from SMT solvers.
• Figure 5: Log-scaled Loss Convergence Comparison using loss \ref{['eq:loss']}. Only success trials are considered.

Theorems & Definitions (5)

• Definition 3.1: Dynamical systems
• Definition 3.2: Asymptotic stability
• Definition 3.3: Lie derivative
• Proposition 3.4: Lyapunov functions for asymptotic stability
• Remark 4.1