Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL. (English) Zbl 1468.68309

Summary: The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has applications in number theory, computer algebra and cryptography. In this paper, we provide an implementation of the LLL algorithm. Both its soundness and its polynomial running-time have been verified using Isabelle/HOL. Our implementation is nearly as fast as an implementation in a commercial computer algebra system, and its efficiency can be further increased by connecting it with fast untrusted lattice reduction algorithms and certifying their output. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.


68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
11H06 Lattices and convex bodies (number-theoretic aspects)
11Y16 Number-theoretic algorithms; complexity
68V20 Formalization of mathematics in connection with theorem provers
Full Text: DOI


[1] Ballarin, C., Locales: a module system for mathematical theories, J. Autom. Reason., 52, 2, 123-153 (2014) · Zbl 1315.68218
[2] Bottesch, R., Divasón, J., Haslbeck, M., Joosten, S.J.C., Thiemann, R., Yamada, A.: A verified LLL algorithm. In: Archive of Formal Proofs (2018). http://isa-afp.org/entries/LLL_Basis_Reduction.html, Formal proof development · Zbl 1409.68252
[3] Bottesch, R., Haslbeck, M.W., Thiemann, R.: A verified efficient implementation of the LLL basis reduction algorithm. In: LPAR 2018, volume 57 of EPiC Series in Computing, pp. 64-180 (2018) · Zbl 1409.68252
[4] Cohen, C.: Construction of real algebraic numbers in Coq. In: ITP 2012, volume 7406 of LNCS, pp. 7-82 (2012) · Zbl 1360.68744
[5] Collins, G.E.: Factoring univariate integral polynomials in polynomial average time. In: EUROSAM 1979, volume 72 of LNCS (1979) · Zbl 0409.68021
[6] Divasón, J., Joosten, S.J.C., Kunčar, O., Thiemann, R., Yamada, A.: Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). In: CPP 2018, pp. 2-13. ACM (2018)
[7] Divasón, J.; Joosten, S.; Thiemann, R.; Yamada, A., A verified implementation of the Berlekamp-Zassenhaus factorization algorithm, J. Autom. Reason., 64, 699-735 (2020) · Zbl 1469.68165
[8] Divasón, J., Joosten, S.J.C., Thiemann, R., Yamada, A.: A formalization of the LLL basis reduction algorithm. In: ITP 2018, volume 10895 of LNCS, pp. 160-177 (2018) · Zbl 1468.68287
[9] Divasón, J., Joosten, S.J.C., Thiemann, R., Yamada, A.: A verified factorization algorithm for integer polynomials with polynomial complexity. In: Archive of Formal Proofs (2018). http://isa-afp.org/entries/LLL_Factorization.html, Formal proof development · Zbl 1468.68287
[10] Eberl, M.: Verified solving and asymptotics of linear recurrences. In: CPP 2019, pp. 27-37. ACM (2019)
[11] Eberl, M., Haslbeck, M.W., Nipkow, T.: Verified analysis of random binary tree structures. In: ITP 2018, volume 10895 of LNCS, pp. 196-214 (2018) · Zbl 1468.68288
[12] Erlingsson, U., Kaltofen, E., Musser, D.: Generic Gram-Schmidt orthogonalization by exact division. In: ISSAC 1996, pp. 275-282. ACM (1996) · Zbl 0914.65038
[13] Gonthier, G.: Point-free, set-free concrete linear algebra. In: ITP 2011, volume 6898 of LNCS, pp. 103-118 (2011) · Zbl 1342.68285
[14] Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: FLOPS 2010, volume 6009 of LNCS, pp. 103-117 (2010) · Zbl 1284.68131
[15] Harrison, J., The HOL light theory of Euclidean space, J. Autom. Reason., 50, 2, 173-190 (2013) · Zbl 1260.68373
[16] Joosten, SJC; Thiemann, R.; Yamada, A., A verified implementation of algebraic numbers in Isabelle/HOL, J. Autom. Reason., 64, 363-389 (2020) · Zbl 1468.68326
[17] Lenstra, AK; Lenstra, HW; Lovász, L., Factoring polynomials with rational coefficients, Math. Ann., 261, 515-534 (1982) · Zbl 0488.12001
[18] Li, W., Paulson, L.C.: A modular, efficient formalisation of real algebraic numbers. In: CPP 2016, pp. 66-75. ACM (2016)
[19] McCarthy, JA; Fetscher, B.; New, MS; Feltey, D.; Findler, RB, A Coq library for internal verification of running-times, Sci. Comput. Program., 164, 49-65 (2018)
[20] Micciancio, D., The shortest vector in a lattice is hard to approximate to within some constant, SIAM J. Comput., 30, 6, 2008-2035 (2000) · Zbl 0980.68054
[21] Nguyen, PQ; Vallée, B., The LLL Algorithm-Survey and Applications. Information Security and Cryptography (2010), Berlin: Springer, Berlin
[22] Nipkow, T.: Verified root-balanced trees. In: APLAS 2017, volume 10695 of LNCS, pp. 255-272 (2017)
[23] Nipkow, T.; Klein, G., Concrete Semantics (2014), Berlin: Springer, Berlin · Zbl 1410.68004
[24] Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer (2002) · Zbl 0994.68131
[25] Storjohann, A.: Faster algorithms for integer lattice basis reduction. Technical Report 249, Department of Computer Science, ETH Zurich (1996) · Zbl 0914.65043
[26] Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: TPHOLs’09, volume 5674 of LNCS, pp. 452-468 (2009) · Zbl 1252.68265
[27] Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle/HOL. In: CPP 2016, pp. 88-99. ACM (2016)
[28] van Hoeij, M., Factoring polynomials and the knapsack problem, J. Number Theory, 95, 167-189 (2002) · Zbl 1081.11080
[29] von zur Gathen, J.; Gerhard, J., Modern Computer Algebra (2013), Cambridge: Cambridge University Press, Cambridge · Zbl 1277.68002
[30] Wolfram Research, Inc.: Mathematica Version 11.3. Champaign, Illinois (2018)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.