Learning-enabled Polynomial Lyapunov Function Synthesis via High-Accuracy Counterexample-Guided Framework
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions
We investigate the formal synthesis of global polynomial Lyapunov functions for polynomial vector fields. We establish that a sign-definite polynomial must satisfy specific algebraic constraints, which we leverage to dev…
Design SynthesisvalidAutomated and Sound Synthesis of Lyapunov Functions with SMT Solvers
In this paper we employ SMT solvers to soundly synthesise Lyapunov functions that assert the stability of a given dynamical model. The search for a Lyapunov function is framed as the satisfiability of a second-order logi…
Formal Synthesis of Lyapunov Neural Networks
We propose an automatic and formally sound method for synthesising Lyapunov functions for the asymptotic stability of autonomous non-linear systems. Traditional methods are either analytical and require manual effort or …
Polynomial Lyapunov Functions and Invariant Sets from a New Hierarchy of Quadratic Lyapunov Functions for LTV Systems
We introduce a new class of quadratic functions based on a hierarchy of linear time-varying (LTV) dynamical systems. These quadratic functions in the higher order space can be also seen as a non-homogeneous polynomial Ly…
Koopman-Based Neural Lyapunov Functions for General Attractors
Koopman spectral theory has grown in the past decade as a powerful tool for dynamical systems analysis and control. In this paper, we show how recent data-driven techniques for estimating Koopman-Invariant subspaces with…