NLCertify: A Tool for Formal Nonlinear Optimization

TL;DR

NLCertify is a software tool that certifies nonlinear inequalities involving transcendental functions using semialgebraic optimization and formal proof techniques, integrating with Coq for correctness.

Contribution

It introduces a novel software package that combines sparse semialgebraic optimization with formal verification for nonlinear inequalities involving transcendental functions.

Findings

Successfully certifies nonlinear inequalities over specified domains.

Integrates with Coq for formal correctness proofs.

Handles transcendental multivariate functions efficiently.

Abstract

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 and a transcendental multivariate function as input, NLCertify provides OCaml libraries that produce nonnegativity certificates for the function over the box, which can be ultimately proved correct inside the Coq proof assistant.