Research map / Optimization / Nonconvex and smooth optimization

Finding Simple Proofs for First-Order Optimization

NeurIPS 2026 · Optimization › Nonconvex and smooth optimization · approach: Coordinate and Adam convergence analysis · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Treats performance-estimation-problem (PEP) dual certificates as objects to simplify, using exhaustive sparsification, weighted/reweighted l1 heuristics, and an SDP for candidate intermediate lemmas, yielding simpler GD, FGM, and proximal proofs.

Problem

Worst-case convergence proofs for first-order optimization obtained from PEP dual certificates are dense and hard to interpret; the task is to find simpler proof structures (fewer active hypotheses, simpler residuals, intermediate lemmas) that still prove the same bound.

Approach

Cast proof simplification as a second-stage optimization over the set of Lagrangian dual certificates that prove a fixed bound, using sparsity surrogates (exhaustive subset search, log-sum/capped-l1 majorization, weighted l1) to minimize active hypotheses, plus a candidate-lemma SDP that derives new valid inequalities (e.g., Lyapunov functions) from existing ones.

Key results

• One-step GD: exhaustive sparsification reduces the certificate to three active interpolation hypotheses and recovers a tight rate rho = max{(1-γμ)^2,(γL-1)^2} for 0<γ<=2/L.
• Proximal point: candidate-lemma SDP recovers a compact Lyapunov proof of the sharp bounds ||g_N|| <= Δ0/A_N and F(x_N)-F* <= Δ0^2/(4A_N).
• FGM at N=3: normalized log-sum heuristic moves the returned active pattern closer to the exhaustive one than plain l1 and log-sum.

Surprising findings

• Adding redundant valid inequalities (e.g., descent lemma) before sparsifying can lead to simpler certificates despite the larger search space.

Limitations

• Exhaustive sparsification cost grows exponentially with number of hypothesis patterns, limiting it to small instances.
• Examples are limited to GD, FGM and proximal methods on small horizons.
• Simplicity is defined operationally via active counts rather than human-judged readability.

Experimental setup

Metrics: active hypothesis count active residual count worst-case rate

Baselines: plain l1 log-sum penalty

Builds on: performance estimation problem interpolation conditions for smooth convex functions reweighted l1 minimization capped-l1 multi-stage convex relaxation

Closest papers by meaning

• Paths, Proofs, and Perfection: Developing a Human-Interpretable Proof System for Constrained Shortest Paths (AAAI 2024 · similarity 0.86)
• ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.86)
• SMILE: Bridging Continuous Optimization and Discrete Symbolic Recovery (NeurIPS 2026 · similarity 0.86)
• On The Complexity of First-Order Methods in Stochastic Bilevel Optimization (ICML 2024 · similarity 0.85)
• 3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes (NeurIPS 2025 · similarity 0.85)
• A Generalization Result for Convergence in Learning-to-Optimize (ICML 2025 · similarity 0.85)