面向带块结构优化问题的算法形式化
最优化与控制
2025-03-25 v1
摘要
块结构问题是数值优化和机器学习领域进步的核心。本文为此类设置下的两个关键算法的收敛分析提供形式化：块坐标下降（BCD）方法和交替方向乘子法（ADMM）。我们利用基于类型论的Lean4证明辅助器，构建一个严格的框架来形式化表示这些算法。对非光滑和非凸优化中至关重要的概念进行了形式化，尤其是次梯度，这一概念扩展了经典可微性以处理非光滑情形，以及Kurdyka-Lojasiewicz（KL）属性，这一属性为分析非凸情形下的收敛提供了 essential 工具。这些定义和性质对于相应的收敛分析至关重要。我们形式化了这些算法的收敛证明，表明我们的数据定义和结构是连贯且稳健的。这些形式化为分析更一般的优化算法的收敛奠定了基础。
引用
@article{arxiv.2503.18806,
title = {Formalization of Algorithms for Optimization with Block Structures},
author = {Chenyi Li and Zichen Wang and Yifan Bai and Yunxi Duan and Yuqing Gao and Pengfei Hao and Zaiwen Wen},
journal= {arXiv preprint arXiv:2503.18806},
year = {2025}
}