Document Open Access Logo

Verifying an Efficient Algorithm for Computing Bernoulli Numbers

Authors Manuel Eberl , Peter Lammich

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.35.pdf
  • Filesize: 0.92 MB
  • 19 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.35.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Bernoulli numbers
  • LLVM
  • verification
  • Isabelle
  • Chinese remainder theorem
  • modular arithmetic
  • Montgomery arithmetic

Metrics

Abstract

The Bernoulli numbers B_k are a sequence of rational numbers that is ubiquitous in mathematics, but difficult to compute efficiently (compared to e.g. approximating π).
In 2008, Harvey gave the currently fastest known practical way for computing them: his algorithm computes B_k mod p in time O(p log^{1 + o(1)} p). By doing this for O(k) many small primes p in parallel and then combining the results with the Chinese Remainder Theorem, one recovers the value of B_k as a rational number in O(k² log^{2 + o(1)} k) time. One advantage of this approach is that the expensive part of the algorithm is highly parallelisable and has very low memory requirements. This algorithm still holds the world record with its computation of B_{10⁸}.
We give a verified efficient LLVM implementation of this algorithm. This was achieved by formalising the necessary mathematical background theory in Isabelle/HOL, proving an abstract version of the algorithm correct, and refining this abstract version down to LLVM using Lammich’s Isabelle-LLVM framework, including many low-level optimisations. The performance of the resulting LLVM code is comparable with Harvey’s original unverified and hand-optimised C++ implementation.

Cite As Get BibTex

Manuel Eberl and Peter Lammich. Verifying an Efficient Algorithm for Computing Bernoulli Numbers. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.35

Author Details

Manuel Eberl
  • University of Innsbruck, Austria
Peter Lammich
  • University of Twente, Enschede, The Netherlands

Acknowledgements

The computational results presented here have been achieved (in part) using the LEO HPC infrastructure of the University of Innsbruck.

Supplementary Materials

References

  1. J. C. Adams. On the calculation of Bernoulli’s numbers up to B_62 by means of Staudt’s theorem. In Report of the meeting of the British Association for the Advancement of Science, Rep. Brit. Assn., pages 8-15, 1877. URL: https://gallica.bnf.fr/ark:/12148/bpt6k78160g.
  2. Shigeki Akiyama and Yoshio Tanigawa. Multiple zeta values at non-positive integers. The Ramanujan Journal, 5(4):327-351, 2001. URL: https://doi.org/10.1023/A:1013981102941.
  3. Richard P. Brent and David Harvey. Fast Computation of Bernoulli, Tangent and Secant Numbers, pages 127-142. Springer New York, 2013. URL: https://doi.org/10.1007/978-1-4614-7621-4_8.
  4. Lukas Bulwahn and Manuel Eberl. Bernoulli numbers. Archive of Formal Proofs, January 2017. Formal proof development. URL: https://isa-afp.org/entries/Bernoulli.html.
  5. Henri Cohen. Number Theory: Volume II: Analytic and Modern Tools. Graduate Texts in Mathematics. Springer New York, 2007. Google Scholar
  6. Manuel Eberl. Concrete bounds for Chebyshev’s prime counting functions. Archive of Formal Proofs, September 2024. Formal proof development. URL: https://isa-afp.org/entries/Chebyshev_Prime_Bounds.html.
  7. Manuel Eberl. Kummer’s congruence. Archive of Formal Proofs, March 2024. Formal proof development. URL: https://isa-afp.org/entries/Kummer_Congruence.html.
  8. Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In 2019 IEEE Symposium on Security and Privacy (SP), pages 1202-1219, 2019. URL: https://doi.org/10.1109/SP.2019.00005.
  9. Eugene Eric Kim and Betty Alexandra Toole. Ada and the first computer. Scientific American, 280(5):76-81, May 1999. URL: https://doi.org/10.1038/scientificamerican0599-76.
  10. Greg Fee and Simon Plouffe. An efficient algorithm for the computation of Bernoulli numbers, 2007. URL: https://arxiv.org/abs/math/0702300.
  11. Mathias Fleury and Peter Lammich. A more pragmatic CDCL for IsaSAT and targetting LLVM (short paper). In Brigitte Pientka and Cesare Tinelli, editors, Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings, volume 14132 of Lecture Notes in Computer Science, pages 207-219. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-38499-8_12.
  12. The GNU multiple precision arithmetic library. URL: https://gmplib.org/.
  13. Arnd Hartmanns, Bram Kohlen, and Peter Lammich. Efficient formally verified maximal end component decomposition for MDPs. In André Platzer, Kristin Yvonne Rozier, Matteo Pradella, and Matteo Rossi, editors, Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I, volume 14933 of Lecture Notes in Computer Science, pages 206-225. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-71162-6_11.
  14. David Harvey. A multimodular algorithm for computing Bernoulli numbers. Math. Comput., 79(272):2361-2370, 2010. URL: https://doi.org/10.1090/S0025-5718-2010-02367-1.
  15. M. Kaneko. The Akiyama-Tanigawa algorithm for Bernoulli numbers. Journal of Integer Sequences, 3, 2000. Google Scholar
  16. Donald E. Knuth and Thomas J. Buckholtz. Computation of tangent, Euler, and Bernoulli numbers. Mathematics of Computation, 21(100):663-688, 1967. URL: https://doi.org/10.1090/s0025-5718-1967-0221735-9.
  17. Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, and Peter Lammich. A formally verified IEEE 754 floating-point implementation of interval iteration for MDPs. CoRR, abs/2501.10127, 2025. URL: https://doi.org/10.48550/arXiv.2501.10127.
  18. Peter Lammich. Generating verified LLVM from Isabelle/HOL. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, volume 141 of LIPIcs, pages 22:1-22:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.22.
  19. Peter Lammich. Fast and verified UNSAT certificate checking. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, volume 14739 of Lecture Notes in Computer Science, pages 439-457. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63498-7_26.
  20. Peter Lammich. Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting. J. Autom. Reason., 68(3):14, 2024. URL: https://doi.org/10.1007/S10817-024-09701-W.
  21. Peter Lammich and Thomas Tuerk. Applying data refinement for monadic programs to Hopcroft’s algorithm. In Proc. of ITP, volume 7406 of LNCS, pages 166-182. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_12.
  22. D. H. Lehmer. An extension of the table of Bernoulli numbers. Duke Mathematical Journal, 2(3), September 1936. URL: https://doi.org/10.1215/s0012-7094-36-00238-7.
  23. Peter L. Montgomery. Modular multiplication without trial division. Mathematics of Computation, 44(170):519-521, 1985. URL: https://doi.org/10.1090/s0025-5718-1985-0777282-x.
  24. Joachim von zur Gathen and Jürgen Gerhard. Modern Computer Algebra. Cambridge University Press, 3rd edition, 2013. Google Scholar
  25. Christoph Walther. Formally verified Montgomery multiplication. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, volume 10982 of Lecture Notes in Computer Science, pages 505-522. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96142-2_30.
  26. Alexander Yee and Shigeru Kondo. 10 trillion digits of pi: A case study of summing hypergeometric series to high precision on multicore systems. Technical report, Siebel School of Computing and Data Science, 2011. URL: https://hdl.handle.net/2142/28348.
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