SEVA-Lyap: Solver-Aware Data Evolution and Verification-Guided Test-Time Adaptation for Symbolic Lyapunov Function Discovery

Lyapunov functions provide fundamental certificates for the stability of dynamical systems, yet discovering explicit symbolic Lyapunov functions remains a long-standing computational challenge due to the vast search space and strict mathematical constraints. Recently, symbolic transformers have advanced this direction by formulating Lyapunov discovery as a sequence-to-sequence translation task, directly predicting interpretable Lyapunov functions from system dynamics. Despite this pioneering advance, these models face two critical bottlenecks: they rely on static synthetic datasets fixed prior to training, and they lack mechanisms to adapt at test time. Consequently, rare regions of the system distribution can remain underrepresented, making novel or hard systems difficult to solve. To address these limitations, we introduce SEVA-Lyap, a unified framework integrating solver-aware data evolution with verification-guided test-time adaptation. During training, SEVA-Lyap continuously evolves verified examples around the weaknesses of the current solver, creating a progressively challenging curriculum that strengthens reusable symbolic solving capability. At inference, SEVA-Lyap allocates additional test-time compute through targeted risk-seeking adaptation when direct prediction fails. Extensive evaluations demonstrate that SEVA-Lyap raises system-level verification success from 70.75% to 92.00% on polynomial systems and from 60.50% to 74.50% on non-polynomial systems, while reliably solving representative challenging dynamics and demonstrating notable transferability. Anonymous code and data are available at https://anonymous.4open.science/r/SEVA-review-DBD6-0921.