Learning-Enabled Polynomial Lyapunov Function Synthesis via High-Accuracy Counterexample-Guided Framework

Abstract

Polynomial Lyapunov function \mathcal V (x) provides mathematically rigorous that converts stability analysis into efficiently solvable optimization problem. Traditional numerical methods rely on user-defined templates, while emerging neural \mathcal V (x) offer flexibility but exhibit poor generalization yield from naive Square polynomial networks. In this paper, we propose a novel learning-enabled polynomial \mathcal V (x) synthesis approach, where a data-driven machine learning process guided by target-based sampling to fit candidate \mathcal V (x) which naturally compatible with the sum-of-squares (SOS) soundness verification. The framework is structured as an iterative loop between a Learner and a Verifier , where the Learner trains expressive polynomial \mathcal V (x) network via polynomial expansions, while the Verifier encodes learned candidates with SOS constraints to identify a real \mathcal V (x) by solving LMI feasibility test problems. The entire procedure is driven by a high-accuracy counterexample guidance technique to further enhance efficiency. Experimental results demonstrate that our approach outperforms both SMT-based polynomial neural Lyapunov function synthesis and traditional SOS method.