精读笔记
Problem Setting
这篇论文实际处理的是 PEP-based optimization proof discovery 中的“第二阶段问题”：不是证明 bound 是否成立，而是在已成立的 bound 的 dual certificate family 中寻找一个更简单、更可解释、更可复用的代表。
困难点在于 PEP dual certificate 本质上是一个数值代数对象：multipliers 多、slack dense、解不唯一，且通常只在固定 N、固定参数、固定 formulation 下可读。它和人类证明之间缺少一层结构压缩：哪些 interpolation inequalities 是真正承载 proof 的，哪些只是数值 solver 为满足 PSD slack 随手摊开的冗余。
以前 PEP 工作的瓶颈不是 tightness，而是 interpretability。PEP 能给出 worst-case bound 和可验证 dual certificate，但证书本身不一定能迁移成 theorem proof、Lyapunov function 或 reusable lemma。关键矛盾是：机器最容易产生的是 dense certificate，而研究者真正需要的是 sparse, modular, pattern-level proof structure。
Motivation
已有路线的不足很明确：PEP/SDP 负责“证真”，但不负责“解释证明”。一个 dual feasible point 可以 certify rate，却可能完全隐藏证明机制。对于优化理论研究者，真正有价值的往往不是某个数值 bound，而是能否看出 telescoping、Lyapunov decrement、curvature weakening、active interpolation pattern 这类可迁移结构。
作者的核心观察是 dual certificates 非唯一：同一个 PEP、同一个 target rate 下存在大量等价证书。既然 solver 返回的只是其中一个任意点，那么可以在 certificate space 内继续优化另一个目标：proof simplicity。
关键缺口是缺少一个系统方法，把 dense numerical certificate 蒸馏成 proof ingredients。传统上这一步靠人工观察 multiplier pattern、猜 Lyapunov function、重写 residual；本文把这一步显式建模为 sparse optimization / SDP post-processing。
Core Idea
论文的核心思想是：把“简单证明”视为同一 theorem 的不同 certificate representation 中的稀疏结构选择问题。PEP dual identity 本来就把目标 gap 写成若干 valid inequalities 加 PSD residual 的非负组合；因此 proof complexity 可以直接落到 multiplier support 和 residual decomposition 上。
这个建模方式改变了信息流：过去是从算法和函数类直接推 proof；这里是先让 PEP 生成一个证书空间，再在证书空间中寻找人类可读结构。新的 inductive bias 是 sparsity 和 modularity：少量 active hypotheses、低复杂 residual、显式 intermediate lemma。它本质上不是更强的 PEP，而是对 PEP 输出的 representation alignment。
和 prior 的本质区别在于，已有 PEP 工作主要优化 rate 或自动找 certificate；本文优化 certificate 的形状。它不是提出新的 first-order method，也不是新的 worst-case analysis framework，而是把 proof simplification 变成一个可计算的二级优化问题。
Method
第一，定义 proof identity 的复杂度。目标 bound 写成 initialization-performance gap = 非负 interpolation inequalities + 非负 residuals。active hypothesis set 和 active residual set 成为 proof complexity 的 proxy。这一步解决的是“简单性不可优化”的问题，把 proof aesthetics 转成 support selection。
第二，做 sparsification。小实例用 exhaustive subset search，直接测试某个 active pattern 是否还能 certify 目标 rate；大实例用 weighted l1、log-sum、normalized log-sum、capped-l1 等 surrogate。它解决的是 dense multipliers 的问题，核心变化是从求任意 feasible certificate 变成在 feasible certificate set 中偏向 sparse support。
第三，允许扩展 hypothesis set。作者强调先加入冗余但 valid 的 inequalities，之后再稀疏化。这看似反直觉，但机制上很重要：更大的 dictionary 可能包含更接近人类 proof step 的 atoms，使最终表示更短。
第四，candidate-lemma SDP。它搜索由已有 hypotheses 和 PSD residual 组合出的新 valid inequality，并允许这些新 inequality 作为中间引理进入终端证明。它解决的是“只靠原始 pairwise interpolation atom 不够 modular”的问题；核心变化是从 flat certificate 转为 two-level proof：先证明 lemma，再用 lemma 证明 rate。
Key Insight / Why It Works
最关键的 insight 是：PEP dual certificate 已经包含证明的全部代数信息，只是坐标系不对。dense certificate 并不意味着证明本身复杂，可能只是 solver 在一个不利 basis 中返回了非稀疏表示。sparsification 和 candidate lemma search 的作用，是在同一个 cone/affine feasible set 内寻找更好的 basis representation。
真正有效的部分大概率是两个 inductive biases：support sparsity 和 derived-lemma modularity。support sparsity 能恢复“哪些 interpolation inequalities 真正必要”；derived lemma search 能把一堆局部 inequalities 合成为 Lyapunov decrement 或 fitted interpolation inequality。这比单纯 l1 后处理更强，因为它允许改变 proof granularity。
GD 的 fitted curvature 例子说明了一个很有意思的机制：简单证明不一定使用原始最强函数类参数，而是使用一个更弱但更匹配 stepsize 的 larger class。也就是说，proof simplification 可能来自“放松局部 hypotheses，使 residual 变简单”，而不是更精细地使用全部信息。这是可迁移 insight。
Proximal 部分是论文最有说服力的地方：candidate-lemma SDP 恢复 Lyapunov potential/decrement，而不是只减少 multiplier 数量。这说明方法有机会发现中间结构，而不仅是做稀疏回归式剪枝。
FGM 部分更像支持性证据。normalized log-sum/capped-l1 比 plain l1 好，主要说明 scaling matters；增益来源不清，可能很大程度来自 multiplier normalization 和已知 active pattern 的结构先验，而不是一个普适的 proof simplifier。
整体判断：本文的核心贡献不是 engineering scaling，而是把 certificate simplification 形式化为优化问题，并展示了 sparse/lemma inductive bias 可以从 PEP dual 中抽出人类证明结构。engineering 成分主要在具体 heuristic、normalization、threshold 和 case-specific SDP 模板。
Relation To Prior Work
它最接近 PEP、interpolation-based worst-case analysis、automatic Lyapunov discovery、以及 Goujaud/Taylor 系列关于 fundamental proof structures 的工作。技术谱系上，它不是传统 symbolic theorem proving，而是 convex optimization certificate post-processing。
和经典 PEP 的差异：PEP 关心 primal worst-case value 和 dual certificate feasibility；本文关心 dual feasible set 内的证书选择。换句话说，PEP 给出“存在证明”，本文试图找“好证明”。
和自动 Lyapunov 搜索的关系更微妙。proximal 例子中，candidate lemma search 实际上在做 Lyapunov function discovery，只是它从 PEP dual decomposition 出发，而不是直接参数化 potential。看似新的一部分是 sparse optimization 语言，但 l1/log-sum/capped-l1 本身不是新技术；实质创新是把这些稀疏选择工具放进 PEP dual certificate space，并用它们组织 proof atoms。
和 formal proof / Lean 的关系目前偏愿景。本文确实降低了后续 formalization 的复杂度，但没有展示自动 formal proof pipeline。这里新增的信息是 proof pre-processing，而不是 end-to-end formalization。
Dataset / Evaluation
evaluation 是一组优化理论 case studies，不是大规模 benchmark。覆盖了 GD、FGM、proximal point、accelerated proximal point，场景上包括 smooth/strongly convex、smooth convex、convex proximal、monotone/saddle setting。对论文主张来说，这种覆盖比堆数值表更有意义，因为它检验的是能否从不同 PEP 结构中恢复 proof pattern。
GD 例子验证了 sparse certificate 和 fitted interpolation 的可解释性；FGM 例子验证 sparsity heuristic 能减少 active inequalities，但没有完全证明 scalability；proximal 例子验证 candidate lemma search 可恢复 Lyapunov proof，这是最强 evidence。
但 evaluation 的限制也明显：实例都相对小、结构已高度 PEP-friendly，并且作者对 candidate lemma family、hypothesis expansion、目标 relaxation 有相当多人工设计。benchmark 主要支持“这个 workflow 能在若干典型一阶优化证明中工作”，还不足以支持“通用自动简单证明发现器”。没有真实 deployment 问题，因为对象是理论证明；也没有证明对大型 horizon 或复杂 algorithm families 的稳定泛化。
Limitation
第一，方法成立依赖 exact finite-dimensional SDP reformulation 和有限 hypothesis form。没有这层 PEP/interpolation machinery，整个 certificate simplification 无从开始。
第二，简单性是表示依赖的。active multiplier 数量只在固定 dictionary 下有意义；加入不同 redundant inequalities 可能改变最稀疏证明。因此“最简单证明”不是 intrinsic object，而是相对于 chosen proof atoms 的最优表示。
第三，candidate lemma search 并不完全自动。文中虽然给出 SDP formulation，但 lemma slots、允许使用的 hypothesis subset、residual structure、目标 relaxation 都需要设计。方法可能只是把人工猜 Lyapunov 的问题转移为人工设计 lemma search space。文中未充分说明如何系统选择这些空间。
第四，scalability 仍是硬上限。exhaustive sparsification 指数复杂；l1 类 surrogate 可扩展一些，但在 SDP certificate space 中仍可能受规模限制。FGM 的 normalization 改善说明数值尺度非常关键，也意味着 heuristic 鲁棒性并不天然。
第五，泛化 claim 要克制。proximal 和 GD 的结果很漂亮，但它们本身有强结构和已知 proof archetype。方法是否能发现完全未知的 proof mechanism，还是主要在 rediscover known latent structure，文中证据不足。
第六，增益归因不总是清晰。FGM 中 normalized penalties 的提升可能主要来自 scaling；GD fitted curvature 依赖较强的 branchwise analytic structure；proximal lemma recovery 可能受 candidate form 的隐式监督影响。
Takeaway
- 1. PEP dual certificate 不应只被看作 correctness certificate，也可以看作 proof search space；这会改变自动优化理论发现的工作流。
- 2. 真正值得迁移的 insight 是：先用强系统生成 dense certificate，再用 sparse/modular inductive bias 做 representation distillation。
- 这一范式可迁移到 SOS proof、operator splitting certificates、control Lyapunov certificates 等领域。
- 3. “加入冗余 inequalities 再稀疏化”是重要策略。
一句话总结
这篇论文把 PEP 生成的稠密 dual certificate 重新定义为可优化的证明表示空间，用稀疏化和候选引理搜索把“证真”推进到“找可读证明”，属于 optimization certificate post-processing 向 proof synthesis 演化的一步。