Summary#

This tutorial demonstrates the complete workflow of PEP to derive convergence proofs of an optimization algorithm.

Provide user input Formulate Primal PEP Numerically verify convergence rate Relax primal PEP via interactive dashboard Find analytical proofs Verify analytical proofs

After the user provides the four ingredients of convergence analysis, PEPFlow automatically formulates both Primal PEP and Dual PEP and solves them solve them numerically using CVXPY.

To obtain an analytical convergence proof, however, several steps still require human interaction. The user is encouraged to use the interactive dashboard to explore and gain intuition about the sparsity pattern of the dual variable \(\lambda\), and to identify its symbolic expression — a step that still relies on human intelligence.

Once \(\lambda\) is determined, the remaining task is to verify that the other dual variable, \(S\), is positive semidefinite. This verification is largely mechanical: it involves decomposing the inner product \(\langle G, S \rangle\) into a sum of squares, which corresponds to performing the Cholesky factorization of \(S\).

Moreover, PEPFlow offers a user-friendly interface for symbolic verification of convergence proofs. Two key features in PEPFlow make this workflow intuitive and efficient:

  • an interactive dashboard for visualizing and exploring sparsity patterns of \(\lambda\);

  • In PEPFlow, all function values and inner products are represented in terms of coordinates of basis variables. PEPFlow enables users to access these quantities simply by their name tags, while all computations are handled automatically in coordinates—eliminating the need to manually construct or verify coefficients in the Primal PEP.