Formalization of Complexity Analysis of the First-order Algorithms for Convex Optimization
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910536350826496 |
|---|---|
| author | Li, Chenyi Wang, Ziyu He, Wanyi Wu, Yuxuan Xu, Shengyang Wen, Zaiwen |
| author_facet | Li, Chenyi Wang, Ziyu He, Wanyi Wu, Yuxuan Xu, Shengyang Wen, Zaiwen |
| contents | The convergence rate of various first-order optimization algorithms is a pivotal concern within the numerical optimization community, as it directly reflects the efficiency of these algorithms across different optimization problems. Our goal is making a significant step forward in the formal mathematical representation of optimization techniques using the Lean4 theorem prover. We first formalize the gradient for smooth functions and the subgradient for convex functions on a Hilbert space, laying the groundwork for the accurate formalization of algorithmic structures. Then, we extend our contribution by proving several properties of differentiable convex functions that have not yet been formalized in Mathlib. Finally, a comprehensive formalization of these algorithms is presented. These developments are not only noteworthy on their own but also serve as essential precursors to the formalization of a broader spectrum of numerical algorithms and their applications in machine learning as well as many other areas. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_11437 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Formalization of Complexity Analysis of the First-order Algorithms for Convex Optimization Li, Chenyi Wang, Ziyu He, Wanyi Wu, Yuxuan Xu, Shengyang Wen, Zaiwen Optimization and Control Numerical Analysis G.1.6 The convergence rate of various first-order optimization algorithms is a pivotal concern within the numerical optimization community, as it directly reflects the efficiency of these algorithms across different optimization problems. Our goal is making a significant step forward in the formal mathematical representation of optimization techniques using the Lean4 theorem prover. We first formalize the gradient for smooth functions and the subgradient for convex functions on a Hilbert space, laying the groundwork for the accurate formalization of algorithmic structures. Then, we extend our contribution by proving several properties of differentiable convex functions that have not yet been formalized in Mathlib. Finally, a comprehensive formalization of these algorithms is presented. These developments are not only noteworthy on their own but also serve as essential precursors to the formalization of a broader spectrum of numerical algorithms and their applications in machine learning as well as many other areas. |
| title | Formalization of Complexity Analysis of the First-order Algorithms for Convex Optimization |
| topic | Optimization and Control Numerical Analysis G.1.6 |
| url | https://arxiv.org/abs/2403.11437 |