Formalization of Algorithms for Optimization with Block Structures
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866909550247936000 |
|---|---|
| author | Li, Chenyi Wang, Zichen Bai, Yifan Duan, Yunxi Gao, Yuqing Hao, Pengfei Wen, Zaiwen |
| author_facet | Li, Chenyi Wang, Zichen Bai, Yifan Duan, Yunxi Gao, Yuqing Hao, Pengfei Wen, Zaiwen |
| contents | Block-structured problems are central to advances in numerical optimization and machine learning. This paper provides the formalization of convergence analysis for two pivotal algorithms in such settings: the block coordinate descent (BCD) method and the alternating direction method of multipliers (ADMM). Utilizing the type-theory-based proof assistant Lean4, we develop a rigorous framework to formally represent these algorithms. Essential concepts in nonsmooth and nonconvex optimization are formalized, notably subdifferentials, which extend the classical differentiability to handle nonsmooth scenarios, and the Kurdyka-Lojasiewicz (KL) property, which provides essential tools to analyze convergence in nonconvex settings. Such definitions and properties are crucial for the corresponding convergence analyses. We formalize the convergence proofs of these algorithms, demonstrating that our definitions and structures are coherent and robust. These formalizations lay a basis for analyzing the convergence of more general optimization algorithms. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_18806 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formalization of Algorithms for Optimization with Block Structures Li, Chenyi Wang, Zichen Bai, Yifan Duan, Yunxi Gao, Yuqing Hao, Pengfei Wen, Zaiwen Optimization and Control G.1.6 Block-structured problems are central to advances in numerical optimization and machine learning. This paper provides the formalization of convergence analysis for two pivotal algorithms in such settings: the block coordinate descent (BCD) method and the alternating direction method of multipliers (ADMM). Utilizing the type-theory-based proof assistant Lean4, we develop a rigorous framework to formally represent these algorithms. Essential concepts in nonsmooth and nonconvex optimization are formalized, notably subdifferentials, which extend the classical differentiability to handle nonsmooth scenarios, and the Kurdyka-Lojasiewicz (KL) property, which provides essential tools to analyze convergence in nonconvex settings. Such definitions and properties are crucial for the corresponding convergence analyses. We formalize the convergence proofs of these algorithms, demonstrating that our definitions and structures are coherent and robust. These formalizations lay a basis for analyzing the convergence of more general optimization algorithms. |
| title | Formalization of Algorithms for Optimization with Block Structures |
| topic | Optimization and Control G.1.6 |
| url | https://arxiv.org/abs/2503.18806 |