Towards Verified Linear Algebra Programs Through Equivalence
summary
Extends the Coq mathcomp libraries with dot product, projection and basis theorems and uses them to mechanize Classical Gram‑Schmidt, proving nonzero outputs, pairwise orthogonality and span preservation; classical version proof is complete and a paper proof of the unique lemmas for Modified Gram‑Schmidt is formalized with the work‑in‑progress mechanization aiming to close exact Real equivalence by induction on k; plans include adapting lemmas to floating‑point error bounds and linking to low‑level reasoning frameworks and LGTM.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:42Verified linear algebra motivation
- 2:05Gram-Schmidt variants overview
- 3:49Classical vs modified Gram-Schmidt
- 5:54Numerical stability comparison
- 6:35Formalization challenges
- 7:40Linear algebra library in Coq
- 9:25Orthogonal decomposition theorem
- 10:06Classical Gram-Schmidt correctness
- 12:35Modified Gram-Schmidt correctness
- 13:36Future work
- 14:58Conclusion
- 16:29Q&A
related talks
55mProving Theorems and Certifying Programs with Coq
01mScale By the Bay 2021 intro video by Ryan Orendorff
01h 04mFrom Proofs to Algorithms for Machine Learning Problems
01h 04mSketching and Randomized Linear Algebra
18mA Verified Compiler for a Functional Tensor Language
32mRandomized Numerical Linear Algebra: Overview
20mTensor Algebra Equivalence Checker
27mAlmost-Orthogonal Bases for Inner Product Polynomials