Sparse Certificates Turn Automated Bounds Into Simpler Proofs

Automated performance-estimation methods can certify convergence rates for first-order optimization algorithms, but the certificates they return are often too dense to serve as human proofs. This paper treats that gap as an optimization problem in its own right. Starting from Lagrangian dual certificates for performance estimation problems, the authors search for smaller certificate structures: fewer active inequalities, simpler residual patterns, and intermediate lemmas that expose the proof mechanism rather than only certify the final bound.

Core Contribution

The paper’s main contribution is a second-stage workflow for proof discovery. Prior performance-estimation work already showed how to find tight bounds by solving structured semidefinite programs. The new step asks which parts of those certificates are actually needed. The authors measure proof complexity through active hypotheses and residual structure, then apply sparse optimization and statistical-learning-style post-processing to prune the certificate.

That framing matters because a dual certificate is not the same object as a useful proof. A dense certificate may verify a rate, but it gives little guidance about which interpolation inequalities, monotonicity relations, or potential functions explain the result. The paper’s claim is narrower and more practical: a machine-generated certificate can be turned into a smaller proof sketch before a human or formal system finishes the argument.

Technical Approach

The workflow begins with a dual certificate from a performance estimation problem for a first-order method. The authors then search over simplified versions using three families of procedures: exhaustive sparsification, weighted $\ell_1$-type heuristics, and SDP formulations designed to discover intermediate lemmas. The objects being simplified are not algorithm iterates themselves, but the proof ingredients: active interpolation constraints, multipliers, and residual identities.

The appendix pages make the style of output concrete. For the accelerated proximal point method, the paper derives a saddle-gap certificate through an operator estimate in a real Hilbert space. With $x_{k+1}=(\mathrm{Id}+\beta M)^{-1}(y_k)$ and a coupled recurrence for $y_{k+1}$, the proof defines residuals $r_k=y_{k-1}-x_k$ and $q_k=\beta^{-1}r_k$. The key lemma establishes, for every $N\geq 1$,

Applied on a product Hilbert space, that lemma yields the accelerated proximal point saddle-gap bound

This is the kind of intermediate statement the paper wants the search procedure to expose: a compact lemma that can be reused in a clean proof.

Results and Analysis

The clearest quantitative example in the attached pages is the fast-gradient method sparsity comparison for $N=3$. The raw active interpolation-multiplier pattern contains 16 active entries. Plain $\ell_1$ and log-sum sparsification reduce that to 8. Normalized log-sum and capped $\ell_1$ reduce it to 7. The conjectured active pattern has 6 entries, matching the exhaustive active pattern for that instance. In the paper’s notation, the conjectured pattern has size $N+(N-1)+1=2N$, so the $N=3$ case gives exactly 6 active constraints.

That result supports the paper’s central point better than a generic runtime benchmark would. The payoff is not just that a solver returns fewer nonzero multipliers; it identifies a structured chain of constraints, with blocks corresponding to $x_\star\to y_k$, $y_k\to y_{k+1}$, and the terminal edge $y_{N-1}\to x_N$. This is a proof pattern, not merely a smaller vector.

The evidence is still case-study evidence. The paper demonstrates the approach on gradient descent, proximal methods, and fast-gradient methods, and the appendix supplies formal derivations for recovered structures such as the accelerated proximal point bound. But it does not establish that the same sparse-search procedures will scale smoothly to arbitrary algorithms, nonsmooth composite settings beyond the examples, or large performance-estimation instances where exhaustive sparsification becomes costly. The work is best read as a practical proof-preprocessing method: strong enough to show that certificate simplification can recover meaningful lemmas, but not a general guarantee that simple proofs will always be found.