Finding Simple Proofs for First-Order Optimization¶

会议: NeurIPS 2026
arXiv: 2607.08753
代码: https://github.com/DanielBergThomsen/simple-proofs
领域: 优化/理论
关键词: 一阶优化, 性能估计问题 (PEP), 证明简化, 稀疏优化, 候选引理 SDP

一句话总结¶

针对机器自动生成优化算法收敛性证书过于冗密且难以解释的问题，本文将寻找简洁证明形式化为在拉格朗日对偶证书上的二阶段稀疏优化与半定规划（SDP）搜寻问题，成功自动剔除冗余不等式并提炼出紧凑的李雅普诺夫函数。

研究背景与动机¶

在现代数学与计算机辅助理论研究中，仅获得真值证书往往是不够的，理论学者更需要结构透明、易于人类复查与扩展复用的证明骨架。性能估计问题（Performance Estimation Problems, PEP）及其半定规划（SDP）松弛技术近年来取得突破，能够通过数值求解精确刻画一阶优化方法在各类凸/强凸函数族下的最坏情况性能界。然而，数值求解器直接输出的拉格朗日对偶证书通常极其稠密，不仅与具体的超参数紧密耦合，还存在强烈的非唯一性，难以让研究者洞察收敛机理背后的核心归纳模式。

这种机器生成证书与理论理解之间的核心矛盾在于：数值 SDP 解盲目使用了插值不等式全集中的大量非零乘子，混杂了复杂的多点交叉项与高秩残差，掩盖了起决定性作用的核心假设与单步能量递减结构。现有工作主要依赖人工试错去猜测潜在的势函数或手动削减对偶乘子，面对步长变化或多步动量累积时往往力不从心。

本文的切入角度是：将证明简化本身视为建立在对偶证书集合上的二阶段优化问题，以显式度量指标（有效假设数与残差复杂度）驱动搜索。核心 idea：通过对对偶乘子施加带归一化的凹稀疏惩罚（Majorized Sparsification）与构建派生不等式的候选引理 SDP，从稠密数值证书中自主修剪冗余假设，并自动提取单步李雅普诺夫递减引理。

方法详解¶

整体框架¶

本文针对一阶优化问题 $\min_{x\in\mathbb{R}^d} f(x)$（其中 $f$ 属于特定函数类 $\mathcal{F}$），基于插值 PEP 框架将有限采样轨迹的对偶收敛证明形式化为两类非负项的线性组合：有效假设项（如两点插值不等式）与非负残差项（半正定松弛分解出的二次平方和）。整个简化流程分为三个阶段： 1. 基线对偶证书生成与松弛：求解原 PEP 对应的对偶 SDP，获取最优最坏情况比率 $\rho_\star$；随后设定微小的松弛界 $\bar{\rho}=(1+\varepsilon_{\mathrm{rel}})\rho_\star$，为对偶乘子腾出可压缩的搜索空间。 2. 假设稀疏化与支撑集筛选：在小规模问题上执行全排列子集枚举；在多步或大视界问题上，引入坐标尺度归一化的 Log-sum 或截断 $\ell_1$ 凹惩罚，借助逐次线性化（Majorized Minimization）迭代求解加权对偶 SDP，压零绝大部分冗余乘子。 3. 候选引理 SDP 提取与势函数重构：构建参数化派生不等式集合，通过求解联立的半定规划验证其自身有效性，并将选中的辅助不等式提升为独立中间引理，直接恢复局部李雅普诺夫函数。

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    A["初始一阶算法与函数类规范<br/>(PEP 对偶证书定义)"] --> B["阶段 1：对偶可行域松弛<br/>固定目标比率 ρ ⩽ (1+ε_rel)ρ_star"]
    B --> C["阶段 2： majorized 稀疏化启发式<br/>坐标归一化凹惩罚与加权迭代"]
    C --> D["阶段 3：候选引理 SDP 搜索<br/>提取派生不等式与单步递减项"]
    D --> E["紧凑符号证明结构<br/>(稀疏插值模式 / 紧凑李雅普诺夫引理)"]

关键设计¶

1. 基于有效模式的证明复杂度度量：为证明简洁性建立操作化数学定义 以往优化界证明往往缺乏定量度量标准。本文针对标准收敛恒等式： $$ \rho(N)\mathcal{I}f - \mathcal{P}f = \sum \lambda_h H_h + \sum}^r c_i R_i $$ 显式定义了两个离散复杂度指标：假设复杂度 $|\mathcal{A}^H(C)|$（对偶乘子 $\lambda_h > \varepsilon_{\mathrm{act}}$ 的有效不等式个数）与残差复杂度 $|\mathcal{A}^R(C)|$（正系数残差项 $c_i > \varepsilon_{\mathrm{act}}$ 的个数）。这一量化标准将“寻找直观证明”这一主观需求，直接转变为离散支撑集极小化的数学规划目标。

2. 逐次优化的凹惩罚稀疏化启发式：克服尺度差异造成的对偶乘子压缩失真 在面对多步快速梯度法等较大视界时，穷举子集搜索面临组合爆炸（NP-hard）。标准 $\ell_1$（Lasso）松弛对绝对幅值敏感，容易因不同采样点间乘子数量级差异数倍而保留稠密模式。本文采用带参考尺度 $M_h$ 的归一化 Log-sum 惩罚 $\phi_h(x) = \log(x/M_h + \delta)$ 与截断 $\ell_1$ 惩罚 $\phi_h(x) = \min\{\theta, x/M_h\}$。在每一轮迭代中计算超差分权重 $w_h^{[m+1]} \in \partial \phi_h(\lambda_h^{[m]})$，将非凸稀疏问题转化为带权凸 SDP 序列 $\min \sum_h w_h \lambda_h$，在几轮内稳定收敛到高稀疏度支撑集。

3. 候选引理半定规划（Candidate-Lemma SDP）：从机械求和中抽象出单步递减与李雅普诺夫势函数 当算法步数增加时，端到端求和证明往往隐藏了中间变量的演化规律。本文提出候选引理 SDP，预设一组由待定局部变量组成的辅助不等式 $\Psi_\kappa \geqslant 0$（其自身由允许的局部假设 $\mathcal{I}_\kappa$ 和残差非负张成）。通过变量吸收技巧消去双线性乘积项 $\zeta_h^{(\kappa)} = \eta_\kappa \alpha_h^{(\kappa)}$，构造完全线性的 SDP 约束，直接在凸规划中共同求解全局证明乘子与局部引理内部系数。该机制能够在不预设完整证明路径的前提下，自动识别出算法局部能量递减的李雅普诺夫函数。

一个完整示例¶

以单步梯度下降（GD）在强凸平滑函数类 $\mathcal{F}_{\mu, L}$ 上的收敛证明为例： - 原始数值状态：采样点集包含极小点 $x_\star$、初值 $x_0$ 及更新点 $x_1$。在未修剪时，两两之间共有 6 个非平庸的两点插值不等式 $H_{\mu, L}(x_i, x_j)$，数值求解器返回的 6 个乘子全部非零。 - 稀疏化过程：穷举稀疏化与候选引理 SDP 发现，只需保留 3 个有效假设即可保持收敛收缩因子 $\rho_\gamma = \max\{(1-\gamma\mu)^2, (\gamma L - 1)^2\}$ 不变，其余 3 个乘子严格归零。 - 提炼出的证明结构：进一步通过拟合曲率候选引理发现，原本复杂的残差可折叠为单项平方差，本质上等价于在一个放宽的函数类 $\mathcal{F}_{\mu_\gamma, L_\gamma}$ 上建立极简等式： $$ \rho_\gamma (f(x_0) - f_\star) - (f(x_1) - f_\star) = \lambda_{\star,0} H_{\mu_\gamma,L_\gamma}(x_\star,x_0) + \lambda_{\star,1} H_{\mu_\gamma,L_\gamma}(x_\star,x_1) + \lambda_{0,1} H_{\mu_\gamma,L_\gamma}(x_0,x_1) + R_\gamma $$ 其中残差收缩为极简的单秩形式 $R_\gamma = \frac{\gamma}{4\sqrt{\rho_\gamma}} \|\nabla f(x_0) + \nabla f(x_1) - \gamma\mu_\gamma L_\gamma (x_0 - x_\star)\|^2$。

实验关键数据¶

主实验¶

论文在三个典型优化场景验证了简化流程：快速梯度法（FGM）乘子稀疏化、单步梯度下降（GD）曲率拟合，以及近端点法（PPM）与加速近端点法（APPM）的李雅普诺夫函数提取。下表展示了 FGM 在视界 $N=3$ 下各稀疏化方法对有效插值假设数量的精简效果（候选总空间为 20 个两点插值不等式）。

方法 / 算法配置	目标比率与容差	有效假设数 (Active Hypotheses)	相对于原始稠密乘子压缩率	还原猜想结构一致性
原始数值对偶解 (Raw SDP)	$\rho_{\mathrm{rel}} = \frac{2L}{N^2+5N+2}$	16	0.0% (基线)	极差 (全稠密混杂)
普通 $\ell_1$ 惩罚 (Plain $\ell_1$)	$\rho_{\mathrm{rel}} = \frac{2L}{N^2+5N+2}$	8	50.0%	部分保留 (跨层冗余项)
Log-sum 启发式 (Log-sum)	$\rho_{\mathrm{rel}} = \frac{2L}{N^2+5N+2}$	8	50.0%	部分保留
归一化 Log-sum (Norm. Log-sum)	$\rho_{\mathrm{rel}} = \frac{2L}{N^2+5N+2}$	7	56.25%	极高 (仅多 1 个非零项)
截断 $\ell_1$ 启发式 (Capped $\ell_1$)	$\rho_{\mathrm{rel}} = \frac{2L}{N^2+5N+2}$	7	56.25%	极高 (仅多 1 个非零项)
穷举搜索 / 理论猜想 (Exhaustive / Conjecture)	$\rho_{\mathrm{rel}} = \frac{2L}{N^2+5N+2}$	6	62.5%	理论最优结构 ($2N$ 模式)

消融与代表性实例分析¶

针对单步梯度下降（GD，$\mu=0.1, L=1$）和近端点法（PPM），候选引理 SDP 提取出的核心参数与解析证明复杂度对比如下：

实验案例	原始分析形式	提取出的简化证明形式	复杂度变化与关键参数
单步 GD (步长 $\gamma \leqslant \frac{2}{L+\mu}$)	6 个插值项 + 复杂 3 项残差和 $R_\gamma^-$	3 个放宽类插值项 + 单平方残差 $R_\gamma$	拟合曲率 $(\mu_\gamma, L_\gamma) = (\mu, \frac{2}{\gamma}-\mu)$，残差从多项交叉合流为秩-1 项
单步 GD (步长 $\gamma \geqslant \frac{2}{L+\mu}$)	6 个插值项 + 复杂 3 项残差和 $R_\gamma^+$	3 个放宽类插值项 + 单平方残差 $R_\gamma$	拟合曲率 $(\mu_\gamma, L_\gamma) = (\frac{2}{\gamma}-L, L)$，自动匹配 Uschmajew-Vandereycken 弱强凸技巧
PPM 紧致次梯度界 ($\\|g_N\\|_{B^{-1}}$)	归纳法/高维端到端算子展开	局部李雅普诺夫势函数 $\mathcal{V}_k$	单步递减 $\mathcal{V}_k - \mathcal{V}_{k+1} \geqslant 0$ 完全解耦，直出 $\\|g_N\\|_{B^{-1}} \leqslant \frac{\Delta_0}{A_N}$
APPM 鞍点间隙界 ($\Phi(u_N, v_\star) - \Phi(u_\star, v_N)$)	稠密机器双线性验证	单调算子局部李雅普诺夫引理	导出 $\mathcal{V}_k - \mathcal{V}_{k-1} = -k(k-1)\beta \langle x_{k-1}-x_k, q_{k-1}-q_k \rangle \leqslant 0$

关键发现¶

对偶乘子尺度的归一化是连续松弛算法成败的核心：普通 $\ell_1$ 和未归一化的 Log-sum 在视界 $N \geqslant 3$ 时，因不同对偶不等式的物理量纲差异，过早将某些小幅值关键乘子截断，从而留下了 8 个非零项；而归一化 Log-sum 与截断 $\ell_1$ 能够将假设数稳定压至 7，极其逼近穷举法的极限 6。
放宽函数类曲率可显著净化残差：在 GD 实验中，候选引理自动搜索出的拟合曲率 $(\mu_\gamma, L_\gamma)$ 满足 $\gamma = 2/(\mu_\gamma + L_\gamma)$。在这一弱化后的函数类上，原始对偶证书中极其繁冗的三块平方残差合并成了单一紧致平方项，彻底消除了代数杂乱性。
机器可全自主发现非平凡李雅普诺夫函数：在无需人工设计势函数猜测公式的前提下，候选引理 SDP 成功在近端算法上合成出前人耗费大量精力才构造出的紧致势函数 $\mathcal{V}_k$。

亮点与洞察¶

将“证明简化”提升为规范化的二次数学规划：超越了“只要数值通过就算完事”的传统 PEP 视角，把证明可读性分解为“支持集基数”与“矩阵秩”，使证明简化成为可被数值优化的严谨流程。
归一化凹惩罚平替组合穷举：利用统计学习中的 Majorized Minimization 技术，在极短计算时间内实现了逼近 NP-hard 最优稀疏支撑集的性能，扫清了机器证明向大步数算法扩展的计算瓶颈。
自动搭建局部递减引理与李雅普诺夫桥梁：候选引理 SDP 不仅能压减既有条目，还能反向合成具有单步递减性质的未知泛函，极大缩短了计算机辅助发现到 Lean/Coq 形式化证明之间的距离。

局限与展望¶

搜索空间仍受限于预设项的形式：目前的候选引理 SDP 仍需事先指定允许参与引理的局部变量采样索引（如单步相邻项），对于跨越任意多步的复杂全局引理仍需较好的先验结构假设。
非凸目标目前依赖局部极小化：Majorized Sparsification 虽然经验上逼近最优解，但在极度病态的多极小对偶面中不能理论保证找到全局最小基数。
拓展方向：将该流水线直接与交互式定理证明器（如 Lean 4）的符号求解后端对接，实现从“PEP 数值求解 → 对偶证书稀疏化 → Lean 自动生成与检查代码”的端到端自动化。

评分¶

新颖性: ⭐⭐⭐⭐⭐ 首次系统性将证明简化形式化为对偶证书上的稀疏优化与引理 SDP 搜索。
实验充分度: ⭐⭐⭐⭐⭐ 涵盖 GD、FGM、PPM、APPM 四大经典范式，兼具穷举基准对比与解析闭式恢复。
写作质量: ⭐⭐⭐⭐⭐ 数学表达严谨，问题动机阐述极其透彻，对偶提升与符号吸收推导丝丝入扣。
价值: ⭐⭐⭐⭐⭐ 极大推进了计算机辅助最优化证明向透明化、模块化和形式化定理证明演进的步伐。

实验案例	原始分析形式	提取出的简化证明形式	复杂度变化与关键参数
单步 GD (步长 \(\gamma \leqslant \frac{2}{L+\mu}\))	6 个插值项 + 复杂 3 项残差和 \(R_\gamma^-\)	3 个放宽类插值项 + 单平方残差 \(R_\gamma\)	拟合曲率 \((\mu_\gamma, L_\gamma) = (\mu, \frac{2}{\gamma}-\mu)\)，残差从多项交叉合流为秩-1 项
单步 GD (步长 \(\gamma \geqslant \frac{2}{L+\mu}\))	6 个插值项 + 复杂 3 项残差和 \(R_\gamma^+\)	3 个放宽类插值项 + 单平方残差 \(R_\gamma\)	拟合曲率 \((\mu_\gamma, L_\gamma) = (\frac{2}{\gamma}-L, L)\)，自动匹配 Uschmajew-Vandereycken 弱强凸技巧
PPM 紧致次梯度界 (\(\\|g_N\\|_{B^{-1}}\))	归纳法/高维端到端算子展开	局部李雅普诺夫势函数 \(\mathcal{V}_k\)	单步递减 \(\mathcal{V}_k - \mathcal{V}_{k+1} \geqslant 0\) 完全解耦，直出 \(\\|g_N\\|_{B^{-1}} \leqslant \frac{\Delta_0}{A_N}\)
APPM 鞍点间隙界 (\(\Phi(u_N, v_\star) - \Phi(u_\star, v_N)\))	稠密机器双线性验证	单调算子局部李雅普诺夫引理	导出 \(\mathcal{V}_k - \mathcal{V}_{k-1} = -k(k-1)\beta \langle x_{k-1}-x_k, q_{k-1}-q_k \rangle \leqslant 0\)

方法 / 算法配置	目标比率与容差	有效假设数 (Active Hypotheses)	相对于原始稠密乘子压缩率	还原猜想结构一致性
原始数值对偶解 (Raw SDP)	\(\rho_{\mathrm{rel}} = \frac{2L}{N^2+5N+2}\)	16	0.0% (基线)	极差 (全稠密混杂)
普通 \(\ell_1\) 惩罚 (Plain \(\ell_1\))	\(\rho_{\mathrm{rel}} = \frac{2L}{N^2+5N+2}\)	8	50.0%	部分保留 (跨层冗余项)
Log-sum 启发式 (Log-sum)	\(\rho_{\mathrm{rel}} = \frac{2L}{N^2+5N+2}\)	8	50.0%	部分保留
归一化 Log-sum (Norm. Log-sum)	\(\rho_{\mathrm{rel}} = \frac{2L}{N^2+5N+2}\)	7	56.25%	极高 (仅多 1 个非零项)
截断 \(\ell_1\) 启发式 (Capped \(\ell_1\))	\(\rho_{\mathrm{rel}} = \frac{2L}{N^2+5N+2}\)	7	56.25%	极高 (仅多 1 个非零项)
穷举搜索 / 理论猜想 (Exhaustive / Conjecture)	\(\rho_{\mathrm{rel}} = \frac{2L}{N^2+5N+2}\)	6	62.5%	理论最优结构 (\(2N\) 模式)