Control Lyapunov Functions

Also known as CLF

Latest papers

13 papers2 papers in the last four weeks, with none the four weeks before. 0.0% of all new papers.

LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification
Oct 21, 2026Zhipeng Cao, Peiyang Song, Nikolaus Vertovec +6Formal Verification Control Lyapunov Functions
Institute of Software, Chinese Academy of Sciences (CAS) · School of Advanced Interdisciplinary Sciences, University of Chinese Academy of Sciences · Language Technologies Institute, School of Computer Science, Carnegie Mellon University +5
A Rate Transfer Method: Convergence Rates in Stochastic Gradient Descent via Stochastic Calculus
Oct 13, 2026Neil WaltonControl Lyapunov Functions Stochastic Optimization Convergence
Durham University
Optimal Safety Control using High-Order Control Barrier Functions
Jul 19, 2026Neng Li, Zuodong Pan, Jiaxing Wang +2High-Order Control Barrier Functions Lyapunov-Based Control
Key Laboratory of Intelligent Control and Optimization for Industrial Equipment of Ministry of Education, Dalian University of Technology, Dalian 116024, China
Reachability Guarantees for Cart-Pole Swing-Up and Stabilization
Jun 26, 2026Mohamed Khalid M JaffarReachability Analysis Lyapunov-Based Control
Department of Aerospace Engineering University of Maryland, College Park, USA
Conflict-Aware Switching for CBF-CLF-Based Multi-Goal Navigation
Jun 19, 2026Rohan Walia, Kevin LeahyControl Lyapunov Functions Robot Navigation
Robotics Engineering Department, Worcester Polytechnic Institute, Worcester, MA 01609, USA
MARCH: Model-Assisted Reinforcement Learning for the Perceptive Control of Humanoids over Sparse Footholds
Jun 9, 2026Codrin Crismariu, Ryan K. CosnerControl Lyapunov Functions Humanoid Robot Locomotion
Department of Mechanical Engineering, Tufts University, Medford, MA, United States
Non-Asymptotic Convergence of Stochastic Iterative Algorithms: A Lyapunov Framework
May 29, 2026Zaiwei Chen, Siva Theja MaguluriControl Lyapunov Functions Lyapunov Stability
Purdue IE · Georgia Tech IE
Learned Lyapunov Shielding for Adaptive Control
May 7, 2026Giansalvo Cirrincione, Adriano FagioliniLyapunov-Based Control Safe RL
Laboratoire LTI, Université de Picardie Jules Verne, Amiens, France. · MIRPALab, Department of Engineering, University of Palermo, 90128 Palermo, Italy.
Stability of Control Lyapunov Function Guided Reinforcement Learning
May 3, 2026Zachary Olkin, William D. Compton, Aaron D. AmesRL Control Lyapunov Stability
The authors are with the Department of Control and Dynamical Systems at the California Institute of Technology.
Zero-Shot, Safe and Time-Efficient UAV Navigation via Potential-Based Reward Shaping, Control Lyapunov and Barrier Functions
May 3, 2026Ashik Abrar Naeem, Mohammad Ariful HaqueRL Control Control Lyapunov Functions
A Closed-Form CLF-CBF Controller for Whole-Body Continuum Soft Robot Collision Avoidance
Mar 19, 2026Kiwan Wong, Maximillian Stölzle, Wei Xiao +1Control Lyapunov Functions Continuum Robot Control
Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, MA 02139, USA · Robotics Engineering Department, Worcester Polytechnic Institute, Worcester, MA 01609, USA
Safety-Guaranteed Imitation Learning from Nonlinear Model Predictive Control for Spacecraft Close Proximity Operations
Mar 19, 2026Alexander Meinert, Niklas Baldauf, Peter Stadler +1Control Lyapunov Functions Imitation Learning
Space Applications Group, e:fs TechHub GmbH, Gaimersheim, Germany. · Faculty of Electrical Engineering and Information Technology, Ingolstadt University of Applied Sciences, Germany.
Safety-critical Control Under Partial Observability: Reach-Avoid POMDP meets Belief Space Control
Mar 11, 2026Matti Vahs, Joris Verhagen, Jana TumovaControl Lyapunov Functions Partially Observable Markov Decision Processes
Division of Robotics, Perception and Learning, KTH Royal Institute of Technology, Stockholm, Sweden · Digital Futures

Oct 21, 2026J/K move · Enter open · S save

LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification

Zhipeng Cao, Peiyang Song, Nikolaus Vertovec, Weiru Cui+5

Institute of Software, Chinese Academy of Sciences (CAS) · School of Advanced Interdisciplinary Sciences, University of Chinese Academy of Sciences · Language Technologies Institute, School of Computer Science, Carnegie Mellon University+5

Formal Verification Control Lyapunov Functions Large Language Model-Guided Theorem Proving

Open paper AskPDF arXiv

Lyapunov functions and barrier certificates give state-space guarantees of stability and safety, but synthesizing and verifying them---especially for nonlinear, high-dimensional systems---remains an open challenge. Existing pipelines verify candidates with numerical solvers (sum-of-squares programs), interval methods, or satisfiability-modulo-theories (SMT) solvers, which often require relaxations, are conservative, or scale poorly with model dimension and nonlinearity. These limitations have also shaped benchmark design: standard test suites are dominated by low-dimensional polynomial systems chosen to suit what solvers can handle rather than what engineering applications require. We address both sides of this challenge. First, we introduce DynaCertBench, a benchmark of 105 instances: 80 non-redundant systems curated from the literature, extended with high-dimensional and control-constrained variants and new nonlinearly coupled systems, comprehensively spanning stability, region-of-attraction, forward-invariance, and safety tasks. Second, we present LLM2Cert, an LLM-driven framework that synthesizes candidate certificates and verifies them against their proof obligations: each obligation is routed to an SMT solver or directly to the Lean Proof-Repair agent. On DynaCertBench, LLM2Cert verifies 81 of 105 instances (

77.1\%

), a

17.1

percentage point improvement over one-shot proposal without feedback. On the 81 fixed certificates, LLM2Cert verifies 22 that All-SMT leaves unresolved. Code and data are available at https://github.com/FormalCert-AI/llm2cert.