Humboldt-Universität zu Berlin - Mathematisch-Naturwissenschaftliche Fakultät - Institut für Mathematik

In this talk, we provide an overview of Gurobi's algorithmic
components for solving nonlinear optimization problems to global optimality. In essence, we extend our existing mixed-integer programming (MIP) framework to handle such problems. This includes our presolve algorithms, an extension of the branch-and-bound method utilizing spatial relaxations, and an interior point algorithm for nonlinear problems, which serves as a primal heuristic to find high-quality solutions. As a result, we can compute solutions to nonlinear optimization  problems along with certificates for global optimality. Finally, we have extended gurobipy to facilitate the easy formulation of expression-based nonlinear optimization problems in Python.
Gurobi's nonlinear solver applies to explicit expression-based
constraints and does not require the supply of derivative data.

The Abs-Smooth Frank-Wolfe algorithm (ASFW) is a non-smooth variant of the popular Frank-Wolfe algorithms. In this talk we sketch and analyze the "vanilla" and the "heavy-ball" variants of the ASFW algorithm. We provide stronger and more general primal-dual convergence results for ASFW when applied in the convex setting. We derive a convergence rate for our algorithm which is identical to the smooth case. So far, there is limited understanding of accelerated convergence regimes in the context of ASFW. We also provide some answers in this context by looking into some special cases.

The theory of energetic rate-independent systems is an elegant way to describe nonlinear systems in mechanics and other fields. One particular advantage is that it yields a natural time discretization that consists of a sequence of minimization problems. Unfortunately, in many interesting cases the objective functional is only given implicitly as the solution of a second minimization problem for a
curve length in the state space. Therefore, its evaluation and obtaining derivatives can be very costly. Instead, we present a transformation based on the Finsler exponential map that turns the second minimization problem into an initial-value-problem for a second-order ODE. Solutions of this can be found much cheaper numerically, or may even be available in closed form. We show examples of this construction, and how to use it to obtain fast and robust Proximal Newton solvers for finite-strain elastoplasticity. 

tLean is an interactive theorem prover and programming language. It allows its users to write definitions and proofs from mathematics or computer science in a formal language, so that they may be verified. We'll introduce formalization in Lean with a simple study of linked lists. Then, we'll proceed with a discussion of what it means to verify algorithms in Lean, and how it differs from algorithms that produce proofs. Finally, we'll implement a variant of subgradient descent in Lean and prove a convergence theorem for it.