![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Case Study: Verifying an Efficient Algorithm to Compute Bernoulli Numbers
![]() Case Study: Verifying an Efficient Algorithm to Compute Bernoulli NumbersAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact nobody. BPRW03 - Big proof: formalizing mathematics at scale 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) 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^8). We give a fully 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. This talk is part of the Isaac Newton Institute Seminar Series series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsC2:AD Seminars Department of Archaeology - Conferences and Workshops Laing O'Rourke Centre SeminarsOther talksMultiscale Organization of Neuronal Activity Unifies Scale-Dependent Theories of Brain Function Bayesian regression discontinuity design with unknown cut-off Chalk talk Homotopy theory of lattices Structure Prediction and Design using AlphaFold |