Certification of Real Inequalities -- Templates and Sums of Squares

TL;DR

This paper introduces a new certified global optimization method for nonlinear multivariate functions involving transcendental and semialgebraic operations, combining approximation techniques with sums of squares relaxations for scalable and precise bounds.

Contribution

It develops a novel template-based framework that integrates maxplus estimators and linear templates to efficiently certify lower bounds for complex transcendental inequalities.

Findings

Effective on problems from global optimization literature

Successfully applied to inequalities from the Flyspeck project

Balances precision and scalability in certification process

Abstract

We consider the problem of certifying lower bounds for real-valued multivariate transcendental functions. The functions we are dealing with are nonlinear and involve semialgebraic operations as well as some transcendental functions like $\cos$, $\arctan$, $\exp$, etc. Our general framework is to use different approximation methods to relax the original problem into polynomial optimization problems, which we solve by sparse sums of squares relaxations. In particular, we combine the ideas of the maxplus estimators (originally introduced in optimal control) and of the linear templates (originally introduced in static analysis by abstract interpretation). The nonlinear templates control the complexity of the semialgebraic relaxations at the price of coarsening the maxplus approximations. In that way, we arrive at a new - template based - certified global optimization method, which exploits both the precision of sums of squares relaxations and the scalability of abstraction methods. We analyze the performance of the method on problems from the global optimization literature, as well as medium-size inequalities issued from the Flyspeck project.