(Nearest) Neighbors You Can Rely On: Formally Verified k-d Tree Construction and Search in Coq
2023
Online
report
The k-d tree is a classic binary space-partitioning tree used to organize points in k-dimensional space. While used in computational geometry and graphics, the data structure has a long history of application in nearest neighbor search. The objective of the nearest neighbor search problem is to efficiently find the closest point(s) to a given query point, and is the basis, in turn, of common machine learning techniques. We present in this paper a case study in the certified implementation, using the Coq proof assistant, of k-d tree construction from a set of data and the accompanying K-nearest neighbors search algorithm. Our experience demonstrates an intuitive method for specifying properties of these algorithms using the notion of list permutations.
Titel: |
(Nearest) Neighbors You Can Rely On: Formally Verified k-d Tree Construction and Search in Coq
|
---|---|
Autor/in / Beteiligte Person: | Hamid, Nadeem Abdul |
Link: | |
Veröffentlichung: | 2023 |
Medientyp: | report |
Schlagwort: |
|
Sonstiges: |
|