Formally Verified Implementation of the K-Nearest Neighbors Classification Algorithm

Formally Verified Implementation of the K-Nearest Neighbors Classification Algorithm

연구 분야: Verification

학회: Brazilian Symposium on Formal Methods

Classification, one of the most commonly applied algorithmic techniques in data mining, involves assigning a class label to observations based on previously seen data. Among the most ubiquitous and well-known approaches to classification is K-nearest neighbor ( NN) search, which predicts the class label for a query by determining the plurality class of its K-nearest data points. In this paper, we present a mechanically verified implementation of a K-nearest neighbors classification algorithm in the COQ proof assistant, a powerful formal verification tool. Formally certifying the implementation, by proving that it meets its specification, provides a strong guarantee and high confidence that the classifier actually produces results in the expected manner. Given the conceptually simple nature of the NN algorithm, this serves as a good baseline for developing specification and verification techniques for machine learning implementations.