Formal Synthesis of Safe Kolmogorov-Arnold Network Controllers with Barrier Certificates

Formal Synthesis of Safe Kolmogorov-Arnold Network Controllers with Barrier Certificates

Xiongqi Zhang, Ning Lv, Wang Lin, Zuohua Ding

Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence
Main Track. Pages 302-310. https://doi.org/10.24963/ijcai.2025/35

Control barrier certificate generation is an efficient and powerful technique for the safe control of cyber-physical systems. Feed-forward neural networks (FNNs) are commonly used to synthesize control barrier certificates and safe controllers, but they struggle to effectively address the challenges posed by high-dimensional complex systems. In this paper, we propose a novel method for generating control barrier certificates and controllers using Kolmogorov-Arnold Networks (KANs). Specifically, it utilizes KANs to replace FNNs as the template of control barrier certificates and contrllers. Since KAN has learnable activation functions, it can efficiently improve the representation power. Then, it leverages the pruning and symbolization properties of KANs, which significantly simplify the network structure, allowing for more efficient formal verification of the simplified candidate KAN control barrier certificates and controllers using Satisfiability Modulo Theories. We implement the tool KAN4CBC, and evaluate its performance over a set of benchmarks. The experimental results demonstrate that our method addresses the issues of system dimension expansion and improved solution efficiency.
Keywords:
Agent-based and Multi-agent Systems: MAS: Formal verification, validation and synthesis
Multidisciplinary Topics and Applications: MTA: Software engineering