Formalization of Complexity Analysis of the First-order Optimization Algorithms
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要