Formal Synthesis of Barrier Certificates Using Fourier Kolmogorov-Arnold Network
Authors: Xiongqi Zhang, Junwei Xu, Yang Wang, Dongming Xiang, Wang Lin, Zuohua Ding
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We implement the tool KAN4BC, and evaluate its performance over a set of benchmarks. The experimental results demonstrate the effectiveness and efficiency of our method. We implement our tool KAN4BC and conduct a detailed experimental evaluation on a set of benchmarks, demonstrating that our approach is more effective in generating barrier certificates than the state-of-the-art tool FOOSIL2.0. Experiments We have implemented a tool named KAN4BC using Py Torch platform for synthesizing Fourier KAN barrier certificates. We compare our tool against the latest version of FOSSIL2.0 (Edwards, Peruffo, and Abate 2024). |
| Researcher Affiliation | Academia | Xiongqi Zhang, Junwei Xu, Yang Wang, Dongming Xiang, Wang Lin*, Zuohua Ding School of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou, China EMAIL, EMAIL, EMAIL |
| Pseudocode | Yes | Algorithm 1: Learning Formally Verified Barrier Certificate Input: System S = (f, XD, XI, XU), a discretization parameter ϵ Output: Barrier Certificates B function LEARNER(S, ϵ) repeat D Sample Data(S, ϵ) compute loss LB and η, update Fourier KAN until LB = 0 return candidate Fourier KAN barrier B, η end function function VERIFIER(B, η, iter) if iter < Max Iter then B encoding d Real(B) Cex verify d Real(B) if Cex = None then return True else D D Cex end if else L cal Lipschitz(B) if Lϵ + η 0 then return True end if end if return False end function function CEGIS(S) initialise Fourier KAN, S, ϵ repeat iter iter + 1 B, η LEARNER(S, ϵ) Flag VERIFIER(B, η, iter) until Flag = True or iter = Max Iter + 1 return B end function |
| Open Source Code | No | The paper mentions implementing a tool named KAN4BC but does not provide a direct link to a repository, an explicit statement of code release, or mention its availability in supplementary materials for the described methodology. |
| Open Datasets | Yes | The cases from barr1 to barr4 are taken from FOSSIL2.0 s own benchmarks, barr1 originally presented in (Zeng et al. 2016), barr2 (Liu et al. 2015) includes non-polynomial terms in the dynamics, barr3 (Prajna 2006) uses non-convex domains, barr4 (Barry, Majumdar, and Tedrake 2012) represents a robotics application, specifically the control of a plane s angular velocity, barr5 and barr6 (Sogokon, Ghorbal, and Johnson 2016) are 2-dimensional models, barr7 (Sankaranarayanan, Chen et al. 2013) is a 4-dimensional model. |
| Dataset Splits | Yes | We sample 256 points from the initial region,1024 points from unsafe region, and 16384 points from domain region. We sample 512 points each from the initial region and the unsafe region, and 32768 points from the domain region. |
| Hardware Specification | Yes | All experiments are performed on a machine running Ubuntu 24.04 with AMD Ryzen 5 5600G and 16GB memory. |
| Software Dependencies | No | The paper mentions using Py Torch platform and d Real as an SMT verifier, but it does not specify version numbers for either software dependency. |
| Experiment Setup | Yes | We use Adam W 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 (18) with τI = τU = τD = 0. We set the hyper-parameter gridsize in Fourier KAN to 1. The timeout is set to 1 hour, meaning that if a real barrier certificate is not synthesized within 1 hour, the attempt is considered a failure. |