NLCertify

NLCertify: A Tool for Formal Nonlinear Optimization. NLCertify is a software package for handling formal certification of nonlinear inequalities involving transcendental multivariate functions. The tool exploits sparse semialgebraic optimization techniques with approximation methods for transcendental functions, as well as formal features. Given a box K and a function f as input, NLCertify provides OCaml libraries that produce nonnegativity certificates for f over K, which can be ultimately proved correct inside the Coq proof assistant. One specific challenge of the field of formal nonlinear reasoning is to develop adaptive techniques to produce certificates with a reduced complexity. The software first builds the abstract syntax tree t of f. The leaves of t are semialgebraic functions obtained by composition of polynomials with some basic operations (including the square root, sup, inf, +, x, -, /, etc). The other nodes can be either univariate transcendental functions (arctan, cos, exp, etc) or basic operations. NLCertify approximates t with means of semialgebraic estimators and provides lower and upper bounds of t over K. When t represents a polynomial, the tool computes lower and upper bounds of t using a hierarchy of semidefinite (SDP) relaxations, via an interface with the external SDPA solver. The extension to the semialgebraic case is straightforward through the implementation of the Lasserre-Putinar lifting-strategy. The user can choose to approximate transcendental functions with best uniform (or minimax) polynomials as well as maxplus estimators. Univariate minimax polynomials are provided using an interface with the Sollya environment, in which an iterative algorithm designed by Remez is implemented. Alternatively, the maxplus approach builds lower (resp. upper) estimators using concave maxima (resp. convex infima) of quadratic forms. In this way, NLCertify computes certified global estimators from approximations of primitive functions by induction over the syntax tree t. These various approximation and optimization algorithms are placed in a unified framework extending to about 15000 lines of OCaml code and 3600 lines of Coq code. The NLCertify package solves successfully non-trivial inequalities from the Flyspeck project (essentially tight inequalities, involving both semialgebraic and transcendental expressions of 6 12 variables) as well as significant global optimization benchmarks.