Zubov-Net: Anchored Neural Networks for Learning Maximal Lyapunov Functions with Formal Guarantees

Lyapunov functions are a central tool for certifying the stability of physical and engineered systems, yet constructing them remains a long-standing computational challenge. Neural networks can learn Lyapunov functions from data, but the learned functions rarely come with formal guarantees. We introduce Zubov-Net, a neural architecture whose outputs are guaranteed to be Lyapunov functions near the equilibrium and whose sublevel sets can cover any compact subset of the region of attraction (ROA). Zubov-Net multiplies a known local Lyapunov function, the anchor, by a learned positive correction. Because this design enforces the local Lyapunov conditions for every choice of network parameters, training only has to learn the global shape of the basin from trajectory data and a well-scaled residual of Zubov's equation. We prove a universal approximation theorem for anchored networks: they can approximate a maximal Lyapunov function arbitrarily well on each of its sublevel sets. Across a range of benchmarks with two to twenty state variables, the formally verified ROA estimates of Zubov-Net are consistently, and often substantially, larger than those of the baseline certificates.