LIPIcs.ITP.2024.25.pdf
- Filesize: 0.74 MB
- 16 pages
Document
Formalizing the Cholesky Factorization Theorem
Authors
Carl Kwan 
,
Warren A. Hunt Jr.
-
Part of:
Volume:
15th International Conference on Interactive Theorem Proving (ITP 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-09-02
File
Document Identifiers
Author Details
Acknowledgements
We would like to thank Robert van de Geijn, Margaret Myers, and the anonymous reviewers for their helpful comments and feedback.
Cite AsGet BibTex
Carl Kwan and Warren A. Hunt Jr.. Formalizing the Cholesky Factorization Theorem. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.25
https://doi.org/10.4230/LIPIcs.ITP.2024.25
Abstract
We present a formal proof of the Cholesky Factorization Theorem, a fundamental result in numerical linear algebra, by verifying formally a Cholesky decomposition algorithm in ACL2. Our mechanical proof of correctness is largely automatic for two main reasons: (1) we employ a derivation which involves partitioning the matrix to obtain the desired result; and (2) we provide an inductive invariant for the Cholesky decomposition algorithm. To formalize (1), we build support for reasoning about partitioned matrices. This is a departure from how typical numerical linear algebra algorithms are presented, i.e. via excessive indexing. To enable (2), we build a new recursive recognizer for a matrix to be Cholesky decomposable and mathematically prove that the recognizer is indeed necessary and sufficient. Guided by the recognizer, ACL2 automatically inducts and verifies the Cholesky decomposition algorithm. We also present our ACL2-based formalization of the decomposition algorithm itself, and discuss how to bridge the gap between verifying a decomposition algorithm and proving the Cholesky Factorization Theorem. To our knowledge, this is the first formalization of the Cholesky Factorization Theorem.
Subject Classification
ACM Subject Classification
- Theory of computation → Automated reasoning
- Mathematics of computing → Computations on matrices
Keywords
- Numerical linear algebra
- Cholesky factorization theorem
- Matrix decomposition
- Automated reasoning
- ACL2
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- ACL2. Df: Support for floating-point operations. Accessed 2024-06-06. URL: https://cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____DF.
- ACL2. Loop$. Accessed 2024-06-06. URL: https://cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2____LOOP_42.
- ACL2. User manual for the ACL2 Theorem Prover and the ACL2 Community Books. Accessed 2023-07-12. URL: https://cs.utexas.edu/users/moore/acl2/current/manual/index.html.
- Stephen Boyd and Lieven Vandenberghe. Convex Optimization. Cambridge University Press, 2004. URL: https://doi.org/10.1017/CBO9780511804441.
- Robert S. Boyer and J. Strother Moore. Single-threaded objects in ACL2. In Proceedings of the 4th International Symposium on Practical Aspects of Declarative Languages, PADL '02, pages 9-27, Berlin, Heidelberg, 2002. Springer-Verlag. URL: https://doi.org/10.5555/645772.667953.
- Ruben Gamboa, John Cowles, and Jeff Van Baalen. Using ACL2 arrays to formalize matrix algebra, 2003. URL: https://cs.uwyo.edu/~ruben/static/pdf/matalg.pdf.
- Ruben A. Gamboa and Matt Kaufmann. Nonstandard analysis in ACL2. J. Autom. Reason., 27(4):323-351, November 2001. URL: https://doi.org/10.1023/A:1011908113514.
- John A. Gunnels, Fred G. Gustavson, Greg M. Henry, and Robert A. van de Geijn. FLAME: Formal linear algebra methods environment. ACM Trans. Math. Softw., 27(4):422-455, December 2001. URL: https://doi.org/10.1145/504210.504213.
- John Harrison. The HOL Light theory of Euclidean space. Journal of Automated Reasoning, 50:173-190, 2012. URL: https://doi.org/10.1007/s10817-012-9250-9.
- Joe Hendrix. Matrices in ACL2, 2003. URL: https://cs.utexas.edu/users/moore/acl2/workshop-2003/contrib/hendrix/hendrix.pdf.
- Matt Kaufmann and J Strother Moore. ACL2 home page. https://cs.utexas.edu/~moore/acl2/, 1997. Accessed 2024-06-25.
- Matt Kaufmann and J Strother Moore. ACL2 system and community books. https://github.com/acl2/acl2, 2014. Accessed 2024-06-25.
- Carl Kwan. Classical LU decomposition in ACL2. Electronic Proceedings in Theoretical Computer Science, 393:1-5, November 2023. URL: https://doi.org/10.4204/eptcs.393.1.
- Carl Kwan and Mark R. Greenstreet. Real vector spaces and the Cauchy-Schwarz inequality in ACL2(r). Electronic Proceedings in Theoretical Computer Science, 280:111-127, October 2018. URL: https://doi.org/10.4204/eptcs.280.9.
- Lean mathlib3 documentation: LDL decomposition. https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix/ldl.html. Accessed 2023-07-13.
- Lean mathlib3 documentation: Matrices. https://leanprover-community.github.io/mathlib_docs/data/matrix/basic.html. Accessed 2023-07-13.
- ZhengPu Shi and Gang Chen. Integration of multiple formal matrix models in Coq. In Wei Dong and Jean-Pierre Talpin, editors, Dependable Software Engineering. Theories, Tools, and Applications, pages 169-186, Cham, 2022. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-21213-0_11.
- Zhiping Shi, Yan Zhang, Zhenke Liu, Xinan Kang, Yong Guan, Jie Zhang, and Xiaoyu Song. Formalization of matrix theory in HOL4. Advances in Mechanical Engineering, 6:195-276, 2014. URL: https://doi.org/10.1155/2014/195276.
- Christian Sternagel and René Thiemann. Executable matrix operations on matrices of arbitrary dimensions. Archive of Formal Proofs, June 2010. , Formal proof development. URL: https://isa-afp.org/entries/Matrix.html.
- René Thiemann and Akihisa Yamada. Matrices, Jordan normal forms, and spectral radius theory. Archive of Formal Proofs, August 2015. , Formal proof development. URL: https://isa-afp.org/entries/Jordan_Normal_Form.html.