A verified LLL algorithm

Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada

Research output: Contribution to journalArticle

Abstract

The Lenstra-Lenstra-Lovász basis reduction algorithm, also known as LLL algorithm, is an algorithm to find a basis with short, nearly orthogonal vectors of an integer lattice. Thereby, it can also be seen as an approximation to solve the shortest vector problem (SVP), which is an NP-hard problem, where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm also possesses many applications in diverse fields of computer science, from cryptanalysis to number theory, but it is specially well-known since it was used to implement the first polynomial-time algorithm to factor polynomials. In this work we present the first mechanized soundness proof of the LLL algorithm to compute short vectors in lattices. The formalization follows a textbook by von zur Gathen and Gerhard.
LanguageEnglish
JournalArchive of Formal Proofs
Volume2018
StatePublished - 2018

Fingerprint

Polynomials
Number theory
Textbooks
Computer science
Computational complexity

Cite this

Divasón, J., Joosten, S., Thiemann, R., & Yamada, A. (2018). A verified LLL algorithm. Archive of Formal Proofs, 2018.
Divasón, Jose ; Joosten, Sebastiaan ; Thiemann, René ; Yamada, Akihisa. / A verified LLL algorithm. In: Archive of Formal Proofs. 2018 ; Vol. 2018.
@article{538865f8952144f7aeb4e557a620aad4,
title = "A verified LLL algorithm",
abstract = "The Lenstra-Lenstra-Lov{\'a}sz basis reduction algorithm, also known as LLL algorithm, is an algorithm to find a basis with short, nearly orthogonal vectors of an integer lattice. Thereby, it can also be seen as an approximation to solve the shortest vector problem (SVP), which is an NP-hard problem, where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm also possesses many applications in diverse fields of computer science, from cryptanalysis to number theory, but it is specially well-known since it was used to implement the first polynomial-time algorithm to factor polynomials. In this work we present the first mechanized soundness proof of the LLL algorithm to compute short vectors in lattices. The formalization follows a textbook by von zur Gathen and Gerhard.",
author = "Jose Divas{\'o}n and Sebastiaan Joosten and Ren{\'e} Thiemann and Akihisa Yamada",
year = "2018",
language = "English",
volume = "2018",
journal = "Archive of Formal Proofs",
issn = "2150-914x",
publisher = "SourceForge",

}

Divasón, J, Joosten, S, Thiemann, R & Yamada, A 2018, 'A verified LLL algorithm' Archive of Formal Proofs, vol 2018.

A verified LLL algorithm. / Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa.

In: Archive of Formal Proofs, Vol. 2018, 2018.

Research output: Contribution to journalArticle

TY - JOUR

T1 - A verified LLL algorithm

AU - Divasón,Jose

AU - Joosten,Sebastiaan

AU - Thiemann,René

AU - Yamada,Akihisa

PY - 2018

Y1 - 2018

N2 - The Lenstra-Lenstra-Lovász basis reduction algorithm, also known as LLL algorithm, is an algorithm to find a basis with short, nearly orthogonal vectors of an integer lattice. Thereby, it can also be seen as an approximation to solve the shortest vector problem (SVP), which is an NP-hard problem, where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm also possesses many applications in diverse fields of computer science, from cryptanalysis to number theory, but it is specially well-known since it was used to implement the first polynomial-time algorithm to factor polynomials. In this work we present the first mechanized soundness proof of the LLL algorithm to compute short vectors in lattices. The formalization follows a textbook by von zur Gathen and Gerhard.

AB - The Lenstra-Lenstra-Lovász basis reduction algorithm, also known as LLL algorithm, is an algorithm to find a basis with short, nearly orthogonal vectors of an integer lattice. Thereby, it can also be seen as an approximation to solve the shortest vector problem (SVP), which is an NP-hard problem, where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm also possesses many applications in diverse fields of computer science, from cryptanalysis to number theory, but it is specially well-known since it was used to implement the first polynomial-time algorithm to factor polynomials. In this work we present the first mechanized soundness proof of the LLL algorithm to compute short vectors in lattices. The formalization follows a textbook by von zur Gathen and Gerhard.

M3 - Article

VL - 2018

JO - Archive of Formal Proofs

T2 - Archive of Formal Proofs

JF - Archive of Formal Proofs

SN - 2150-914x

ER -

Divasón J, Joosten S, Thiemann R, Yamada A. A verified LLL algorithm. Archive of Formal Proofs. 2018;2018.