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

Polynomial Lyapunov function 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 V(x) offer flexibility but exhibit poor generalization yield from naive Square NNs. In this paper, we propose a novel learning-enabled polynomial V(x) synthesis approach, where an automated machine learning process guided by goal-oriented sampling to fit candidate 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 V(x) network via polynomial expansions, while the Verifier encodes learned candidates with SOS constraints to identify a real 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.