An official website of the United States government
We present a two-stage approach for learning stability-certified neural controllers that achieves a reduction of up to ~95% in training time compared to the state-of-the-art baseline, which introduced monotonic neural Lyapunov architectures. Our method combines monotonic neural Lyapunov functions with fulfillment priority logic (FPL) to efficiently initialize controllers before formal verification. Traditional approaches for jointly learning controllers and neural Lyapunov functions require computationally expensive mixed-integer linear programming (MILP) or satisfiability modulo theory (SMT) solvers at each training iteration, often taking several hours to converge. We address this bottleneck by leveraging FPL to perform early joint initialization of the controller and Lyapunov networks. Building on the monotonic neural network architecture from the baseline, which guarantees non-negativity and a unique global minimum by construction, our method focuses on efficiently satisfying the remaining property of decreasing along trajectories. Existing works focus on maximizing the region of attraction/convergence of the learned controller. In contrast, leveraging FPL allows us to (1) increase learning efficiency substantially and (2) focus on complementary performance metrics, such as convergence rate and control effort minimization, thereby adding significant specification flexibility. In this paper, we encode an approximate Lyapunov-decrease condition in FPL to pre-train the controller and Lyapunov networks, then apply a MILP-based verification/refinement step. This decouples efficient learning from certificate enforcement and allows the FPL specification to include auxiliary objectives (e.g., convergence rate and control effort), whose influence persists through the final MILP pass. The resulting controllers converge rapidly while admitting formal Lyapunov certificates on standard nonlinear control benchmarks.
more »
« less
This content will become publicly available on May 1, 2027
Accelerating Lyapunov-Stable Neural Control using Fulfillment Priority Logic
We present a two-stage approach for learning stability-certified neural controllers that achieves a reduction of up to ∼95% in training time compared to the state-of-the-art baseline, which introduced monotonic neural Lyapunov architectures. Our method combines monotonic neural Lyapunov functions with fulfillment priority logic (FPL) to efficiently initialize controllers before formal verification. Traditional approaches for jointly learning controllers and neural Lyapunov functions require computationally expensive mixed-integer linear programming (MILP) or satisfiability modulo theory (SMT) solvers at each training iteration, often taking several hours to converge. We address this bottleneck by leveraging FPL to perform early joint initialization of the controller and Lyapunov networks. Building on the monotonic neural network architecture from the baseline, which guarantees non-negativity and a unique global minimum by construction, our method focuses on efficiently satisfying the remaining property of decreasing along trajectories. Existing works focus on maximizing the region of attraction/convergence of the learned controller. In contrast, leveraging FPL allows us to (1) increase learning efficiency substantially and (2) focus on complementary performance metrics, such as convergence rate and control effort minimization, thereby adding significant specification flexibility. In this paper, we encode an approximate Lyapunov-decrease condition in FPL to pre-train the controller and Lyapunov networks, then apply a MILP-based verification/refinement step. This decouples efficient learning from certificate enforcement and allows the FPL specification to include auxiliary objectives (e.g., convergence rate and control effort), whose influence persists through the final MILP pass. The resulting controllers converge rapidly while admitting formal Lyapunov certificates on standard nonlinear control benchmarks.
more »
« less
- Award ID(s):
- 2238476
- PAR ID:
- 10684886
- Publisher / Repository:
- In Proceedings of the 2026 American Control Conference (ACC 2026)
- Date Published:
- Format(s):
- Medium: X
- Location:
- New Orleans, LA, USA
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Despite advances in learning-based methods, finding valid Lyapunov functions for nonlinear dynamical systems remains challenging. Current neural network approaches face two main issues: challenges in scalable verification and limited interpretability. To address these, we propose an end-to-end framework using transformers to construct analytical Lyapunov functions (local), which simplifies formal verification, enhances interpretability, and provides valuable insights for control engineers. Our framework consists of a transformer-based trainer that generates candidate Lyapunov functions and a falsifier that verifies candidate expressions and refines the model via risk-seeking policy gradient. Unlike Alfarano et al. (2024), which utilizes pre-training and seeks global Lyapunov functions for low-dimensional systems, our model is trained from scratch via reinforcement learning (RL) and succeeds in finding local Lyapunov functions for high-dimensional and non-polynomial systems. Given the symbolic nature of the Lyapunov function candidates, we employ efficient optimization methods for falsification during training and formal verification tools for the final verification. We demonstrate the efficiency of our approach on a range of nonlinear dynamical systems with up to ten dimensions and show that it can discover Lyapunov functions not previously identified in the control literature. Full implementation is available on https://github.com/JieFeng-cse/Analytical-Lyapunov-Function-Discovery.more » « less
-
Certificate functions can be used to efficiently capture and prove various properties of a system or controller. Control barrier functions (CBFs) are certificate functions that define a region of forward-invariance, which makes them a natural choice to enforce a notion of “safety” for a system. However, synthesizing CBFs, especially in the case of complex systems with learning-enabled components, remains a challenge. Recent work achieves promising results by leveraging neural networks as function approximators to learn CBFs. However, a single CBF may not exist or be difficult to obtain for complex hybrid systems. To overcome this difficulty, this paper presents a framework to simultaneously learn simpler, time-varying control barrier functions (TV-CBFs) that are composable. We embed these neural certificates in a compositional framework based on assume-guarantee contracts. The resulting neural barrier contracts can then be combined by leveraging the rigorous contract algebra. Learning multiple, composable CBFs empowers the verification process (1) by simplifying the verification of complex systems via decomposition and (2) by broadening the expressivity in capturing complex systems and controllers. We illustrate the effectiveness of our approach on the verification of an aircraft’s automatic landing system and a quadrotor navigating an indoor environment.more » « less
-
Deep learning methods have been widely used in robotic applications, making learning-enabled control design for complex nonlinear systems a promising direction. Although deep reinforcement learning methods have demonstrated impressive empirical performance, they lack the stability guarantees that are important in safety-critical situations. One way to provide these guarantees is to learn Lyapunov certificates alongside control policies. There are three related problems: 1) verify that a given Lyapunov function candidate satisfies the conditions for a given controller on a region, 2) find a valid Lyapunov function and controller on a given region, and 3) find a valid Lyapunov function and a controller such that the region of attraction is as large as possible. Previous work has shown that if the dynamics are piecewise linear, it is possible to solve problem 1) and 2) by solving a Mixed-Integer Linear Program (MILP). In this work, we build upon this method by proposing a Lyapunov neural network that considers monotonicity over half spaces in different directions. We 1) propose a specific choice of Lyapunov function architecture that ensures non-negativity and a unique global minimum by construction, and 2) show that this can be leveraged to find the controller and Lyapunov certificates faster and with a larger valid region by maximizing the size of a square inscribed in a given level set. We apply our method to a 2D inverted pendulum, unicycle path following, a 3-D feedback system, and a 4-D cart pole system, and demonstrate it can shorten the training time by half compared to the baseline, as well as find a larger ROA.more » « less
-
null (Ed.)With the goal of moving towards implementation of increasingly dynamic behaviors on underactuated systems, this paper presents an optimization-based approach for solving full-body dynamics based controllers on underactuated bipedal robots. The primary focus of this paper is on the development of an alternative approach to the implementation of controllers utilizing control Lyapunov function based quadratic programs. This approach utilizes many of the desirable aspects from successful inverse dynamics based controllers in the literature, while also incorporating a variant of control Lyapunov functions that renders better convergence in the context of tracking outputs. The principal benefits of this formulation include a greater ability to add costs which regulate the resulting behavior of the robot. In addition, the model error-prone inertia matrix is used only once, in a non-inverted form. The result is a successful demonstration of the controller for walking in simulation, and applied on hardware in real-time for dynamic crouching.more » « less
