콜모고로프-아르노 네트워크(KAN)의 속성 검증을 위한 최적 추상화

Optimal Abstractions for Verifying Properties of Kolmogorov-Arnold Networks (KANs)

본 연구는 콜모고로프-아르노 네트워크(KAN)의 속성 검증을 위한 새로운 접근 방식을 제시합니다. KAN은 비선형, 단변수 활성화 함수를 특징으로 하는 신경망의 한 종류이며, 일반적으로 다항식 스플라인 또는 가우스 프로세스로 구현됩니다. 제안하는 방법은 각 KAN 유닛을 다변수 선형(PWA) 함수로 대체하여 수학적 "추상화"를 생성하며, 이를 통해 원본 네트워크와 근사 네트워크 간의 로컬 및 글로벌 오차 추정치를 제공합니다. 이러한 추상화는 문제를 혼합 정수 선형 계획법(MILP)으로 변환하여 해결함으로써, 특정 입력 집합에 속하는 입력에 대해 출력값이 지정된 속성을 만족하는지 여부를 판단합니다. 중요한 과제는 PWA 근사에서 사용되는 구간의 수를 균형 있게 결정하는 것입니다. 구간이 너무 많으면 검증에 필요한 이진 변수가 증가하여 계산적으로 불가능해지고, 반대로 구간이 너무 적으면 과도한 오차 마진이 발생하여 의미 없는 경계를 제공합니다. 본 연구의 핵심 기여는 KAN의 구조를 활용하여 최적의 추상화를 찾는 체계적인 프레임워크를 개발한 것입니다. 본 연구는 유닛 수준에서의 동적 프로그래밍과 네트워크 전체의 나apsack 최적화를 결합하여 총 구간 수를 최소화하면서 동시에 지정된 오차 경계를 보장합니다. 이러한 접근 방식은 각 유닛에 대한 최적의 근사 전략을 결정하면서 전체적인 정확도 요구 사항을 유지합니다. 여러 KAN 벤치마크에 대한 실험적 평가 결과, 제안하는 방법의 초기 분석 비용은 우수한 검증 결과로 정당화됩니다.

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.