Top

Published in:

2025 | OriginalPaper | Chapter

Formally Verified Implementation of the K-Nearest Neighbors Classification Algorithm

Authors : Bernny Velasquez, Jessica Herring, Nadeem Abdul Hamid

Published in: Formal Methods: Foundations and Applications

Publisher: Springer Nature Switzerland

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

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 (\(K\)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 \(K\)NN algorithm, this serves as a good baseline for developing specification and verification techniques for machine learning implementations.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Soundness-Preserving Fusion of Modal Logics in Coq

next chapter Formal Verification of Forward Secrecy and Post-Compromise Security for TreeKEM

Available only for authorised users

Throughout the paper, lowercase k denotes the number of dimensions of the data points and uppercase K is the number of nearest neighbors that are sought.

The Coq syntax we use for function headers is: \((\textit{ident}_{\tiny \text {{function}}}\ {\textbf {(}}\textit{ident}_{\tiny \text {{param}}} {\textbf {:}} \ \textit{type}_{\tiny \text {{param}}} {\textbf {)}} \cdots \ {\textbf {(}}\textit{ident}_{\tiny \text {{param}}}\ {\textbf {:}} \ \textit{type}_{\tiny \text {{param}}} {\textbf {)}}\ {\textbf {:}} \ \textit{type}_{\tiny \text {{return}}})\) representing a named function with explicitly-typed parameters.

As part of our work for the implementation of this paper, we abstracted the distance metric, D, used by knn_search - an improvement over [16]. For space reasons, we omit any further discussion about it throughout the rest of this paper.

https://coq.inria.fr/doc/v8.16/stdlib/Coq.FSets.FMapAVL.html.

https://coq.inria.fr/doc/v8.16/stdlib/Coq.Structures.Orders.html.

Conventionally, in Coq theorem statements, a conjunction of premises is written as a string of implication clauses (... -> ... -> ...).

https://coq.inria.fr/refman/using/libraries/funind.html.

Note, that correctness of the mechanics of the algorithm implementation (as formalized in this work), does not imply that the algorithm will necessarily produce accurate classifications for data points. It could well be that the correct plurality vote of the K nearest neighbors is different from the actual label of a query point.

The Coq proof assistant, v8.16 (2022). https://coq.inria.fr/

Anderson, E.: The species problem in Iris. Ann. Mo. Bot. Gard. 23(3), 457–509 (1936). http://www.jstor.org/stable/2394164

Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) Programming Languages and Systems, pp. 1–17. Springer, Berlin Heidelberg, Berlin, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_1CrossRef

Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: a practical tool for the coq proof assistant. In: Hagiya, M., Wadler, P. (eds.) Functional and Logic Programming, pp. 114–129. Springer, Berlin Heidelberg, Berlin, Heidelberg (2006). https://doi.org/10.1007/11737414_9CrossRef

Barthe, G., Grégoire, B., Zanella Béguelin, S.: Formal certification of code-based cryptographic proofs. In: POPL ’09: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 90–101. Association for Computing Machinery, New York, NY, USA (2009). https://doi.org/10.1145/1480881.1480894

Bentley, J.L.: Multidimensional binary search trees used for associative searching. Commun. ACM 18(9), 509–517 (1975). https://doi.org/10.1145/361002.361007CrossRef

Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions. Springer Publishing Company, 1st edn. (2010). https://doi.org/10.1007/978-3-662-07964-5

Braiek, H.B., Khomh, F.: On testing machine learning programs. J. Syst. Softw. 164, 110542 (2020). https://doi.org/10.1016/j.jss.2020.110542CrossRef

Cover, T., Hart, P.: Nearest neighbor pattern classification. IEEE Trans. Inf. Theory 13(1), 21–27 (1967). https://doi.org/10.1109/TIT.1967.1053964CrossRef

10.

Cunningham, P., Delany, S.J.: K-nearest neighbour classifiers - a tutorial. ACM Comput. Surv. 54(6), 1–25 (2021). https://doi.org/10.1145/3459665

11.

Fan, A.Z., Koutris, P.: Certifiable robustness for nearest neighbor classifiers. In: Olteanu, D., Vortmeier, N. (eds.) 25th International Conference on Database Theory, ICDT 2022, March 29 to April 1, 2022, Edinburgh, UK (Virtual Conference). LIPIcs, vol. 220, pp. 1–20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022). https://doi.org/10.4230/LIPICS.ICDT.2022.6

12.

Fassina, N., Ranzato, F., Zanella, M.: Robustness certification of k-nearest neighbors. In: Proceedings of the 23rd IEEE International Conference on Data Mining (ICDM’23) (2023)

13.

Friedman, J.H., Bentley, J.L., Finkel, R.A.: An algorithm for finding best matches in logarithmic expected time. ACM Trans. Math. Softw. 3(3), 209–226 (1977). https://doi.org/10.1145/355744.355745CrossRef

14.

Gu, R., Shao, Z., Chen, H., Wu, X., Kim, J., Sjöberg, V., Costanzo, D.: Certikos: an extensible architecture for building certified concurrent OS kernels. In: OSDI’16: Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, pp. 653–669. USENIX Association, USA (2016)

15.

Hall, J.A.: Seven myths of formal methods. IEEE Softw. 7(5), 11–19 (1990)CrossRef

16.

Hamid, N.A.: (Nearest) neighbors you can rely on: formally verified k-d tree construction and search in Coq. In: SAC ’24: Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing, pp. 1684–1693. Association for Computing Machinery, New York, NY, USA (2024). https://doi.org/10.1145/3605098.3635960

17.

Kneuper, R.: Limits of formal methods. Form. Asp. Comput. 9(4), 379–394 (1997). https://doi.org/10.1007/BF01211297CrossRef

18.

Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009). https://doi.org/10.1145/1538788.1538814CrossRef

19.

Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems: a survey. ACM Comput. Surv. 52(5), 1–41 (2019). https://doi.org/10.1145/3342355

20.

Namiot, D., Ilyushin, E., Chizhov, I.: On a formal verification of machine learning systems. Int. J. Open Inf. Technol. 10(05), 30–34 (2022)

21.

Pierce, B.C., et al.: Logical Foundations, Software Foundations, vol. 1. Electronic textbook (2023). http://softwarefoundations.cis.upenn.edu, version 6.5

22.

Selsam, D., Liang, P., Dill, D.L.: Developing bug-free machine learning systems with formal mathematics. In: ICML’17: Proceedings of the 34th International Conference on Machine Learning, vol. 70, pp. 3047–3056. JMLR.org (2017)

23.

Seshia, S.A., Sadigh, D., Sastry, S.S.: Toward verified artificial intelligence. Commun. ACM 65(7), 46–55 (2022). https://doi.org/10.1145/3503914CrossRef

24.

Sitawarin, C., Kornaropoulos, E.M., Song, D., Wagner, D.: Adversarial examples for k-nearest neighbor classifiers based on higher-order voronoi diagrams. In: Beygelzimer, A., Dauphin, Y., Liang, P., Vaughan, J.W. (eds.) Advances in Neural Information Processing Systems, vol. 34. Curran Associates Inc, Red Hook, NY (2021)

25.

Syriopoulos, P.K., Kalampalikis, N.G., Kotsiantis, S.B., Vrahatis, M.N.: kNN classification: a review. Ann. Math. Artif. Intell. 1–33 (2023). https://doi.org/10.1007/s10472-023-09882-x

Title: Formally Verified Implementation of the K-Nearest Neighbors Classification Algorithm
Authors: Bernny Velasquez
Jessica Herring
Nadeem Abdul Hamid
Publisher: Springer Nature Switzerland
Book: Formal Methods: Foundations and Applications
Print ISBN: 978-3-031-78115-5

Electronic ISBN: 978-3-031-78116-2

Copyright Year: 2025
DOI: https://doi.org/10.1007/978-3-031-78116-2_9

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"