Formal Verification of Kolmogorov-Arnold Networks

Motivated by the Kolmogorov-Arnold representation theorem, Kolmogorov-Arnold Networks (KANs) are a novel neural network architecture that replace the weight matrices and fixed activation functions of a multi-layer perceptron with a learned univariate spline on every edge and an unweighted sum on every node. They have quickly become popular, being utilized as scientific surrogates, safe controllers and barrier certificates, but attempts to verify them are limited. Mainstream neural network verification tools have no spline operator, and conversion from a KAN with a grid of $G$ cells to a ReLU network inflates the network by a factor of $G$. Therefore, this work develops formal verification utilizing set-based reachability for KANs by directly considering its unique architecture. We show that degree-1 KANs without the base branch admit exact verification, and that KANs of degree $\ge 2$ or with the base branch admit sound verification. We compare head-to-head a method family instantiated on the KAN structure; using interval bound propagation, CROWN-style bounds, mixed-integer linear programs (MILPs), and star-set reachability. We demonstrate formal verification of five classes of properties for trained KANs, namely robustness, output ranges, barrier conditions, monotone ordering and one-step reachability; including certified robustness for an adversarially attacked $784$-input MNIST KAN and all three conditions of a control barrier certificate whose barrier and controller are both KANs. Our literature-based case studies collectively can be considered a small KAN verification benchmark, *e.g.* for VNN-COMP.