Formally Stable and Interpretable Genetic Programming for Control

Kurzfassung

Genetic programming can produce explicit symbolic control laws, but good performance on simulated trajectories does not establish stability over a continuous region of the state space. This work introduces Control-Lyapunov-Function Genetic Programming (CLF-GP), an extension of Inclusive Genetic Programming (IGP) in which each individual carries both a controller and a candidate Lyapunov function. The candidate follows a standard sum-of-squares structure, so it is positive definite by construction and the search only has to satisfy the decrease condition. This condition is checked on sampled states away from the equilibrium and through a matrix inequality on the linearised closed loop near it. The fitness combines trajectory cost with the size of the certified sublevel set, and counterexamples returned by a falsifier during evolution are fed back into it. The final candidate is then verified with a satisfiability modulo theories (SMT) solver. In sixteen independent runs on a cart-pole benchmark, eleven certificates were proved, two remained undecided within the time budget, two were refuted by dense sampling and one could not be verified. That last candidate had passed two million sampled checks, so dense sampling alone would have accepted a certificate that the solver could not prove.The interpretability of the evolved laws was scored separately by a large language model, whose validation showed consistent scores for clearly readable and clearly opaque expressions but sensitivity to gain changes in between. In most runs the certified region did not contain the nominal initial state, and enlarging it without degrading trajectory cost is the main open problem, together with the inclusion of interpretability in the evolutionary pipeline.