Pith. sign in

REVIEW 2 major objections 9 minor 49 references

Sparse optimization turns dense proof certificates into simple proofs

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · glm-5.2

2026-07-10 01:46 UTC pith:SSQES7V3

load-bearing objection Solid methodology paper on simplifying PEP certificates into human-readable proofs; main limitation is that the candidate-lemma search needs hand-specified structure. the 2 major comments →

arxiv 2607.08753 v1 pith:SSQES7V3 submitted 2026-07-09 math.OC

Finding Simple Proofs for First-Order Optimization

Daniel Berg Thomsen , Manu Upadhyaya , Baptiste Goujaud , Aymeric Dieuleveut , Adrien Taylor This is my paper
classification math.OC MSC 90C2549M3768Q25
keywords performance estimation problemsproof simplificationsparse optimizationLagrangian dual certificatesfirst-order methodsLyapunov functionssemidefinite programming
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper addresses a gap in computer-aided mathematics: automated solvers can certify that an optimization algorithm achieves a certain worst-case performance bound, but the certificates they produce are dense, non-unique, and hard for humans to read or reuse. The authors treat proof simplification as a second-stage optimization problem. Starting from a Lagrangian dual certificate—a set of nonnegative multipliers on interpolation inequalities that together certify a convergence rate—they apply sparse optimization techniques to prune away redundant inequalities, leaving only the essential ones. They introduce three families of procedures: exhaustive sparsification (checking all subsets of hypotheses to find the minimum-cardinality proof, feasible for small instances), weighted l1-type heuristics (iterative reweighting schemes that scale to larger problems), and an SDP-based candidate-lemma search that derives new valid inequalities from existing ones, potentially surfacing intermediate lemmas such as Lyapunov functions. On gradient descent, the methods recover a clean three-inequality proof with fitted curvature parameters that weaken the function-class assumptions just enough to make the proof work. On fast-gradient methods, normalized sparsity heuristics reduce the number of active multipliers toward a conjectured minimal pattern. On proximal point methods, the candidate-lemma SDP recovers Lyapunov potential functions and their one-step decrements, yielding streamlined proofs of sharp residual and saddle-gap bounds.

Core claim

The central mechanism is a two-stage pipeline. In the first stage, a performance estimation problem (PEP) is solved numerically, yielding a Lagrangian dual certificate: a set of nonnegative multipliers on valid interpolation inequalities that sum to a proof of the target convergence rate. In the second stage, the certificate is re-optimized for sparsity rather than for the rate itself. The key technical objects are (i) the active hypothesis set—the subset of inequalities with positive multipliers, whose size measures proof complexity—and (ii) the candidate-lemma SDP, which searches for new valid inequalities expressible as nonnegative combinations of existing hypotheses plus residual terms.当

What carries the argument

The machinery operates on the proof identity ρI_f − P_f = Σ λ_h H_h + Σ c_i R_i, where H_h are valid interpolation inequalities, R_i are nonnegative residual terms, and all multipliers are nonnegative. Sparsification minimizes the count of active H_h (and optionally active R_i) subject to the certificate still proving a relaxed target rate ρ̄. The candidate-lemma SDP introduces auxiliary inequalities Ψ_κ, each certifiable from existing hypotheses, and searches for multipliers η_κ that make them useful in the main proof—effectively discovering intermediate lemmas by optimization.

Load-bearing premise

The candidate-lemma search requires the user to pre-specify the family of allowable intermediate inequalities (for example, restricting to interpolation inequalities with weaker curvature parameters, or specific potential-function forms). The method optimizes within this hand-constrained space; it does not discover lemma structure from scratch.

What would settle it

A concrete test: apply the candidate-lemma SDP to a problem where the natural Lyapunov function or intermediate lemma lies outside the pre-specified family (e.g., a non-polynomial potential, or a lemma involving cross-terms not representable as interpolation inequalities). If the SDP returns no useful lemma, the method's scope is confirmed to be limited by the user's structural ansatz.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • If the pipeline generalizes, it could become a standard post-processing step after any PEP-based analysis: solve the SDP, then automatically distill the resulting certificate into a human-readable proof structure before attempting hand derivation or formalization.
  • The candidate-lemma SDP's recovery of Lyapunov functions suggests that automated proof simplification can serve as a discovery tool for potential-based analyses of algorithms where no human has yet identified the right Lyapunov function.
  • The fitted-curvature technique for gradient descent—relaxing strong-convexity and smoothness parameters just enough to admit a simpler proof—could extend to other algorithm classes where proofs are known to be tight but structurally opaque.
  • Sparse certificates that expose multiplier patterns (as in the FGM conjectured 2N-active pattern) could guide the design of new algorithms by revealing which inequalities are load-bearing.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The method's success depends on the pre-specified structure of candidate lemmas; if the right intermediate inequality does not lie in the constrained search space, the SDP cannot find it. A fully automated lemma-discovery procedure would need a richer or adaptive hypothesis space.
  • The approach could in principle extend beyond first-order optimization to any domain where proofs reduce to sums of nonnegligible terms certified by convex programs—e.g., stability proofs in control theory or sum-of-squares certificates in polynomial optimization.
  • The distinction between 'the certificate proves the bound' and 'the simplified certificate reveals the proof structure' suggests a formal hierarchy of certificate readability that could be made precise, connecting sparsity of the dual solution to proof-theoretic notions of proof complexity.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 9 minor

Summary. This paper addresses the problem of simplifying machine-generated certificates from performance estimation problems (PEPs) for first-order optimization methods. The authors treat proof simplification as a second-stage optimization problem over Lagrangian dual certificates. They introduce two complexity measures (hypothesis complexity and residual complexity), and develop three classes of procedures: exhaustive sparsification, weighted $l_1$-type heuristics for larger instances, and an SDP-based candidate-lemma search that can discover intermediate lemmas (including Lyapunov functions). The methods are demonstrated on gradient descent (recovering a three-hypothesis proof with fitted curvature parameters), fast-gradient methods (sparsifying multiplier patterns), and proximal point methods (recovering Lyapunov functions for residual/value bounds and a saddle-gap estimate). The SDP formulations are derived in Appendices A-B, and closed-form proofs for all three theorems are provided in Appendix E. Code is publicly available.

Significance. The paper makes a methodological contribution at the interface of optimization theory and computer-assisted proof. The key insight—that PEP dual certificates can be post-processed via sparse optimization to yield interpretable proof structures—is well-motivated and timely. Specific strengths include: (i) the sparsification procedures (exhaustive and weighted-$l_1$) are genuinely autonomous and require no pre-specification of proof structure; (ii) the candidate-lemma SDP (CL-SDP) provides a principled mechanism for deriving valid inequalities from existing hypotheses; (iii) all recovered results are verified by complete closed-form proofs (Appendix E); (iv) the code is public, supporting reproducibility. The recovery of Lyapunov functions for proximal methods (Theorems 2-3) is a particularly compelling demonstration. The paper is honest about limitations: the FGM heuristics approach but do not always reach the conjectured 2N pattern (Figure 3), and the candidate-lemma search requires the user to constrain the lemma search space.

major comments (2)
  1. [Section 3.3 and Appendix B] The candidate-lemma SDP (CL-SDP) requires the user to pre-specify the structure of allowable lemmas: the index set L_cand, the hypothesis subsets I_kappa, and the form of Psi_kappa. In the GD example (Section 4.1.2, Appendix C.2), the search is restricted to interpolation inequalities with weaker curvature parameters (a,b). In the proximal examples (Section 5), specific potential function forms are imposed. The paper acknowledges this ('Rather than prescribing a single proof template, the workflow exposes proof patterns and candidate lemmas by searching over certificate representations'), but the degree of hand-specification is not fully transparent from the main text alone. A reader must consult Appendix C.2 to understand how constrained the GD lemma search actually is. The paper would benefit from a brief discussion in Section 3.3 of how sensitive the results are to the choice of lemma
  2. [Section 3.3 and Appendix B] The candidate-lemma SDP (CL-SDP) requires the user to pre-specify the structure of allowable lemmas: the index set L_cand, the hypothesis subsets I_kappa, and the form of Psi_kappa. In the GD example (Section 4.1.2, Appendix C.2), the search is restricted to interpolation inequalities with weaker curvature parameters (a,b). In the proximal examples (Section 5), specific potential function forms are imposed. The paper acknowledges this ('Rather than prescribing a single proof template, the workflow exposes proof patterns and candidate lemmas by searching over certificate representations'), but the degree of hand-specification is not fully transparent from the main text alone. A reader must consult Appendix C.2 to understand how constrained the GD lemma search actually is. The paper would benefit from a brief discussion in Section 3.3 of how sensitive the results are to the choice of lemma
minor comments (9)
  1. Abstract: The phrase 'autonomously prune redundant inequalities' slightly overstates the autonomy of the candidate-lemma search, which requires pre-specified lemma structure. Consider softening to 'systematically prune' or clarifying that autonomy applies to the sparsification procedures.
  2. Section 2.1, equation (Proof): The notation uses both $K_{i,j}$ as a set indexing hypotheses and $l$ as an element of that set, but the superscript $(l)$ on $H$ and $lambda$ is sometimes written as a parenthesized superscript and sometimes not. Consistency would aid readability.
  3. Section 4.1.2, equation (5): The fitted curvature parameters $(mu_gamma, L_gamma)$ are defined piecewise, but the threshold $2/(L+mu)$ is only implicitly motivated. A brief sentence explaining why this threshold arises would help the reader.
  4. Figure 3 (left panel): The y-axis label 'Active multipliers' could be confused with the 'active hypotheses' terminology of Section 2.2. Consider using 'Active hypothesis multipliers' or adding a clarifying caption note.
  5. Remark 1: The reference to Taylor et al. [37, Theorem 3.3] is used to connect the fitted-curvature proof to prior work, but the connection is stated in passing. A sentence or two explaining the relationship between the fitted curvature trick and the composite optimization setting of [37] would strengthen the remark.
  6. Notation: The bracket notation $J_{n,m}K$ for integer intervals is introduced in the Notation section but used inconsistently; sometimes $J0,NK$ appears without the subscript, and the closing bracket is sometimes omitted in inline math.
  7. Appendix C.2, equation (GD-CL-SDP): The constraint $Qhat_{i,j}(c) - Q^{mu,L}_{i,j} succeq 0$ certifies validity by enforcing $H_{a,b}(x_i, x_j) geq H_{mu,L}(x_i, x_j) geq 0$. This is correct, but the direction of the inequality (that the fitted inequality is weaker) should be stated more explicitly in the main text, as it is central to why the fitted curvatures yield valid proofs.
  8. Section 5.2: The APPM recurrence (APPM) uses the same momentum coefficient $k/(k+2)$ as FGM but the connection to the FGM parameterization is not discussed. A brief note on why this specific parameterization is used would contextualize the result for readers familiar with FGM but not with APPM.
  9. Table 1 (Appendix F): The bullet-style spy plot is clear, but the row/column ordering differs between panels (e.g., 'Raw' includes $x_3$ as both source and target, while 'Conjecture' does not). Using a consistent ordering across all panels, or noting the difference, would help readers verify the counts.

Circularity Check

0 steps flagged

No significant circularity: the paper's simplification procedures search within a well-defined feasible set of dual certificates, and all recovered proofs are independently verifiable.

full rationale

The paper treats PEP dual certificates as inputs and applies sparsification heuristics or candidate-lemma SDP searches to find structurally simpler certificates within the same feasible set. The key derivation chain is: (1) solve the PEP SDP to get a dense dual certificate certifying a worst-case rate; (2) post-process via exhaustive sparsification, weighted l1 heuristics, or candidate-lemma SDP to find a sparser or more structured certificate proving the same (or relaxed) bound. None of these steps reduce to their inputs by construction. The sparsification procedures genuinely search over subsets of active hypotheses and check feasibility—a combinatorial search, not a tautology. The candidate-lemma SDP (CL-SDP, Appendix B) derives valid inequalities from existing interpolation hypotheses, which is a legitimate logical derivation (if H_h >= 0 and the lemma is a nonnegative combination of H_h terms plus PSD residual, then the lemma >= 0). The fitted-curvature GD proof (Theorem 1) uses the inclusion F_{mu,L} subset F_{mu_gamma, L_gamma}, which is a genuine relaxation, not a renaming. The proximal proofs (Theorems 2-3, Appendix E) are complete, self-contained Lyapunov arguments verified independently of the SDP search that motivated them. Self-citations to prior PEP work (Taylor et al., Goujaud et al.) provide the framework and software but are not load-bearing for the mathematical validity of the recovered proofs, which stand on their own. The paper honestly reports that heuristics do not always reach the conjectured optimum (Figure 3, FGM). No step in the derivation chain is equivalent to its inputs by definition.

Axiom & Free-Parameter Ledger

5 free parameters · 4 axioms · 0 invented entities

The paper introduces no new mathematical entities or physical objects. The free parameters are all numerical tolerances and penalty hyperparameters for the sparsification heuristics, not fitted physical constants. The axioms are standard PEP framework assumptions plus the ad-hoc choice of lemma search space.

free parameters (5)
  • epsilon_act = 10^{-7} (in FGM table)
    Threshold for determining active multipliers in numerical experiments; affects which hypotheses are counted as active.
  • epsilon_rel = set to recover rho_rel = 2L/(N^2+5N+2)
    Relative suboptimality tolerance for the relaxed target rate; controls the trade-off between certificate sparsity and bound tightness.
  • delta = not specified numerically
    Stabilization constant in the log-sum penalty (Section 3.2); affects sparsification behavior.
  • M_h = estimated from feasible range, clipped
    Reference scale for normalizing multipliers in the normalized log-sum and capped l1 penalties (Section 3.2).
  • theta = not specified numerically
    Normalized activation threshold for the capped l1 penalty (Section 3.2).
axioms (4)
  • standard math Interpolation inequalities for F_{mu,L} are valid and complete for representing the function class in PEP formulations.
    Used throughout as the hypothesis set H_{mu,L}(u,v) >= 0; established by Taylor et al. [36].
  • domain assumption Assumption 1 (Finite hypothesis form): admissibility requirements can be represented by finitely many scalar hypotheses at sampled points.
    Stated in Appendix A.1; foundational for reducing the infinite-dimensional PEP to a finite SDP.
  • domain assumption Assumption 2 (Gram representability): sampled quantities can be encoded by scalar coordinates and a PSD Gram matrix.
    Stated in Appendix A.2; enables the SDP lift of the finite PEP.
  • ad hoc to paper The candidate-lemma search space (I_kappa subsets, Psi_kappa structure) is pre-specified by the user.
    Section 3.3 and Appendix C.2: the user must constrain the lemma structure (e.g., to weaker interpolation classes) before solving the SDP.

pith-pipeline@v1.1.0-glm · 27078 in / 2689 out tokens · 229998 ms · 2026-07-10T01:46:07.365081+00:00 · methodology

0 comments
read the original abstract

Progress in mathematics often requires more than a certificate of truth: it requires proof structures that are transparent, checkable, and reusable. Automated systems can increasingly certify that a result is true; what they typically return, however, is a dense certificate rather than an interpretable, reusable proof structure. Recent work on performance estimation problems has shown that performance bounds and complexity analyses of first-order optimization methods can be discovered by searching over a structured space of Lagrangian dual certificates. We cast the search for simpler proof structures as a second-stage optimization problem over these certificates. Starting from dual certificates, we develop post-processing procedures using tools from sparse optimization and statistical learning. We measure complexity through features such as active hypotheses and residual structure, and introduce methods based on exhaustive sparsification, weighted $\ell_1$-type heuristics, and semidefinite programming (SDP) formulations for discovering simple proofs and intermediate lemmas. Examples on gradient descent, proximal methods, and fast-gradient methods show that these procedures can autonomously prune redundant inequalities, reveal structured proof patterns, and, in the proximal setting, recover Lyapunov functions as intermediate lemmas that lead to simple, streamlined proofs. By distilling dense machine-generated certificates into compact proof structures, this workflow acts as a pre-processing step for the final proof, reducing the complexity that must be managed during human interpretation, reuse, and formalization.

Figures

Figures reproduced from arXiv: 2607.08753 by Adrien Taylor, Aymeric Dieuleveut, Baptiste Goujaud, Daniel Berg Thomsen, Manu Upadhyaya.

Figure 1
Figure 1. Figure 1: One-step gradient descent with functional-residual normalization. Left: raw certificate [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Fitted interpolation curvatures identified from singleton candidate lemmas for the one-step [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: FGM hypothesis complexity across horizon lengths: all methods on the left, and the [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

49 extracted references · 49 canonical work pages · 5 internal anchors

  1. [1]

    Abbaszadehpeivasti, E

    H. Abbaszadehpeivasti, E. de Klerk, and M. Zamani. On the rate of convergence of the difference-of-convex algorithm (DCA).Journal of Optimization Theory and Applications, 202 (1):475–496, 2024. doi: 10.1007/s10957-023-02199-z

    work page doi:10.1007/s10957-023-02199-z 2024

  2. [2]

    J. M. Altschuler and P. A. Parrilo. Acceleration by stepsize hedging: Multi-step descent and the silver stepsize schedule.Journal of the ACM, 72(2):1–38, 2025. doi: 10.1145/3708502

    work page doi:10.1145/3708502 2025

  3. [3]

    Amaldi and V

    E. Amaldi and V . Kann. On the approximability of minimizing nonzero variables or unsatisfied relations in linear systems.Theoretical Computer Science, 209(1–2):237–260, 1998. doi: 10.1016/S0304-3975(97)00115-1

    work page doi:10.1016/s0304-3975(97)00115-1 1998

  4. [4]

    Principled Analyses and Design of First-Order Methods with Inexact Proximal Operators

    M. Barré, A. Taylor, and F. Bach. Principled analyses and design of first-order methods with inexact proximal operators, 2020. arXiv:2006.06041 [math.OC]

    work page internal anchor Pith review Pith/arXiv arXiv 2020

  5. [5]

    Berg Thomsen, A

    D. Berg Thomsen, A. Taylor, and A. Dieuleveut. Tight analyses of first-order methods with error feedback.Advances in Neural Information Processing Systems (NeurIPS), 2025. URL https://papers.neurips.cc/paper_files/paper/2025/hash/ea9f05e43ff75fc8 d70ba9ff1d18cfa5-Abstract-Conference.html

    work page 2025

  6. [6]

    Bertsimas, A

    D. Bertsimas, A. King, and R. Mazumder. Best subset selection via a modern optimization lens. The Annals of Statistics, 44(2):813–852, 2016. doi: 10.1214/15-AOS1388

    work page doi:10.1214/15-aos1388 2016

  7. [7]

    E. J. Candès, M. B. Wakin, and S. P. Boyd. Enhancing sparsity by reweighted ℓ1 minimization. Journal of Fourier Analysis and Applications, 14(5):877–905, 2008. doi: 10.1007/s00041-008- 9045-x

    work page doi:10.1007/s00041-008- 2008

  8. [8]

    de Klerk, F

    E. de Klerk, F. Glineur, and A. B. Taylor. On the worst-case complexity of the gradient method with exact line search for smooth strongly convex functions.Optimization Letters, 11(7): 1185–1199, 2017. doi: 10.1007/s11590-016-1087-4

    work page doi:10.1007/s11590-016-1087-4 2017

  9. [9]

    Dragomir, A

    R.-A. Dragomir, A. B. Taylor, A. d’Aspremont, and J. Bolte. Optimal complexity and certifica- tion of Bregman first-order methods.Mathematical Programming, 194(1):41–83, 2022. doi: 10.1007/s10107-021-01618-1

    work page doi:10.1007/s10107-021-01618-1 2022

  10. [11]

    Drori and M

    Y . Drori and M. Teboulle. Performance of first-order methods for smooth convex minimization: A novel approach.Mathematical Programming, 145(1):451–482, 2014. doi: 10.1007/s10107- 013-0653-0

    work page doi:10.1007/s10107- 2014

  11. [12]

    Fredholm theory of families of discrete dynamical systems and its applications to bifurcation theory

    M. Fazel, H. Hindi, and S. P. Boyd. Log-det heuristic for matrix rank minimization with applications to Hankel and Euclidean distance matrices. InProceedings of the 2003 Amer- ican Control Conference (ACC), 2003, volume 3, pages 2156–2162. IEEE, 2003. doi: 10.1109/ACC.2003.1243393

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.1109/acc.2003.1243393 2003

  12. [13]

    Gorbunov, A

    E. Gorbunov, A. Taylor, and G. Gidel. Last-iterate convergence of optimistic gradient method for monotone variational inequalities.Advances in Neural Information Processing Systems, 35: 21858–21870, 2022. doi: 10.52202/068431-1589

    work page doi:10.52202/068431-1589 2022

  13. [14]

    Optimal first-order methods for convex functions with a quadratic upper bound

    B. Goujaud, A. Taylor, and A. Dieuleveut. Optimal first-order methods for convex functions with a quadratic upper bound, 2022. arXiv:2205.15033 [math.OC]

    work page internal anchor Pith review Pith/arXiv arXiv 2022

  14. [15]

    Goujaud, A

    B. Goujaud, A. Dieuleveut, and A. Taylor. On fundamental proof structures in first-order optimization. In2023 62nd IEEE Conference on Decision and Control (CDC), pages 3023–

    work page

  15. [16]

    doi: 10.1109/CDC49753.2023.10383282

    IEEE, 2023. doi: 10.1109/CDC49753.2023.10383282

    work page doi:10.1109/cdc49753.2023.10383282 2023

  16. [17]

    Goujaud, C

    B. Goujaud, C. Moucer, F. Glineur, J. M. Hendrickx, A. B. Taylor, and A. Dieuleveut. PEPit: Computer-assisted worst-case analyses of first-order optimization methods in Python.Mathe- matical Programming Computation, 16(3):337–367, 2024. doi: 10.1007/s12532-024-00259-7. 11

    work page doi:10.1007/s12532-024-00259-7 2024

  17. [18]

    Gu and J

    G. Gu and J. Yang. Tight convergence rate in subgradient norm of the proximal point algorithm. Optimization, 2025. doi: 10.1080/02331934.2025.2602877

    work page doi:10.1080/02331934.2025.2602877 2025

  18. [19]

    U. Jang, S. Das Gupta, and E. K. Ryu. Computer-assisted design of accelerated composite optimization methods: OptISTA.Mathematical Programming, pages 1–109, 2025. doi: 10.1007/s10107-025-02258-5

    work page doi:10.1007/s10107-025-02258-5 2025

  19. [20]

    D. Kim. Accelerated proximal point method for maximally monotone operators.Mathematical Programming, 190:57–87, 2021. doi: 10.1007/s10107-021-01643-0

    work page doi:10.1007/s10107-021-01643-0 2021

  20. [21]

    Kim and J

    D. Kim and J. A. Fessler. Optimized first-order methods for smooth convex minimization. Mathematical Programming, 159(1):81–107, 2016. doi: 10.1007/s10107-015-0949-3

    work page doi:10.1007/s10107-015-0949-3 2016

  21. [22]

    Kim and J

    D. Kim and J. A. Fessler. Another look at the fast iterative shrinkage/thresholding algorithm (FISTA).SIAM Journal on Optimization, 28(1):223–250, 2018. doi: 10.1137/16M108940X

    work page doi:10.1137/16m108940x 2018

  22. [23]

    Kim and J

    D. Kim and J. A. Fessler. Generalizing the optimized gradient method for smooth convex mini- mization.SIAM Journal on Optimization, 28(2):1920–1950, 2018. doi: 10.1137/17M112124X

    work page doi:10.1137/17m112124x 1920

  23. [24]

    F. Lieder. On the convergence rate of the Halpern-iteration.Optimization Letters, 15(2): 405–418, 2021. doi: 10.1007/s11590-020-01617-9

    work page doi:10.1007/s11590-020-01617-9 2021

  24. [25]

    Naldi, M

    S. Naldi, M. Safey El Din, A. Taylor, and W. Wang. Solving generic parametric linear matrix inequalities. InProceedings of the 2025 International Symposium on Symbolic and Algebraic Computation, pages 267–276, 2025. doi: 10.1145/3747199.3747570

    work page doi:10.1145/3747199.3747570 2025

  25. [26]

    B. K. Natarajan. Sparse approximate solutions to linear systems.SIAM Journal on Computing, 24(2):227–234, 1995. doi: 10.1137/S0097539792240406

    work page doi:10.1137/s0097539792240406 1995

  26. [27]

    Park and E

    J. Park and E. K. Ryu. Exact optimal accelerated complexity for fixed-point iterations. InProceedings of the 39th International Conference on Machine Learning, volume 162 ofProceedings of Machine Learning Research, pages 17420–17457. PMLR, 2022. URL https://proceedings.mlr.press/v162/park22c.html

    work page 2022

  27. [28]

    Rotaru.Exact Performance Analysis of Fundamental First-Order Optimization Methods

    T. Rotaru.Exact Performance Analysis of Fundamental First-Order Optimization Methods. PhD thesis, KU Leuven, 2026. URL https://lirias.kuleuven.be/handle/20.500.1 2942/781389

    work page 2026

  28. [29]

    Rotaru, F

    T. Rotaru, F. Glineur, and P. Patrinos. Exact worst-case convergence rates of gradient descent: A complete analysis for all constant stepsizes over nonconvex and convex functions, 2024. arXiv:2406.17506 [math.OC]

    work page arXiv 2024

  29. [30]

    E. K. Ryu, A. B. Taylor, C. Bergeling, and P. Giselsson. Operator splitting performance estimation: Tight contraction factors and optimal parameter selection.SIAM Journal on Optimization, 30(3):2251–2271, 2020. doi: 10.1137/19M1304854

    work page doi:10.1137/19m1304854 2020

  30. [31]

    Shugart and J

    H. Shugart and J. M. Altschuler. Negative stepsizes make gradient-descent-ascent converge,

    work page

  31. [32]

    arXiv:2505.01423 [math.OC]

    work page internal anchor Pith review Pith/arXiv arXiv

  32. [33]

    Taylor.Convex interpolation and performance estimation of first-order methods for convex optimization

    A. Taylor.Convex interpolation and performance estimation of first-order methods for convex optimization. PhD thesis, Université Catholique de Louvain, 2017. URL https://hdl.hand le.net/2078.5/67094

    work page 2017

  33. [34]

    Taylor and F

    A. Taylor and F. Bach. Stochastic first-order methods: Non-asymptotic and computer-aided analyses via potential functions. InConference on Learning Theory, pages 2934–2992. PMLR,

    work page

  34. [35]

    URLhttps://proceedings.mlr.press/v99/taylor19a.html

    work page

  35. [36]

    Taylor and Y

    A. Taylor and Y . Drori. An optimal gradient method for smooth strongly convex minimization. Mathematical Programming, 199(1):557–594, 2023. doi: 10.1007/s10107-022-01839-y

    work page doi:10.1007/s10107-022-01839-y 2023

  36. [37]

    A. B. Taylor, J. M. Hendrickx, and F. Glineur. Exact worst-case performance of first-order methods for composite convex optimization.SIAM Journal on Optimization, 27(3):1283–1313,

    work page

  37. [38]

    doi: 10.1137/16M108104X. 12

    work page doi:10.1137/16m108104x

  38. [39]

    A. B. Taylor, J. M. Hendrickx, and F. Glineur. Performance estimation toolbox (PESTO): Automated worst-case analysis of first-order optimization methods. In2017 IEEE 56th Annual Conference on Decision and Control (CDC), pages 1278–1283. IEEE, 2017. doi: 10.1109/CDC.2017.8263832

    work page doi:10.1109/cdc.2017.8263832 2017

  39. [40]

    A. B. Taylor, J. M. Hendrickx, and F. Glineur. Smooth strongly convex interpolation and exact worst-case performance of first-order methods.Mathematical Programming, 161(1-2):307–345,

    work page

  40. [41]

    doi: 10.1007/s10107-016-1009-3

    work page doi:10.1007/s10107-016-1009-3

  41. [42]

    A. B. Taylor, J. M. Hendrickx, and F. Glineur. Exact worst-case convergence rates of the proximal gradient method for composite convex minimization.Journal of Optimization Theory and Applications, 178(2):455–476, 2018. doi: 10.1007/s10957-018-1298-1

    work page doi:10.1007/s10957-018-1298-1 2018

  42. [43]

    Tibshirani

    R. Tibshirani. Regression shrinkage and selection via the lasso.Journal of the Royal Statistical Society: Series B (Methodological), 58(1):267–288, 1996. doi: 10.1111/j.2517- 6161.1996.tb02080.x

    work page doi:10.1111/j.2517- 1996

  43. [44]

    Upadhyaya, S

    M. Upadhyaya, S. Banert, A. B. Taylor, and P. Giselsson. Automated tight Lyapunov anal- ysis for first-order methods.Mathematical Programming, 209(1–2):133–170, 2024. doi: 10.1007/s10107-024-02061-8

    work page doi:10.1007/s10107-024-02061-8 2024

  44. [45]

    Upadhyaya, S

    M. Upadhyaya, S. Das Gupta, A. B. Taylor, S. Banert, and P. Giselsson. The AutoLyap software suite for computer-assisted Lyapunov analyses of first-order methods, 2025. arXiv:2506.24076 [math.OC]

    work page arXiv 2025

  45. [46]

    An optimal first-order method for smooth and strongly convex composite optimization and its stationary limit

    M. Upadhyaya, D. Berg Thomsen, A. Dieuleveut, and A. B. Taylor. An optimal first-order method for smooth and strongly convex composite optimization and its stationary limit, 2026. arXiv:2605.22929 [math.OC]

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  46. [47]

    Uschmajew and B

    A. Uschmajew and B. Vandereycken. A note on the optimal convergence rate of descent methods with fixed step sizes for smooth strongly convex functions.Journal of Optimization Theory and Applications, 194(1):364–373, 2022. doi: 10.1007/s10957-022-02032-z

    work page doi:10.1007/s10957-022-02032-z 2022

  47. [48]

    T. Yoon, J. Kim, J. J. Suh, and E. K. Ryu. Optimal acceleration for minimax and fixed-point problems is not unique. InProceedings of the 41st International Conference on Machine Learning, volume 235 ofProceedings of Machine Learning Research, pages 57244–57314. PMLR, 2024. URLhttps://proceedings.mlr.press/v235/yoon24b.html

    work page 2024

  48. [49]

    1 0 0 # ,bx 1 =

    T. Zhang. Analysis of multi-stage convex relaxation for sparse regularization.Journal of Machine Learning Research, 11(35):1081–1107, 2010. URL https://jmlr.csail.mit.e du/papers/v11/zhang10a.html. 13 Appendices Table of Contents A General PEP framework 15 A.1 Sampled-data PEP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 A.2 Lift...

    work page 2010

  49. [50]

    Finally, convexity gives F(x N)−F ⋆ ⩽⟨g N , xN −x ⋆⟩, and Young’s inequality in theB/B−1 pair yields 2AN(F(x N)−F ⋆)⩽∥x N −x ⋆∥2 B +A 2 N ∥gN ∥2 B−1

    SinceF(x N)−F ⋆ ⩾0, this implies A2 N ∥gN ∥2 B−1 ⩽V N ⩽∆ 2 0, and hence ∥gN ∥B−1 ⩽∆ 0/AN . Finally, convexity gives F(x N)−F ⋆ ⩽⟨g N , xN −x ⋆⟩, and Young’s inequality in theB/B−1 pair yields 2AN(F(x N)−F ⋆)⩽∥x N −x ⋆∥2 B +A 2 N ∥gN ∥2 B−1 . Adding another copy of 2AN(F(x N)−F ⋆) to both sides gives 4AN(F(x N)−F ⋆)⩽V N ⩽∆ 2 0, proving the value bound. 24 ...

    work page