精读笔记

Problem Setting

[Formalization of Line Search Methods by Lean]（arXiv preprint / 2026）

这篇论文不是在解决一个新的 line search 算法问题，而是在解决 line search 理论的机器可验证化问题：如何把 Armijo、Goldstein、Wolfe、backtracking、非单调条件和 Zoutendijk theorem 这些经典非线性优化组件，组织成 Lean 4 中可检查、可复用、相互兼容的定义与证明。

真正困难点不在数学结论本身，而在形式化时会暴露 textbook proof 中被默认跳过的结构：使用的到底是哪种范数，梯度 Lipschitz 是存在某个 L 还是对所有 L，下降方向如何推出足够小步长存在，backtracking 的“终止”是可计算循环还是非构造性最小指数，Zoutendijk 中哪些非零性和下界条件必须显式出现。

以前相关形式化更多覆盖一阶凸优化复杂度、块结构方法、KKT 条件等；这些工作对 line search 这个“算法步长选择—全局收敛证明”的接口覆盖不足。因此这篇的关键矛盾是：优化算法分析高度依赖 line search 条件，但形式化库里缺少把这些条件可靠连接到下降性和 Zoutendijk 型收敛的基础层。

Motivation

已有路线不够的地方在于，它们验证了不少优化算法或最优性理论，但 line search 仍常被当成外部黑箱或 textbook lemma。对于后续想形式化 BFGS、Newton、非单调 Newton、一般非线性规划算法的人来说，这会成为重复成本最高、也最容易引入错误 axiom 的部分。

作者最有价值的观察是：line search 证明里很多“显然”其实不是 Lean 中的显然。例如 Mathlib 对 `Fin n → ℝ` 的默认范数不是优化理论中的欧氏范数；如果直接沿用，会导致欧氏范数平方恒等式和 Cauchy-Schwarz 不成立，只能错误地 axiom 化。又如一阶近似不能写成过强的严格线性下降式，否则对一般光滑凸函数都可能不满足。

所以这篇的动机不是提升优化效率，而是清理 formalization debt：把 line search 理论中依赖隐式语义的部分变成显式、局部、可组合的 Lean hypothesis / lemma。

Core Idea

核心思想可以概括为：把 line search 从“算法伪代码 + 人类证明习惯”改写为一套精确的逻辑接口。每个条件都是 predicate，每个分析跳步都是 lemma，每个数学存在性都显式对应 Lean 中的 witness 或 hypothesis。这样做的本质不是新增优化理论，而是重构理论的信息流：先建立正确的有限维欧氏几何，再用一阶近似保证局部 Armijo 可行性，再用 backtracking 的几何衰减把局部存在性转成离散指数存在性，最后用 Wolfe 曲率和 Lipschitz 梯度把单步下降下界接到 Zoutendijk 求和。

它与 prior 的本质区别在于 prior 更偏“验证具体一阶算法/复杂度/最优性条件”，而这里抽象的是步长选择这一层中间机制。这个层次很关键：许多非线性优化算法的全局收敛分析并不依赖方向如何生成的全部细节，而依赖方向满足 descent/Wolfe/angle 条件。因此 line search formalization 如果 API 设计得好，会比单个算法证明更可迁移。

Method

方法上最关键的不是模块数量，而是几处建模修正。

第一，自定义 `innerpro` 和 `vnorm`。这解决的是 Lean 默认空间结构与优化理论空间结构不一致的问题。没有这一步，后面的 Cauchy-Schwarz、`‖x‖² = <x,x>`、角度余弦定义都会建立在错误范数上。这是整篇里最基础也最实质的 formalization decision。

第二，把不可免费获得的分析性质显式参数化。`GradLipschitz grad L` 和 `FirstOrderApprox f grad` 都作为假设传入，而不是 axiom。它解决的是 arbitrary `f, grad` 下无法证明光滑性/一阶展开的问题，也避免把错误数学陈述写成全局公理。

第三，把 backtracking 的语义拆开：可执行层使用 `test : ℕ → Bool` 和 fuel recursion，数学层使用 `Nat.find` 定义最小满足 Armijo 的指数。这个拆分解决 Lean 中实数比较不可判定与数学 line search 需要最小成功步长之间的冲突。

第四，Zoutendijk 证明采用经典三段式：Armijo 给函数下降，Wolfe 曲率 + Lipschitz 梯度给步长下界，角度定义把方向导数平方归一化为 `cos² θ ‖∇f‖²`，再用有下界目标函数做 telescoping。这里的贡献是把这条分析链条形式化，而不是改进这条链条本身。

Key Insight / Why It Works

这篇真正有效的原因不是 scaling，也不是更强算法，而是 better specification。它把传统优化证明中最容易“看起来对、形式上错”的位置暴露出来并修正：范数错配、Lipschitz 量词错误、一阶近似过强、backtracking 终止性混淆、实数可判定性混淆。这些问题在人类论文里通常不影响阅读，但在 theorem prover 中会直接导致证明失败或错误 axiom。

最可能的核心贡献是欧氏几何层和假设管理层。尤其是指出 Mathlib 默认 sup norm 与优化理论欧氏范数不一致，这不是 engineering 小修，而是决定整个 formalization 是否数学正确的根基。`FirstOrderApprox` 的修正也很关键：用 Armijo 参数 `c1 ∈ (0,1)` 替代过强的严格一阶下降，避免形式化一个实际上不成立的 lemma。

backtracking 部分有一定 engineering 成分：`Bool` oracle + fuel loop 是 Lean 中处理不可判定实数比较的常见折中，数学上合理，但离 verified numerical implementation 还有距离。它更多证明了“如果存在可判定测试且测试 sound，循环能找到成功指数”，没有解决浮点 line search 与实数 Armijo 条件之间的 refinement。

Zoutendijk 部分是经典证明的形式化复现，技术含量在 proof engineering 和假设编排，而不是新的收敛 insight。需要注意的是，定理中 `hwolfe_all` 直接假设每步满足 Wolfe，这意味着 line search 找到 Wolfe step 的存在性并没有完全从算法推出；全局收敛结论的一部分难度被转移到了外部假设。

Relation To Prior Work

它最接近的是 Lean 中优化理论形式化谱系：Li et al. 的一阶凸优化复杂度形式化、块结构算法形式化、KKT/约束最优性形式化，以及 BICMR 的 optimization formalization platform。不同点在于这些工作更偏算法复杂度、结构化算法或最优性条件，而本文补的是非线性优化中 line search 条件与全局收敛分析的基础层。

从优化理论角度看，Armijo、Goldstein、Wolfe、Grippo、Zhang-Hager、Zoutendijk 都不是新思想；新意在于把它们组织成 Lean 可检查的定义和证明链。看似新的部分大多是已有理论的形式化重组，实质创新主要在 formal modeling choices：欧氏范数重建、假设局部化、backtracking 可计算/非计算语义拆分、Zoutendijk 证明依赖的条件显式化。

因此它属于“formal methods for mathematical optimization infrastructure”，不是“new optimization algorithm”。其价值应按库组件质量、假设干净程度、后续复用性来评价，而不是按优化性能来评价。

Dataset / Evaluation

这篇没有传统意义上的 dataset 或实验 benchmark。evaluation 主要是 proof artifact：作者展示 Lean 代码覆盖了多类 line search 条件、backtracking 语义、Zoutendijk theorem 及一个梯度范数趋小的 corollary。

这种 evaluation 能支持的 claim 是有限的：它支持“这些经典定义和部分收敛论证可以被 Lean 形式化”，但不能支持“形成了可部署的 verified optimizer”，也不能充分支持“可扩展到更复杂非线性规划算法”。文中没有系统比较 proof burden、复用接口设计、与 Mathlib/BICMR 现有库的整合难度，也没有展示一个完整高级算法如 BFGS/Newton 在该库上的端到端验证。

非单调条件的覆盖更像 definition-level evaluation：Grippo 和 Zhang-Hager 被定义，并给出若干性质，但没有强证据表明非单调 line search 的核心收敛机制已被完整形式化。

Limitation

核心限制是很多关键能力来自显式假设，而不是从更基础数学结构中推出。`FirstOrderApprox`、`GradLipschitz`、`hwolfe_all`、`hdesc_all`、`hgrad_ne_zero`、目标函数下界等都被作为外部条件携带。这样做形式上干净，但也说明当前库还没有把 differentiability、gradient correctness、line search existence、Wolfe step construction 完整闭合。

Zoutendijk theorem 的形式化尤其依赖 `hwolfe_all`：每一步 Wolfe 条件被假设成立，而不是由某个 verified Wolfe line search procedure 生成。这意味着全局收敛证明中最算法化的一环仍未完全验证。换句话说，论文验证了“若每步满足 Wolfe，则 Zoutendijk bound 成立”，但没有完全验证“所给 line search 算法确实产生满足 Wolfe 的步长”。

backtracking 的可执行性也有限。由于实数比较不可判定，实际可执行版本依赖布尔 oracle；这更像抽象接口，不是端到端数值程序验证。若要面向工程可靠性，还需要浮点误差、近似比较、termination fuel、oracle soundness 与实数规范之间的 refinement proof。

非单调 line search 的上限也明显：reference value 被抽象成参数，这提升泛化性，但也把 Grippo/Zhang-Hager 真正困难的序列性质和收敛控制转移给调用者。文中未充分说明这些非单调组件如何支撑完整收敛 theorem。

Takeaway

• 第一，形式化优化理论时，最值得优先清理的是“隐式数学结构”：范数、内积、可微性、一阶近似、比较可判定性。
• 这些不是实现细节，而是证明正确性的根。
• 第二，line search 是优化形式化中高杠杆的中间层。
• 它不像单个算法那样局部，也不像纯数学定理那样脱离实现；它正好连接算法更新与收敛证明，后续 BFGS/Newton/非单调方法都可能复用。

一句话总结

这篇论文在优化形式化谱系中的位置是：把经典 line search 与 Zoutendijk 收敛分析从 textbook proof 提升为 Lean 可检查的基础组件，贡献主要是规范化和 proof infrastructure，而不是新的优化算法。