Document Open Access Logo

Verification of the CVM Algorithm with a Functional Probabilistic Invariant

Authors Emin Karayel , Seng Joe Watt , Derek Khu , Kuldeep S. Meel , Yong Kiam Tan

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2025.34.pdf
  • Filesize: 1.76 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Higher order logic
  • Mathematics of computing → Probabilistic algorithms
  • Theory of computation → Pseudorandomness and derandomization
Keywords
  • Verification
  • Isabelle/HOL
  • Randomized Algorithms
  • Distinct Elements

Metrics

Abstract

Estimating the number of distinct elements in a data stream is a classic problem with numerous applications in computer science. We formalize a recent, remarkably simple, randomized algorithm for this problem due to Chakraborty, Vinodchandran, and Meel (called the CVM algorithm). Their algorithm deviated considerably from the state of the art, due to its avoidance of intricate derandomization techniques, while still maintaining a close-to-optimal logarithmic space complexity.
Central to our formalization is a new proof technique based on functional probabilistic invariants, which allows us to derive concentration bounds using the Cramér-Chernoff method without relying on independence. This simplifies the formal analysis considerably compared to the original proof by Chakraborty et al. Moreover, our technique opens up the possible algorithm design space; we demonstrate this by introducing and verifying a new variant of the CVM algorithm that is both total and unbiased - neither of which is a property of the original algorithm. In this paper, we introduce the proof technique, describe its use in mechanizing both versions of the CVM algorithm in Isabelle/HOL, and present a supporting formalized library on negatively associated random variables used to verify the latter variant.

Cite As Get BibTex

Emin Karayel, Seng Joe Watt, Derek Khu, Kuldeep S. Meel, and Yong Kiam Tan. Verification of the CVM Algorithm with a Functional Probabilistic Invariant. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 34:1-34:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.34

Author Details

Emin Karayel
  • School of Computation, Information and Technology, Technical University of Munich, Germany
Seng Joe Watt
  • Institute for Infocomm Research (I2R), A*STAR, Singapore
Derek Khu
  • Institute for Infocomm Research (I2R), A*STAR, Singapore
Kuldeep S. Meel
  • Georgia Institute of Technology, Atlanta, GA, USA
  • University of Toronto, Canada
Yong Kiam Tan
  • Institute for Infocomm Research (I2R), A*STAR, Singapore
  • Nanyang Technological University, Singapore

Funding

  • Watt, Seng Joe: Singapore NRF Fellowship Programme NRF-NRFF16-2024-0002.
  • Meel, Kuldeep S.: Natural Sciences and Engineering Research Council of Canada (NSERC), funding reference [RGPIN-2024-05956].
  • Tan, Yong Kiam: Singapore NRF Fellowship Programme NRF-NRFF16-2024-0002.

Supplementary Materials

References

  1. Archive of Formal Proofs. Accessed: 2025-02-26. URL: https://isa-afp.org.
  2. Noga Alon, Yossi Matias, and Mario Szegedy. The space complexity of approximating the frequency moments. J. Comput. Syst. Sci., 58(1):137-147, 1999. URL: https://doi.org/10.1006/JCSS.1997.1545.
  3. Noga Alon and Joel H. Spencer. The Probabilistic Method, Second Edition. John Wiley, 2000. URL: https://doi.org/10.1002/0471722154.
  4. Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. Sci. Comput. Program., 74(8):568-589, 2009. URL: https://doi.org/10.1016/J.SCICO.2007.09.002.
  5. Ziv Bar-Yossef, T. S. Jayram, Ravi Kumar, D. Sivakumar, and Luca Trevisan. Counting distinct elements in a data stream. In José D. P. Rolim and Salil P. Vadhan, editors, RANDOM, volume 2483 of LNCS, pages 1-10. Springer, 2002. URL: https://doi.org/10.1007/3-540-45726-7_1.
  6. Ezio Bartocci, Laura Kovács, and Miroslav Stankovič. Automatic generation of moment-based invariants for Prob-solvable loops. In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, ATVA, volume 11781 of LNCS, pages 255-276. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_15.
  7. Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Probabilistic program verification via inductive synthesis of inductive invariants. In Sriram Sankaranarayanan and Natasha Sharygina, editors, TACAS, volume 13994 of LNCS, pages 410-429. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30820-8_25.
  8. Jarosław Błasiok. Optimal streaming and tracking distinct elements with high probability. ACM Trans. Algorithms, 16(1):3:1-3:28, 2020. URL: https://doi.org/10.1145/3309193.
  9. Azucena Garvía Bosshard, Jonathan Bootle, and Christoph Sprenger. Formal verification of the Sumcheck protocol. In CSF, pages 605-619. IEEE, 2024. URL: https://doi.org/10.1109/CSF61375.2024.00014.
  10. Sourav Chakraborty, N. V. Vinodchandran, and Kuldeep S. Meel. Distinct elements in streams: An algorithm for the (text) book. In Shiri Chechik, Gonzalo Navarro, Eva Rotenberg, and Grzegorz Herman, editors, ESA, volume 244 of LIPIcs, pages 34:1-34:6. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.ESA.2022.34.
  11. Sourav Chakraborty, N. V. Vinodchandran, and Kuldeep S. Meel. Distinct elements in streams: An algorithm for the (text) book. CoRR, abs/2301.10191, 2023. URL: https://doi.org/10.48550/arXiv.2301.10191.
  12. Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint, Temesghen Kahsai, Tristan Ravitch, Stefan Zetzsche, Anjali Joshi, Joseph Tassarotti, Aws Albarghouthi, and Jean-Baptiste Tristan. Verified foundations for differential privacy. CoRR, abs/2412.01671, 2024. URL: https://doi.org/10.48550/arXiv.2412.01671.
  13. Jeffrey Dean and Sanjay Ghemawat. MapReduce: a flexible data processing tool. Commun. ACM, 53(1):72-77, 2010. URL: https://doi.org/10.1145/1629175.1629198.
  14. Jerry den Hartog and Erik P. de Vink. Verifying probabilistic programs using a Hoare like logic. Int. J. Found. Comput. Sci., 13(3):315-340, 2002. URL: https://doi.org/10.1142/S012905410200114X.
  15. Devdatt P. Dubhashi, Volker Priebe, and Desh Ranjan. Negative dependence through the FKG inequality. BRICS Report Series, 3(27), 1996. URL: https://doi.org/10.7146/brics.v3i27.20008.
  16. Devdatt P. Dubhashi and Desh Ranjan. Balls and bins: A study in negative dependence. Random Struct. Algorithms, 13(2):99-124, 1998. URL: https://doi.org/10.1002/(SICI)1098-2418(199809)13:2<99::AID-RSA1>3.0.CO;2-M.
  17. Manuel Eberl, Max W. Haslbeck, and Tobias Nipkow. Verified analysis of random binary tree structures. J. Autom. Reason., 64(5):879-910, 2020. URL: https://doi.org/10.1007/S10817-020-09545-0.
  18. Philippe Flajolet, Éric Fusy, Olivier Gandouet, and Frédéric Meunier. HyperLogLog: the analysis of a near-optimal cardinality estimation algorithm. In Conference on Analysis of Algorithms, 2007. URL: https://doi.org/10.46298/dmtcs.3545.
  19. Philippe Flajolet and G. Nigel Martin. Probabilistic counting algorithms for data base applications. J. Comput. Syst. Sci., 31(2):182-209, 1985. URL: https://doi.org/10.1016/0022-0000(85)90041-8.
  20. C. M. Fortuin, P. W. Kasteleyn, and J. Ginibre. Correlation inequalities on some partially ordered sets. Commun. Math. Phys., 22(2):89-103, 1971. URL: https://doi.org/10.1007/BF01651330.
  21. Michèle Giry. A categorical approach to probability theory. In B. Banaschewski, editor, Categorical Aspects of Topology and Analysis, volume 915 of LNM, pages 68-85. Springer, 1982. URL: https://doi.org/10.1007/BFb0092872.
  22. Kiran Gopinathan and Ilya Sergey. Certifying certainty and uncertainty in approximate membership query structures. In Shuvendu K. Lahiri and Chao Wang, editors, CAV, volume 12225 of LNCS, pages 279-303. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_16.
  23. Peter J. Haas, Jeffrey F. Naughton, S. Seshadri, and Lynne Stokes. Sampling-based estimation of the number of distinct values of an attribute. In Umeshwar Dayal, Peter M. D. Gray, and Shojiro Nishio, editors, VLDB, pages 311-322. Morgan Kaufmann, 1995. URL: http://www.vldb.org/conf/1995/P311.PDF.
  24. Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal. Approximate relational reasoning for higher-order probabilistic programs. Proc. ACM Program. Lang., 9(POPL):1196-1226, 2025. URL: https://doi.org/10.1145/3704877.
  25. Maximilian P. L. Haslbeck and Tobias Nipkow. Verified analysis of list update algorithms. In Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen, editors, FSTTCS, volume 65 of LIPIcs, pages 49:1-49:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2016.49.
  26. Stefan Heule, Marc Nunkesser, and Alexander Hall. HyperLogLog in practice: algorithmic engineering of a state of the art cardinality estimation algorithm. In Giovanna Guerrini and Norman W. Paton, editors, EDBT, pages 683-692. ACM, 2013. URL: https://doi.org/10.1145/2452376.2452456.
  27. Wassily Hoeffding. Probability inequalities for sums of bounded random variables. Journal of the American Statistical Association, 58(301):13-30, March 1963. URL: https://doi.org/10.2307/2282952.
  28. Joe Hurd. Formal verification of probabilistic algorithms. Technical Report UCAM-CL-TR-566, University of Cambridge, Computer Laboratory, 2003. URL: https://doi.org/10.48456/tr-566.
  29. Kumar Joag-Dev and Frank Proschan. Negative association of random variables with applications. Annals of Statistics, 11:286-295, 1983. URL: https://doi.org/10.1214/AOS/1176346079.
  30. Daniel M. Kane, Jelani Nelson, and David P. Woodruff. An optimal algorithm for the distinct elements problem. In Jan Paredaens and Dirk Van Gucht, editors, PODS, pages 41-52. ACM, 2010. URL: https://doi.org/10.1145/1807085.1807094.
  31. Emin Karayel. Formalization of randomized approximation algorithms for frequency moments. In June Andronick and Leonardo de Moura, editors, ITP, volume 237 of LIPIcs, pages 21:1-21:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.ITP.2022.21.
  32. Emin Karayel. An embarrassingly parallel optimal-space cardinality estimation algorithm. In Nicole Megow and Adam D. Smith, editors, APPROX/RANDOM, volume 275 of LIPIcs, pages 35:1-35:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.APPROX/RANDOM.2023.35.
  33. Emin Karayel. Negatively associated random variables. Archive of Formal Proofs, January 2025. , Formal proof development. URL: https://isa-afp.org/entries/Negative_Association.html.
  34. Emin Karayel, Derek Khu, Kuldeep S. Meel, Yong Kiam Tan, and Seng Joe Watt. Verification of the CVM algorithm with a new recursive analysis technique. Archive of Formal Proofs, February 2025. , Formal proof development. URL: https://isa-afp.org/entries/CVM_Distinct_Elements.html.
  35. Donald E. Knuth. The CVM algorithm for estimating distinct elements in streams, 2023. Accessed: 2025-01-14. URL: https://www-cs-faculty.stanford.edu/~knuth/papers/cvm-note.pdf.
  36. Andrey Kofnov, Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, and Efstathia Bura. Moment-based invariants for probabilistic loops with non-polynomial assignments. In Erika Ábrahám and Marco Paolieri, editors, QEST, volume 13479 of LNCS, pages 3-25. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-16336-4_1.
  37. Andreas Lochbihler. Probabilistic functions and cryptographic oracles in higher order logic. In Peter Thiemann, editor, ESOP, volume 9632 of LNCS, pages 503-531. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_20.
  38. Annabelle McIver and Carroll Morgan. Probabilistic loops: Invariants and variants, pages 37-78. Springer, New York, NY, 2005. URL: https://doi.org/10.1007/0-387-27006-X_2.
  39. Michael Mitzenmacher and Eli Upfal. Probability and Computing: Randomization and Probabilistic Techniques in Algorithms and Data Analysis. Cambridge University Press, USA, 2nd edition, 2017. Google Scholar
  40. Rajeev Motwani and Prabhakar Raghavan. Randomized Algorithms. Cambridge University Press, 1995. URL: https://doi.org/10.1017/CBO9780511814075.
  41. Steve Nadis. Computer scientists invent an efficient new way to count, 2024. Accessed: 2025-01-14. URL: https://www.quantamagazine.org/computer-scientists-invent-an-efficient-new-way-to-count-20240516.
  42. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  43. Seth Pettie and Dingyu Wang. Information theoretic limits of cardinality estimation: Fisher meets Shannon. In Samir Khuller and Virginia Vassilevska Williams, editors, STOC, pages 556-569. ACM, 2021. URL: https://doi.org/10.1145/3406325.3451032.
  44. Robert H. Morris Sr. Counting large numbers of events in small registers. Commun. ACM, 21(10):840-842, 1978. URL: https://doi.org/10.1145/359619.359627.
  45. Daniel Stüwe and Manuel Eberl. Probabilistic primality testing. Archive of Formal Proofs, 2019. , Formal proof development. URL: https://isa-afp.org/entries/Probabilistic_Prime_Tests.html.
  46. Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel. Formally certified approximate model counting. In Arie Gurfinkel and Vijay Ganesh, editors, CAV, volume 14681 of LNCS, pages 153-177. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_8.
  47. Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, and Jean-Baptiste Tristan. A formal proof of PAC learnability for decision stumps. In Catalin Hritcu and Andrei Popescu, editors, CPP, pages 5-17. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439917.
  48. Seng Joe Watt, Derek Khu, Emin Karayel, Kuldeep S. Meel, and Yong Kiam Tan. Verification of the CVM algorithm with the transformation-based proof. URL: https://archive.softwareheritage.org/swh:1:dir:7df92f0347e7bd150efef42e3edbbde0037498cc;origin=https://github.com/joewatt95/CVM;visit=swh:1:snp:90c68a9518ce6768c54e4596003838d7d6579cc3;anchor=swh:1:rev:6bba527562c6911c664586df83e2fdeeadbd869a;path=/isabelle/CVM_Transforms/.URL: https://archive.softwareheritage.org/swh:1:dir:7df92f0347e7bd150efef42e3edbbde0037498cc;origin=https://github.com/joewatt95/CVM;visit=swh:1:snp:90c68a9518ce6768c54e4596003838d7d6579cc3;anchor=swh:1:rev:6bba527562c6911c664586df83e2fdeeadbd869a;path=/isabelle/CVM_Transforms/ .
    Software Heritage Logo archived version
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact