Synthesizing Local Control Barrier Functions for Hybrid Systems with LLM-Assisted search

A control barrier function (CBF) certifies that a controller can keep a system within a set of safe states. Manually constructing a CBF for a given system often requires intuition about the function's structure and parameters and is challenging in general. For hybrid systems with mode switching, a single barrier for all modes may be overly conservative. Using per-mode local barriers can reduce this conservatism, but they introduce an additional constraint that at every mode switch, a safe state must remain safe in the next mode. We propose a framework to synthesize per-mode local CBFs satisfying the mode-switching safety constraint. In our framework, a large language model proposes and refines candidate barriers based on feedback from a satisfiability solver checking the conditions for certification. We present case studies in which the framework successfully synthesizes per-mode CBFs. In each case study, the solver proves that the synthesized functions satisfy both the CBF conditions for each mode and the safety constraint at every mode switch. The proposed framework succeeds even when a naively-prompted baseline without solver feedback fails to produce any certified CBFs.