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

1 Introduction

Controller design and synthesis is a fundamental challenge in control theory, particularly for complex and nonlinear systems. With the development of deep learning, neural networks have become widely used in controlling various cyberphysical systems, such as unmanned aerial vehicles, autonomous vehicles, and smart transportation [Andrychowicz et al., 2020; Ding and Tomlin, 2010]. It is important to note that many of these systems are safety-critical, meaning the controller must ensure that the system never enter dangerous or undesirable states during operation. However, synthesizing safe controllers is inherently complex and presents a significant challenge.

∗Corresponding authors.

Control barrier certificate (CBC) generation is an efficient and powerful technique often used for the formal synthesis of safe controllers. The conditions of control barrier certificates impose certain constraints on the controllers. When a control barrier certificate is identified, it divides the model's state space into two regions. This division ensures that any system trajectory starting from a given initial set lies on one side of the control barrier certificate, and cannot reach a given unsafe set on the other side. Therefore, we formally prove the safety of controlled dynamical systems by constructing a control barrier certificate, the existence of which is sufficient to guarantee the safety of the controller.

Sum-of-squares (SOS) programming is a traditional method for synthesizing polynomial barrier certificates [Prajna, 2006; Legat et al., 2020]. But this method lacks scalability and expressiveness. Based on the universal approximation theorem [Leshno et al., 1993], neural networks have the capability to approximate any arbitrary function, making them suitable for representing barrier certificates. Zhao et al. [2020] first synthesized barrier certificates via neural network training and verification. FOSSIL [Abate et al., 2021] is a tool for the automated formal synthesis of barrier certificates, using neural networks as templates and Satisfiability Modulo Theories (SMT) solvers as verification tools. However, traditional feed-forward neural networks (FNNs) often use fixed activation functions, which can significantly impact the efficiency of synthesizing barrier certificates. Moreover, for controlled continuous dynamical systems, most methods tend to perform well on low-dimensional systems but struggle to effectively address the challenges posed by highdimensional complex systems. This is mainly because highdimensional systems require more complex neural network structures to design controllers and control barrier certificates, which causes general SMT verification methods to fail.

Liu et al. [2024] proposed Kolmogorov-Arnold Networks (KANs) as a promising alternative to multi-layer Perceptrons. In contrast to traditional models, KANs use activation functions on the connections between nodes, which can also learn and adapt during the training process. This architectural breakthrough enables KANs to better capture complex, nonlinear relationships by directly optimizing univariate functions. In addition, KANs have pruning properties that can remove unimportant edges and nodes from the network, significantly reducing its complexity. To address the issue of general SMT verification failure caused by neural controllers and neural control barrier certificates in high-dimensional systems, in this paper, we propose a new framework using KANs instead of FNNs to formally synthesize safe controllers and control barrier certificates. Specifically, our proposed framework consists of two parts. In the first part, it uses KANs to generate candidate control barrier certificates and controllers. The B-spline-based learnable activation function enhances the network's representation power and effectively addresses the issues of low success rates encountered when using fixed activation functions in FNNs for safe controller synthesis. In the second part, it prunes the candidate barrier certificate and controller networks, allowing the networks to more efficiently extract important features. Then, symbolization is applied to the networks, resulting in simpler and more human-readable expressions. Finally, it checks whether the candidates satisfy all the requirements of control barrier certificates through the SMT solver dReal. Overall, the main contributions of this work are described as follows:

• We introduce a new type of control barrier certificates and controllers represented as KANs, which uses learnable activation functions to enhance representation power.
• We leverage the pruning and network symbolization of KANs, improving both the efficiency and success rate of SMT verification in high-dimensional systems.
• We implement our tool KAN4CBC and conduct a detailed experimental evaluation on a set of benchmarks, demonstrating that our approach is more effective in generating safe controllers than the state-of-the-art tools.

2 RelatedWork

There are two main methods for analyzing and verifying continuous dynamical systems: reachability computation and barrier certificate synthesis. Reachability relies on over- and under-approximations, but due to the lack of closed-form solutions for ODEs and the computational cost of numerical methods, its scalability is limited. The concept of barrier certificates was first introduced by Prajna [2006], dividing the state space into safe and unsafe regions. This approach provides a more efficient and accurate proof of safety, particularly for nonlinear and uncertain systems, and is especially effective for verifying safety over an infinite time horizon.

In the field of control, researchers have explored various forms of barrier certificates to accommodate different types of dynamical systems. Many studies [Ahmadi and Majumdar, 2016; She et al., 2013] have employed SOS relaxation and semidefinite programming methods to generate polynomial barrier certificates. These approaches transform the barrier certificate synthesis problem into constraints expressed as linear or bilinear matrix inequalities, which are typically solved through numerical optimization. Kong et al. [2014] introduced a novel exponential condition barrier certificate that maintains convexity while reducing conservativeness, providing a more precise and effective approach for safety verification of semialgebraic hybrid systems. Zeng et al. [2016] proposed a new verification condition and a novel computational method combining sampling-based relaxation with least-squares and quadratic programming (LS-QP) alternating projection to find Darboux-type barrier certificates, enhancing the verification of nonlinear hybrid systems. Sogokon et al. [2018] introduced a multi-dimensional framework using vector barrier certificates, thereby extending their applicability.

The emergence of neural networks has provided new possibilities for synthesizing barrier certificates. Researchers have explored learning neural network certificate functions and achieved encouraging results [Zhang et al., 2023b; Lindemann et al., 2021]. However, to ensure deterministic guarantees, these methods must include a verification procedure to confirm the validity of the certificate. Some contributions have employed counterexample-guided Inductive Synthesis (CEGIS) procedure [Liu et al., 2023], where a learner trains a neural network to meet barrier certificate requirements over a finite set of samples, and a verifier either proves validity of the barrier certificate or provides counterexamples using an SMT solver [Kapinski et al., 2014; Chang et al., 2019]. However, the use of fixed activation functions can significantly impact the efficiency and success rate of generating barrier certificates. To address the nondifferentiability issue caused by ReLU, Zhang et al. [2023a] proposed a piecewise linear optimization method combined with Interval Bound Propagation for verification. Hu et al. [2024] proposed using symbolic derivative boundary propagation to verify ReLU-based neural CBCs. However, these methods are not universally applicable and become inefficient for high-dimensional systems. Therefore, in this paper, we propose improvements to the network by using KAN, which not only addresses the issues caused by fixed activation functions but also ensures that SMT verification remains efficient in high-dimensional systems.

3 Preliminaries

This section introduces the basic concepts used in the paper.

3.1 Continuous Dynamical System

Consider a controlled continuous dynamical system S:

where x ⊆ Rn represents the state of the system, ˙x denotes the derivative of x with respect to time t, u ⊆ Rm means a control input, f = (f1, f2, · · · , fn)T is the vector field on the state space Ω ⊆ Rn . We define a feedback controller u = h(x), which leads to the autonomous closed-loop dynamics given by:

Let X ⊆ Rn be a compact set denoting the state space of the system, and XI , XU ⊆ X represent the set of initial states and unsafe states, respectively.

We assume that f and h are Lipschitz continuous, ensuring the existence of a time trajectory ξx0 h (t), where ξx0 h (t) starting from x0 denotes the value of the state x at time t > 0.

In this paper, we focus on the problem of safe controller synthesis, specifically designing a safe controller u = h(x) that guarantees the controlled system (2) remains safe.

Definition 1 (safety). For a controlled continuous dynamical system, a given initial region XI ⊆ X and a given unsafe region XU ⊆ X, the controller u = h(x) is a safe one if the following condition holds:

3.2 Control Barrier Certificate

Verifying the safety of the controller requires analyzing the behavior of system (2) over an infinite time horizon. Following [28], we aim to find a control barrier certificate as proof of safety, with the existence of a control barrier certificate implying the safety of the controller. For a controlled continuous dynamical system (2), given the sets X,XU and XI, if there exists a continuous real-valued function B(x) : X → R satisfying:

then B(x) is a control barrier certificate, and the safety of the system is guaranteed. Here, ˙B(x) is the Lie derivative of B with respect to a vector field f , defined as follows:

Consider a trajectory ξx0 h (t) and observe the evolution of B(ξx0 h (t)) along this trajectory. The initial condition ensures B(x0) ≤ 0, and the final condition requires B(ξx0 h (t)) to decrease alone the trajectory ξx0 h (t). As a result, under inputs provided by h, such a trajectory ξx0 h (t) is prevented from entering the unsafe region XU, where B(x) > 0, so the safety of the controller is guaranteed.

3.3 Problem Statement

Previous works for constructing control barrier certificates and safe controllers often represent them in the form of FNNs. In high-dimensional systems, as the number of layers and nodes in the network increases, the expressions become quite complex, which significantly reduces the efficiency of general SMT methods for verification. To effectively address the challenges of high-dimensional complex systems, we propose using KANs instead of FNNs because they have learnable activation functions, which provide enhanced scalability and expressive power. Additionally, their pruning and symbolization properties can generate simple expressions, making SMT verification more efficient.

Problem 1. Given a controlled continuous dynamical system S, the problem is to synthesize control barrier certificates and safe controllers using KANs to ensure the safety of the system, achieving dimensional scalability and improved verification efficiency.

4 Method

In this section, we introduce a novel framework for synthesizing KAN controllers, which can guarantee the safety of the continuous dynamical systems. The overview of the methodology is depicted in Figure 1. The complete process can be divided into the following two stages.

• We devise a Learner component to synthesize candidate control barrier certificates and controllers. This component trains two KANs on a sampled dataset and learns the networks' activation functions by a special loss function.
• We design a Verifier component to formally verify the validity of the candidate KAN control barrier certificates and controllers. This component utilizes pruning and symbolization to simplify the candidate networks, and then uses the SMT solver to verify their validity.

4.1 Kolmogorov-Arnold Network (KAN)

Kolmogorov-Arnold Network (KAN) is a novel network architecture inspired by the Kolmogorov-Arnold representation theorem [Kolmogorov, 1961].

Theorem 1 (Kolmogorov-Arnold representation theorem). For any continuous function f mapping from [0, 1]n to the real numbers R, there exists a set of continuous functions ϕi,j (where i = 1, 2, . . . , 2n + 1 and j = 1, 2, . . . , n + 1) such that

According to Equation (6), KAN can be represented as a nested combination of two layers of univariate functions. In matrix form, KAN is defined as:

where Φin is a matrix composed of univariate functions, represented as:

and Φout is a row vector of univariate functions:

So the KAN in Equation (7) are simply compositions of two KAN layers. In practical applications, we can achieve deeper KAN by simply stacking more KAN layers. Thus, a L-Layer KAN can be constructed as follows:

where Φl is the matrix of activation functions corresponding to the lth KAN layer. A simple KAN with two input neurons and one output neuron is illustrated in Figure 2.

The shape of a KAN can be represented as an integer array [n0, n1, · · · , nL] , where ni denotes the number of nodes in the i-th layer. Let xl,i denote the ith neuron in the lth layer. There are nlnl+1 activation functions between the l-th layer and the (l + 1)-th layer. Let ϕl,i,j denote the activation function that connects xl,i and xl+1,j. The value of xl+1,j can be calculated as follows:

Different from FNNs, KAN employs learnable activation functions ϕ(x) at the network's edges:

which is the sum of the basis function b(x):

and the spline function spline(x):

where ci is trainable, and Bi(x) are B-spline basis functions, and wb and ws are trainable.

By observing the network structure of KAN, it can fit complex nonlinear relationships with fewer parameters using Bspline functions. This is because B-splines represent global functions through local control, reducing the need for a large number of parameters compared to FNN. By flexibly adjusting the degree k and grid size g, which determine the number of B-splines, KAN can adapt to complex patterns in different data and systems, ensuring the model has strong expressiveness while avoiding overfitting. While maintaining the model's representation power, a smaller grid size can significantly reduce computational complexity, allowing KAN to efficiently handle large-scale datasets. As training progresses, the grid size can also be dynamically adjusted to improve model accuracy without the need to retrain the entire network.

Therefore, it is reasonable to use KANs as the networks for synthesizing control barrier certificates and controllers. For the controlled dynamical system S, we use two KANs to separately train a control barrier certificate and a controller. The input dimension of both networks matches the system's dimension, with the output dimension of the barrier certificate network set to 1, and the output dimension of the controller network corresponding to the control input dimension.

4.2 Training of the KAN Barrier and Controller

In this subsection, we will introduce the method for synthesizing KAN control barrier certificates and controllers. Based on the control barrier certificate conditions, we design a loss function for the training dataset. During the training process, the B-spline functions in KANs are updated by minimizing the loss function value of sampled data points.

Training Dataset Construction. Without loss of generality, consider a state set X. We divide X into a finite number of cells X1, X2, . . . , XN by choosing a discretization parameter ϵ. From each of these cells, we then select sample points xi ∈ Xi such that ∥x-xi∥ ≤ ϵ, for all x ∈ Xi. Let D denote the set of all these sampled points. Using this method, we can construct the dataset DI , DU and DD, with each batch being sampled from XI , XU and X.

Loss Function. We formally define the loss function below:

where τI , τU , τD serve as offsets that are included to enhance the numerical stability during training. Note that the terms in

(15) correspond to the three control barrier certificate conditions, respectively.

To generate a KAN control barrier certificate candidate B(x) and a KAN controller h(x), we employ gradient descent techniques to minimize LB. When the loss decreases to 0, it indicates that the learned KANs can serve as a candidate control barrier certificate and a candidate controller, respectively.

4.3 KAN Barrier and Controller Verification

In this subsection, we will introduce SMT solving for formally verifying candidate control barrier certificates and controllers represented by KANs, as those generated through gradient descent techniques do not provide formal safety guarantees. Before SMT verification, we will prune and symbolize the networks to accelerate the verification process.

Pruning and Symbolization. To facilitate verification, we prune the trained networks into smaller subnetworks. We perform sparsification [Liu et al., 2024] at the node level, and for the i-th neuron in the l-th layer, we define its incoming and outgoing scores as:

If both the incoming and outgoing scores are greater than the threshold, the node is retained, and the remaining unimportant nodes are pruned. We take node x1,1 in Figure 2 as an example, its incoming scores I1,1 = max{|ϕ0,1,1|, |ϕ0,2,1|} and outgoing scores O1,1 = |ϕ1,1,1|. If the score of either I1,1 or O1,1 is less than the threshold, the node, along with its connected edges and activation function, will be removed.

Because B-spline functions are generated recursively, they cannot be formally expressed with explicit expressions, making verification challenging. Since the essence of KAN is to approximate arbitrary functions through the superposition of multiple nonlinear functions, we can transform the activation functions from numerical forms of B-spline to symbolic forms (such as sin, tanh, etc.). In Figure 3, we show the symbolization process through a regression task f(x, y) = sin(πx) + πexp(y). A one-layer KAN with shape [2,1] is initialized and trained using a dataset (xi, yi, fi)where i = 1, 2, . . . , n. Then, the activation functions are set to sin and exp, respectively. At this stage, an accurate symbolic formula cannot be obtained because the input and output of the

Algorithm 1 Learning Formally Verified CBC and controller

Input: System S = (f,XD,XI,XU), a discretization pa-

rameter ϵ Output:control barrier certificate B and a safe controller h function LEARNER(S, ϵ) repeat D ← SampleData(S, ϵ) compute loss LB, update KANs until LB = 0 return candidate KAN barrier B and controller h end function function VERIFIER(B, h, iter) if iter = 1 then B, h ← Pruning and Symbolification(B, h) end if B, h ← encoding dReal(B, h) Cex ← verify dReal(B, h) if Cex = None then return True elseD ← D ∪ Cex end if end function function CEGIS(S) initialise KAN B and h, S, ϵ repeat iter ← iter + 1 B, h ← LEARNER(S, ϵ) F lag ← VERIFIER(B, h, iter) until F lag = True return B, h end function

activation functions may have shifts and scalings. Therefore, after further fitting, the coefficient for x and exp is both set to 3.14. The final output symbolic formula f(x, y) = sin(3.14x) + 3.14exp(y) closely matches the expression of the regression task.

In this way, we simplify candidate barrier certificates and controllers through pruning and symbolization for SMT verification.

SMT Verification. We design a counterexample-guided framework based on the SMT solver for verification, which is designed to find states that violate the barrier conditions in (4). To achieve this, we formulate the negation of the three conditions and verify the conditions are unsatisfiable, as follows:

We choose dReal as our SMT verifier, which ensures the correctness of its unsat decisions. Therefore, when dReal returns unsat for the given formula (17), it confirms that no solution exists within the specified precision, and the simplified candidate control barrier certificate B(x) and controller h(x) are valid. Otherwise, it means that dReal has found a counterexample that violates the safety properties of the control barrier certificate.

During the verification process, dReal can only find one counterexample at a time. To improve the efficiency of verification, points around the counterexample will be sampled and added to the dataset to help the learner refine the control barrier certificate and controller. We repeat this process of refinement and verification until no counterexamples are found.

Our main algorithm is illustrated in Algorithm 1.

5 Experiments

We have implemented a tool named KAN4CBC using PyTorch platform for synthesizing KAN control barrier certificates and safe controlllers. We compare our tool against the latest version of FOSSIL2.0 [Edwards et al., 2024] and nncontroller [Zhao et al., 2021]. To compare and illustrate the performance differences between the automatic learning of activation functions and the manual selection of activation functions, we choose sigmoid function as the activation function for FOSSIL2.0, bent-relu function for nncontroller. For each case, we ensure that the number of sampling points is consistent between the three tools. Besides, we use AdamW as the optimization algorithm whose learning rate is 0.001 with β1 = 0.9, β2 = 0.999 and ε = 10-8 , and the loss function in Equation (15) with τI = τU = τD = 0. We set the hyper-parameter grid size in KAN to 5, and the degree k to 3. The timeout is set to 1 hour, meaning that if a real control barrier certificate and safe controller are not synthesized within 1 hour, the attempt is considered a failure. All experiments are performed on a machine running Ubuntu 24.04 with AMD Ryzen 5 5600G and 16GB memory.

5.1 Case Studies

We evaluate the effectiveness of our tool with examples that include both polynomial and non-polynomial cases. The Ex1 is a 2-dimensional inverted pendulum system [Zhu et al., 2019], the Ex2 is a 3-dimensional ACAS Xu system [Clavi`ere et al., 2021], where a controller is used to control the flight angle of the airplane to prevent collision. The Ex3 is a unicycle system [Yang et al., 2023], where a controller is used to control the unicycle's speed and the angle. The Ex4 [Chesi, 2004], Ex5 [Sassi and Sankaranarayanan, 2015], Ex6 [Zeng et al., 2016], Ex7 [Klipp et al., 2005] and Ex8 [Klipp et al., 2005] are systems with four, five, six, seven, and nine dimensions, respectively. And the Ex1 to Ex3 include nonpolynomial terms in the dynamics.

Example 1 (Inverted Pendulum). The continuous dynamical system is as follows:

The domain is X = {x ∈ R2 | - π4 ≤ x1 ≤ π4 ,- π4 ≤ x2 ≤ π4 }. Our goal is to generate a safe controller that ensures all trajectories starting from the initial region XI = {x ∈ R2 | - π 15 ≤ x1 ≤ π 15 , - π 15 ≤ x2 ≤ π 15 } will never enter the unsafe region XU, which is the complement of {x | - π6 ≤ x1 ≤ π6 , - π6 ≤ x2 ≤ π6 } in X.

We sample 16 points from the initial region, 256 points from unsafe region, and 1024 points from domain region. Using a two-layer KAN with shape [2, 5, 1], KAN4CBC successfully synthesized the KAN barrier certificate and the safety KAN controller, as illustrated in Figure 4, in which initial regions XI and unsafe sets XU are represented in green and red respectively, and the blue line outlines the level curve B(x) = 0. The expressions for the KAN control barrier certificate B(x) and the safe controller h(x) are as follows:

Example 2 (ACAS Xu system). The continuous dynamical system is as follows:

The domain is X = {x ∈ R3 | -1 ≤ x1 ≤ 1, -1 ≤ x2 ≤ 1, 0 ≤ θ ≤ π}. Our goal is to generate a safe controller that ensures all trajectories starting from the initial region XI = {x ∈ R3 | x21 + x22 ≤ 0.25, 0 ≤ θ ≤ π} will never enter the unsafe region XU = {x ∈ R3 | 0.5 ≤ x1 ≤ 0.75, 0.5 ≤ x2 ≤ 1, 0 ≤ θ ≤ π}.

We sample 125 points each from the initial region and the unsafe region, and 1000 points from the domain region. Using a two-layer KAN with shape [3, 5, 1], KAN4CBC successfully synthesized the KAN barrier certificate and safety KAN controller, as illustrated in Figure 5, in which the zero level set of learned barrier certificate (the yellow surface) separates XU (the red cuboid) from simulated trajectories starting from XI (the green ellipsoid). The expressions for the KAN control barrier certificate B(x) and the safe controller h(x) are as follows:

5.2 Results Analysis

Table 1 summarizes the results of our KAN4CBC compared to FOSSIL2.0 and nncontroller in eight different cases. The shape represents the KAN structures corresponding to the control barrier certificate and safe controller. To compare the performance between learnable activation functions and fixed activation function, the number of layers and nodes per layer in the neural network within two other methods are kept consistent with those in KAN. The iter, Tl, Tv, Tsum represent the number of iterations, training time, verification time and the total time required for the method to generate a safe controller in the corresponding case, respectively. And the symbol × indicates the synthesis of the safe controller failed within one hour.

From Table 1, we conclude that our tool KAN4CBC can successfully synthesize safe controllers for all cases. In contrast, FOSSIL2.0 can only synthesize safe controllers for three cases, and nncontroller succeeds in just one case. Our tool is more scalable because KAN has learnable activation functions, which enhance its expressive power compared to neural networks, enabling it to synthesize safe controllers with fewer network nodes. However, the other two tools lack this capability.

Considering efficiency, our tool generally outperforms in the majority of cases because it controls network complexity through its pruning feature, achieving higher computational efficiency, especially in verification. On average, KAN4CBC has a longer training time per iteration, but a shorter verification time, and the total number of iterations is fewer than FOSSIL2.0 and nncontroller, so its total synthesis time ends up being shorter than two other methods. Only for Ex1 and Ex2 do FOSSIL2.0 and nncontroller synthesize safe controllers faster than our tool, because training neural networks is easier than training KAN's B-spline functions for low-dimensional simple systems. Our method outperforms FOSSIL2.0 and nncontroller on high-dimensional examples, because traditional safe controller synthesis using neural networks requires complex structures for high-dimensional systems, resulting in lengthy expressions that hinder SMT solving. In contrast, the KAN achieves strong expressiveness with fewer layers and nodes, and its pruning and network symbolization significantly improve SMT solving efficiency.

In summary, Table 1 indicates that our method successfully synthesizes safe controllers to ensure the system's safety across all eight benchmark experiments, but FOSSIL2.0 and nncontroller fail. Besides, KAN4CBC requires fewer iterations and less time compared to FOSSIL2.0 and nncontroller in most cases. The results demonstrate that our method exhibits superior efficiency and versatility in synthesizing safe controllers in high-dimensional systems.

6 Conclusion

In this paper, we have proposed a novel and efficient method for formally synthesizing control barrier certificates and controllers to verify the safety of controlled continuous dynamical systems. Our synthesis process consists of two stages: First, it generated candidate control barrier certificates and controllers using KAN which can improve representation power. Second, it simplified the candidate barrier certificates and controller networks through pruning, and then output the candidate expressions by symbolizing the networks which makes SMT verification more efficient and overcomes the limitation of SMT verification failure when applying neural barrier certificates to high-dimensional systems. We demonstrated the effectiveness of our tool using several case studies.

Acknowledgements

This work was supported in part by the National Natural Science Foundation of China under Grant 62272416 and Grant 62132014; in part by the Zhejiang Provincial Natural Science Foundation of China under Grant LD24F020006; and in part by the Fundamental Research Funds of Zhejiang SciTech University under Grant 24232090-Y.