Research map / Learning theory and algorithms / Combinatorial and search optimization
Learning-enabled Polynomial Lyapunov Function Synthesis via High-Accuracy Counterexample-Guided Framework
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes SynNLF, a counterexample-guided loop that trains polynomial-expansion neural networks to fit Lyapunov candidates and verifies them via SOS/LMI feasibility, using worst-case minimum-volume ellipsoid counterexample sampling.
Problem
Synthesizing valid Lyapunov functions for nonlinear dynamical systems: template-based SOS methods need expert-chosen shapes, while neural Lyapunov functions built on Square networks with SMT verification generalize poorly and scale badly.
Approach
Replace Square activations with polynomial-expansion network modes (Mul, Ski, affine) so the learned network is directly a polynomial, verify it with Putinar-style SOS relaxation as an LMI feasibility problem, and generate counterexamples from a worst-case point plus a minimum-volume ellipsoid rather than random δ-ball sampling.
Key results
- SynNLF successfully handles all 20 benchmarks, whereas FOSSIL 1.0 and FOSSIL 2.0 find Lyapunov functions for 10 and 12 respectively.
- On the 6 benchmarks solved by all of SynNLF, FOSSIL 1.0 and FOSSIL 2.0, SynNLF takes on average 0.49 s versus 2.32 s for FOSSIL 2.0 (about 4.73x faster).
- SOSTOOLS succeeds on only 9 of the 20 cases, while SynNLF succeeds on all 20.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use SynNLF instead of Square-network SMT-based synthesis | Polynomial Lyapunov function synthesis · 6 examples handled by SynNLF, FOSSIL 1.0, and FOSSIL 2.0 | runtime (s): 0.49 seconds; 2.32 seconds; about 4.73 times faster | Helped |
| Use SynNLF instead of FOSSIL 1.0 | Polynomial Lyapunov function synthesis · 6 examples handled by SynNLF, FOSSIL 1.0, and FOSSIL 2.0 | runtime (s): 0.49 seconds; approximately 3.44 seconds | Helped |
| Use SynNLF instead of FOSSIL 1.0 and FOSSIL 2.0 | Polynomial Lyapunov function synthesis · 20 benchmark examples | successful Lyapunov function synthesis: 20; 10, 12 | Helped |
Surprising findings
- The SOS numerical toolbox SOSTOOLS is often faster than the learning-based approach on most examples, though SynNLF succeeds more often.
Limitations
- Neural V(x) synthesis lacks termination guarantees, so a 20-iteration cap and 60-second validation limit were imposed.
- SOSTOOLS is often faster than the learning-based pipeline on most benchmarks.
- Results are limited to small systems (mostly 2-3 state variables, up to 6).
Experimental setup
Datasets: Benchmark nonlinear dynamical systems (20 examples from prior literature, e.g., Van der Pol oscillator)
Benchmarks: 20 nonlinear system benchmarks (C1-C20) from prior literature
Metrics: success rate (number of systems solved) total time Te iteration count
Baselines: FOSSIL 1.0 FOSSIL 2.0 SOSTOOLS
Builds on: Square neural Lyapunov functions (FOSSIL) Pi-Nets Putinar Positivstellensatz CEGIS SOSTOOLS
Closest papers by meaning
- Analytical Lyapunov Function Discovery: An RL-based Generative Approach (ICML 2025 · similarity 0.89)
- Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformers (NeurIPS 2024 · similarity 0.88)
- Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation (ICML 2024 · similarity 0.88)
- Stability Analysis of Switched Linear Systems with Neural Lyapunov Functions (AAAI 2024 · similarity 0.87)
- Two‑Stage Learning of Stabilizing Neural Controllers via Zubov Sampling and Iterative Domain Expansion (NeurIPS 2025 · similarity 0.85)
- Certifying Stability of Reinforcement Learning Policies using Generalized Lyapunov Functions (NeurIPS 2025 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.