Formalization of Line Search Methods by Lean

技术摘要：利用 Lean 对线搜索方法进行形式化

问题陈述
本文探讨了对非线性优化理论进行严格机器验证的需求，特别侧重于线搜索方法。虽然现有的 Lean 定理证明器中的形式化工作已经涵盖了凸优化的一阶算法、块结构方法以及最优性条件（如 KKT 条件），但控制线搜索的具体理论框架——这对于基于梯度的迭代方法的全局收敛至关重要——仍有待形式化验证。作者旨在将标准的教科书定义、自适应步长选择策略以及收敛论证转化为可由机器检查的 Lean 代码，以消除歧义并确保正确性。

方法论
作者利用 Lean 4 并借助 Mathlib 库，对线搜索的数学基础和算法逻辑进行了形式化。其方法论包括：

1. 数学建模： 将向量空间 $\mathbb{R}^n$ 建模为从 Fin n 到 $\mathbb{R}$ 的函数。作者定义了一个自定义的欧几里得内积和范数 (vnorm)，而不是依赖于 Mathlib 提供的环境上确界范数（sup-norm），并将证明标准性质（如 Cauchy–Schwarz 不等式以及范数平方与内积之间的关系）作为定理而非公理。
2. 形式化假设： 关键假设（例如梯度的 Lipschitz 连续性和一阶近似性质（Taylor 展开行为））被定义为显式的谓词（GradLipschitz、FirstOrderApprox）而非公理，从而确保它们作为假设携带在定理中。
3. 算法形式化： 本文形式化了回溯线搜索（backtracking line search）的逻辑。考虑到在 Lean 的逻辑中实数比较是不可判定的，作者将 Armijo 测试抽象为一个布尔 Oracle（test : N → Bool）用于可执行定义 (backtrackRun)，同时使用 Nat.find 来识别满足条件的最小指数，从而证明满足条件的步长的数学存在性。
4. 收敛证明： 该方法论的核心在于证明 Zoutendijk 定理。这是通过推导每次迭代中函数下降量的下界（结合 Armijo、Wolfe 曲率和 Lipschitz 条件），并通过对这些下界求和，从而证明方向导数平方的级数是有限的。

核心贡献
本文对以下组件提供了全面的形式化：

• 基本定义： 关于下降方向、欧几里得内积和自定义欧几里得范数的形式化定义。
• 线搜索准则： 对以下内容提供了严谨的定义与证明：
  • Armijo 条件： 证明了满足充分下降条件的步长的存在性，及其对函数值严格减少的含义。
  • Goldstein 条件： 形式化了函数值的双重边界。
  • Wolfe 条件： 形式化了 Armijo（充分下降）条件和曲率条件，并证明了 Wolfe 条件蕴含 Armijo 条件。
  • 非单调条件： 形式化了 Grippo 条件（滑动最大值）和 Zhang-Hager 条件（前序值的凸组合），并证明了在特定参数极限下，这些条件会退化为标准的 Armijo 条件。
• 回溯实现： 一个经过验证的回溯线搜索算法实现，该实现保证了终止性以及生成的步长的正定性。
• Zoutendijk 定理： 一个经过机器验证的 Zoutendijk 定理证明，该定理确立了在满足 Wolfe 条件和 Lipschitz 连续梯度的条件下，梯度与搜索方向之间夹角余弦值的平方（由梯度范数加权）之和是有限的。
• 全局收敛： 在 Zoutendijk 可加性界限的假设下，证明了最速下降迭代的梯度范数收敛至零（具体表现为 $\liminf_{k \to \infty} \|\nabla f(x_k)\| = 0$）。

结果
该形式化成功验证了：

1. 下降方向保证了存在能使目标函数严格减少的步长。
2. 在 Armijo 条件引导下，回溯线搜索总能以一个有效的正步长终止。
3. 在 Lipschitz 连续梯度和 Wolfe 条件的假设下，Zoutendijk 定理成立，为收敛行为提供了严谨的界限。
4. 生成序列的梯度范数收敛至零，确认了该方法的全局收敛性。

意义
作者将这项工作定位为非线性优化机器验证的基础性步骤。通过提供可机器检查的线搜索理论定义与证明，本文：

• 补充了现有的关于一阶优化方法和最优性条件的各种形式化工作。
• 弥合了非正式教科书定义与可执行、经验证代码之间的鸿沟。
• 为更高级的非线性规划算法的验证开发建立了可复用的基础。
• 减少了标准优化论证中的歧义，推动该领域向形式化和机器可验证推理发展。

该形式化的代码已向社区开放，以支持进一步的研究与工程应用。