General
This site provides supporting material for the paper A Verified Efficient Implementation of the LLL Basis Reduction Algorithm by Ralph Bottesch, Max W. Haslbeck, and René Thiemann.- The formalization in the paper is part of the archive of formal proofs, directory thys/LLL_Basis_Reduction. It compiles with Isabelle 2018.
- This archive contains the old and new verified Haskell code, the input lattices for the experiments, and an Isabelle-theory that has been used to extract the verified Haskell code.
Experimental Results
The experiments have been conducted as follows.
- Each input lattice input_n.txt contains n vectors of dimension n. The shape of each lattice is fixed, namely it corresponds to a lattice that stems from a polynomial factorization problem. In particular, the numbers in the lattice are either 0, 1, or a n-digit random number.
- All experiments have been conducted on an iMac Pro with 3.2 GHz and 64 GB RAM running macOS High Sierra.
-
The old and new verified Haskell code has been compiled with GHC version 8.2.1 using -O2.
Measurements are conducted using the command line tool time.
In order to generate short vectors in Mathematica (version 11.2.0), we basically invoke Timing[LatticeReduce[input]] within a running Mathematica session.
For the command line tool fplll (version 5.2.1) we again use time for measurement.
In the verified code (old and new) we set the value of the parameter α to 3/2, whereas for Mathematica and fplll we use their default settings (the default value for Mathematica appears to be undocumented, for fplll it is very close to 4/3). Smaller values of α lead to slightly better results.
The table displays the execution times in seconds of our experiments.
input lattice | old verified | new verified | Mathematica | fplll |
---|---|---|---|---|
input_5 | 0.02 | 0.02 | 0.00 | 0.01 |
input_10 | 0.07 | 0.02 | 0.01 | 0.01 |
input_15 | 0.72 | 0.04 | 0.04 | 0.01 |
input_20 | 6.84 | 0.12 | 0.09 | 0.01 |
input_25 | 20.43 | 0.27 | 0.19 | 0.02 |
input_30 | 80.45 | 0.77 | 0.43 | 0.04 |
input_35 | 276.19 | 1.95 | 0.90 | 0.09 |
input_40 | 594.71 | 4.03 | 1.71 | 0.17 |
input_45 | 1666.06 | 8.60 | 3.24 | 0.32 |
input_50 | 3084.39 | 15.69 | 5.20 | 0.53 |
input_55 | 6578.11 | 30.83 | 9.10 | 0.90 |
input_60 | 15599.50 | 60.14 | 14.89 | 1.47 |
input_65 | 20849.24 | 82.32 | 21.73 | 2.14 |
input_70 | 38782.21 | 138.69 | 33.53 | 3.16 |
input_75 | 93912.12 | 275.14 | 52.39 | 4.89 |
input_80 | 140896.27 | 419.77 | 78.66 | 6.80 |
input_85 | 192543.78 | 562.55 | 106.28 | 9.27 |
input_90 | 579173.96 | 1178.88 | 166.69 | 13.62 |
input_95 | 863539.92 | 1680.75 | 231.67 | 17.23 |
input_100 | 633105.25 | 1656.73 | 290.97 | 21.61 |