We present a novel approach for verifying properties of Kolmogorov-Arnold Networks (KANs), a class of neural networks characterized by nonlinear, univariate activation functions typically implemented as piecewise polynomial splines or Gaussian processes. Our method creates mathematical ``abstractions'' by replacing each KAN unit with a piecewise affine (PWA) function, providing both local and global error estimates between the original network and its approximation. These abstractions enable property verification by encoding the problem as a Mixed Integer Linear Program (MILP), determining whether outputs satisfy specified properties when inputs belong to a given set. A critical challenge lies in balancing the number of pieces in the PWA approximation: too many pieces add binary variables that make verification computationally intractable, while too few pieces create excessive error margins that yield uninformative bounds. Our key contribution is a systematic framework that exploits KAN structure to find optimal abstractions. By combining dynamic programming at the unit level with a knapsack optimization across the network, we minimize the total number of pieces while guaranteeing specified error bounds. This approach determines the optimal approximation strategy for each unit while maintaining overall accuracy requirements. Empirical evaluation across multiple KAN benchmarks demonstrates that the upfront analysis costs of our method are justified by superior verification results.

翻译：本文提出了一种验证科尔莫戈罗夫-阿诺德网络（KANs）性质的新方法。KANs是一类以非线性单变量激活函数为特征的神经网络，其激活函数通常实现为分段多项式样条或高斯过程。我们的方法通过将每个KAN单元替换为分段仿射（PWA）函数来构建数学“抽象”，从而提供原始网络与其近似之间的局部和全局误差估计。这些抽象通过将验证问题编码为混合整数线性规划（MILP）来实现性质验证，以判定当输入属于给定集合时，输出是否满足特定性质。一个关键挑战在于平衡PWA近似的分段数量：分段过多会引入大量二元变量，导致验证计算不可行；而分段过少则会产生过大的误差范围，从而得到无信息量的边界。我们的核心贡献是提出一个系统化框架，该框架利用KAN的结构特性来寻找最优抽象。通过结合单元级的动态规划与网络级的背包优化，我们在保证指定误差边界的同时最小化总分段数量。该方法在满足整体精度要求的前提下，为每个单元确定最优近似策略。在多个KAN基准测试上的实证评估表明，我们方法的前期分析成本因其优越的验证结果而具有合理性。