精读笔记

Problem Setting

这篇论文实际处理的是“证明转换问题”：从 PEP/SDP 产生的 tight convergence proof 中系统抽取 Lyapunov-style proof。困难不在于验证某个给定 potential 的下降，而在于从一个全局、密集、证书化的不等式组合中识别出局部、低维、可递推的势函数。以前路线要么靠专家猜 potential，要么在预设 template 内搜索；前者不可系统化，后者可能因 template 偏差而错过 tight bound。关键矛盾是：PEP proof 的搜索空间足够大所以能 tight，但表示形式不适合人读；Lyapunov proof 可读但结构先验太强、难以发现。

Motivation

已有 PEP 文献已经多次出现同一历史模式：先由计算机辅助找到 tight SDP certificate，几年后才有人手工重写成 Lyapunov proof，例如 OGM、OGM-G、APPM/OHM。这个滞后说明 tight proof 和 human-readable proof 之间不是缺少数学事实，而是缺少系统转换机制。作者的核心观察是，PEP 证书并非与 Lyapunov proof 无关；它本身就是由若干非正项组成的证明，只要能把这些项按“迭代层”分组，Lyapunov 结构可能自然浮现。缺口在于：如何判断哪种分组会产生简洁 potential，以及如何从证书矩阵中读出局部表达式。

Core Idea

核心思想是把 Lyapunov 函数定义为 PEP proof 中部分非正项的 partial sum。随着 k 增加，partial sum 纳入更多问题类不等式或 SOS 项，因此下降性自动来自这些基础不等式。这样，Lyapunov proof 的寻找被改写为一个证明分层问题：找到一串递增的 active-index subsets，使得每个 partial sum 既足够局部，又低秩、终端剩余简单。

这个视角的本质区别是：prior template-based Lyapunov search 是先假设 potential 的函数形式，再求可行系数；本文是先拿到 tight PEP certificate，再从它的矩阵 range 中反推出 potential 的局部基。它引入的 inductive bias 是“好的 Lyapunov proof 是 tight certificate 的低秩局部分解”。这比手工猜测更 systematic，也比固定 template 更不容易被错误 ansatz 限制。

Method

方法机制可以压缩为五步。第一，用户选择 PEP active inequalities/SOS 项的递增分层，用 partial sums 定义 V_k；这一步解决 monotonicity 的来源问题。第二，计算对应矩阵 V_k 的 rank，并检查 rank 是否跨 k 基本稳定、终端是否只剩极少不等式；这一步过滤掉虽正确但不可读的证书重排。第三，构造候选局部向量集合，包括迭代点、梯度/算子值、固定点、辅助变量及其 pairwise differences；这一步把“局部性”转成线性代数搜索。第四，检查候选集合是否包含 Range(V_k) 的基；若缺一个方向，则用 basis completion 构造辅助序列，这解释了为什么某些 Lyapunov proof 需要 z_k 之类变量。第五，在发现 skeleton 后，用解析 multipliers 解符号恒等式，得到任意 N、任意 k 的闭式 Lyapunov function。关键不是实现，而是把 proof discovery 拆成“数值结构发现 + 符号证明闭合”。

Key Insight / Why It Works

最核心的 insight 是：PEP dual certificate 本质上已经是一个完备证明，只是其“时间结构”被 SDP 表示抹平了。Lyapunov proof 不是另一种证明，而是同一个 certificate 在迭代维度上的分层投影。只要分层后每个 partial sum 的矩阵 range 低秩，它就能被少量局部向量表达，于是变成人类熟悉的 potential。

最可能的核心贡献是 rank/range/local-basis 这套解释机制。partial sum 本身并不新，文中也承认与 Goujaud et al. 的 note 有联系；真正推进在于把“何时 partial sum 是好的 Lyapunov”形式化为 rank consistency、sufficiency、locality，并给出可执行流程。basis completion 也很有价值，因为它解释了辅助变量不是任意引入的，而是 Range(V_k) 中缺失方向的坐标化。

哪些部分可能只是 engineering：Jupyter notebook、PEPFlow tagging、sympy verification 更多是 workflow 贡献，不是理论核心。新 proof 的发现部分有实质价值，但增益主要来自“更好地读取已有 tight certificate”，不是新的 optimization inequality。Dual-OC-Halpern 是最强的新结果，因为它不只是重写 proof，而是借由证书结构发现了一个新 exact optimal algorithm；但它背后是否来自更一般的 H-duality，文中未充分说明。

Relation To Prior Work

最接近的路线有三条。第一是 PEP/SDP dual certificate 文献，本文直接建立在它之上；不同点是它不满足于 certificate 作为证明终点，而是把 certificate 当作 Lyapunov proof 的原材料。第二是 AutoLyap/IQC/template SDP 路线；这些方法搜索预设 quadratic potential，本文则从 tight PEP proof 反向抽取 potential，因此更少受 ansatz 限制。第三是已有手工 Lyapunov analyses，例如 OGM、OGM-G、OHM/FEG 系列；本文显示这些看似不同的 proof 可以被统一解释为同一 partial-sum/range-basis 机制。

看似新的地方中，partial sum 作为思想并非完全新；真正新增的是 admissibility criteria、local basis detection、basis completion，以及系统覆盖多个问题类。它属于 computer-assisted proof synthesis 的技术谱系，但方向不是“自动证明一个 rate”，而是“把机器证明翻译成人类 proof”。

Dataset / Evaluation

这里没有传统 dataset；evaluation 是数学案例集与开源 notebook workflow。覆盖范围相当广：smooth convex minimization、Bregman composite minimization、proximal monotone inclusion、strongly monotone/contractive fixed point、smooth minimax via monotone-Lipschitz operators。它验证了框架能复现多个历史上独立发展的 Lyapunov proof，并能产生四个新 analytic Lyapunov-style proofs，其中 Dual-OC-Halpern 还对应新 exact optimal algorithm。

但 evaluation 的性质要看清：这不是对自动化能力的统计验证，而是 curated case studies。它支持“该机制能统一许多重要例子”，但不足以支持“给任意 PEP proof 都能自动转 Lyapunov”。候选 basis construction 和 partial-sum choice 仍带有人为 insight。某些 setting，例如 monotone-Lipschitz operator，没有完整 interpolation theorem，因此 tightness claim 是相对于使用的 inequality proof class，而不必然是原问题类的 worst-case tightness。

Limitation

最大限制是 procedure 不是完备算法。Step 1 的分层需要用户提出；Step 3 的候选向量集合是 heuristic；Step 4 若找不到足够多局部基就 abort。也就是说，方法把“猜 Lyapunov 函数”转化成“猜/搜索正确 proof stratification 和局部 basis”，难度下降但没有消失。

另一个限制是对 PEP certificate 的依赖很重。若 PEP 规模过大、certificate 不稳定、SOS decomposition 非唯一、解析公式难以从数值中识别，流程就会卡住。GD 的 reverse-basis LDL decomposition 就说明，有时关键在于选对 PSD 分解；这一步本身可能相当脆弱。rank ≤ 4 的 conciseness 标准是经验性的，文中未充分说明其理论边界。

泛化上限也明确：当前不覆盖 block structure、long/silver/fractal stepsize、ergodic averaging/Jensen 型终端证明等。对这些方法，证明层未必线性跟随迭代编号，partial-sum admissibility 可能需要重写。新算法 Dual-OC-Halpern 的 exact optimality 很有意思，但更一般的 duality 原理没有建立，因此目前更像一个由框架发现的强例子，而不是完整理论闭包。

Takeaway

• 第一，PEP certificate 应该被看作 proof latent structure，而不是最终证明文本；Lyapunov proof 是对该 latent structure 的低秩局部解码。
• 第二，未来的自动 Lyapunov discovery 可能不应从 potential template 开始，而应从 tight certificate 的 range geometry 开始。
• 第三，辅助序列的出现可以被解释为 basis completion，这个 insight 可迁移到其他需要人为引入 momentum/anchor/dual variables 的证明。
• 第四，真正值得推进的是 partial-sum ordering、canonical SOS decomposition、local basis search 的自动化和完备性理论，而不是继续堆更多手工 notebook。

一句话总结

这篇论文把 Lyapunov 分析从“猜 potential 的艺术”推进为“从 tight PEP 证书中解码低秩局部 proof structure”的系统方法，是 computer-assisted optimization proof 从数值证书走向可解释解析证明的一步。