Formal Synthesis of Safe Kolmogorov-Arnold Network Controllers with Barrier Certificates
Xiongqi Zhang, Ning Lv, Wang Lin, Zuohua Ding
Abstract
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.
BibTeX
@inproceedings{ijcai2025_formalsynthesiso,
title = {Formal Synthesis of Safe Kolmogorov-Arnold Network Controllers with Barrier Certificates},
author = {Xiongqi Zhang and Ning Lv and Wang Lin and Zuohua Ding},
booktitle = {IJCAI 2025},
year = {2025}
}