Verification¶
These notebooks verify the worst-case performance of first-order methods on five
example problems. Each one sets up a Verifier, declares
the problem data and the initial condition, writes the algorithm out of
step operators, and solves the resulting verification problem
exactly as a mixed-integer linear program (method='mip').
The notebooks solve the MIPs with Gurobi (solver='gurobi'), which needs a
license. Without one, change solver='gurobi' to
solver='highs' in the verification cells; the bounds are the same, but the
longer horizons take considerably more time with HiGHS.
Examples¶
- Lasso: ISTA on the \(\ell_1\)-regularized least-squares problem, verified with a soft-threshold step.
- Optimal control: a linear-quadratic control problem with input bounds, verified with a saturated linear step.
- Network flow: a capacitated min-cost network-flow linear program, solved by an operator-splitting method.
- Nonnegative least squares: projected gradient descent, whose projection onto the nonnegative orthant is a ReLU step.
- Portfolio: a mean–variance portfolio problem with box bounds and a budget constraint, solved by ADMM.
Once a method is verified, the code generation tutorial shows how
to turn the same Verifier object into an embedded C solver, and the
code generation guide documents that pipeline in full.