Certifying Certainty and Uncertainty in Approximate Membership Data Structures
Abstract:
Approximate Membership Query structures (AMQs) rely on randomisation for time- and space-efficiency, while introducing a possibility of false positive and false negative answers. Correctness proofs of such structures involve subtle reasoning about bounds on probabilities of getting certain outcomes. Because of these subtleties, a number of unsound arguments in such proofs have been made over the years.
In this work, we address the challenge of building rigorous and reusable computer-assisted proofs about probabilistic specifications of AMQs. We describe the framework for systematic decomposition of AMQs and theirproperties into a series of interfaces and reusable components. We implement our framework as a library in the Coq proof assistant and showcaseit by encoding in it a number of non-trivial AMQs, such as Bloom filters,counting filters, quotient filters and blocked constructions, and mechanising the proofs of their probabilistic specifications.
We demonstrate how AMQs encoded in our framework guarantee the absence of false negatives by construction. We also show how the proofs about probabilities of false positives for complex AMQs can be obtained by means of verified reduction to the implementations of their simpler counterparts. Finally, we provide a library of domain-specific theorems and tactics that allow a high degree of automation in probabilistic proofs.
Joint work with Ilya Sergey (NUS). Work appeared at CAV '20.
Biodata:
Kiran Gopinathan is a PhD candidate at the School of Computing at NUS. He has had past experience in a range of disciplines within the field, from interoperable data format design to industrial machine learning. His current main focus lies within the use of formal methods for reasoning about probabilistic algorithms. In particular, his interests relate to how these formal methods can be used to build and construct provably correct probabilistic algorithms. https://gopiandcode.uk/