Learning Lyapunov Functions for Piecewise Affine Systems with Neural Network Controllers

We propose an iterative method for Lyapunov-based stability analysis of piecewise affine dynamical systems in feedback with piecewise affine neural network controllers. In each iteration, a learner uses a collection of samples of the closed-loop system to propose a Lyapunov function candidate by solving a convex program. The learner then queries a verifier, which then solves a mixed-integer program to either validate the proposed Lyapunov function candidate or reject it with a counterexample, i.e., a state where the stability condition fails. We design the learner and the verifier based on the analytic center cutting-plane method (ACCPM), in which the verifier acts as the cutting-plane oracle to refine the set of Lyapunov function candidates. We show that the overall algorithm terminates in a finite number of iterations. We demonstrate the utility of the proposed method in searching for quadratic and piecewise quadratic Lyapunov functions.