Formal Proofs for Nonlinear Optimization
From MaRDI portal
Abstract: We present a formally verified global optimization framework. Given a semialgebraic or transcendental function and a compact semialgebraic domain , we use the nonlinear maxplus template approximation algorithm to provide a certified lower bound of over . This method allows to bound in a modular way some of the constituents of by suprema of quadratic forms with a well chosen curvature. Thus, we reduce the initial goal to a hierarchy of semialgebraic optimization problems, solved by sums of squares relaxations. Our implementation tool interleaves semialgebraic approximations with sums of squares witnesses to form certificates. It is interfaced with Coq and thus benefits from the trusted arithmetic available inside the proof assistant. This feature is used to produce, from the certificates, both valid underestimators and lower bounds for each approximated constituent. The application range for such a tool is widespread; for instance Hales' proof of Kepler's conjecture yields thousands of multivariate transcendental inequalities. We illustrate the performance of our formal framework on some of these inequalities as well as on examples from the global optimization literature.
Recommendations
- NLCertify: a tool for formal nonlinear optimization
- PROOF-THEORETIC METHODS IN NONLINEAR ANALYSIS
- Formal optimization of some reduced linear programming problems
- scientific article; zbMATH DE number 5773704
- Nonlinear alternative theorems and nondifferentiable programming
- Efficient formal verification of bounds of linear programs
- scientific article; zbMATH DE number 4051368
- Optimization theory and methods. Nonlinear programming
- scientific article; zbMATH DE number 1754535
- scientific article; zbMATH DE number 702646
Cites work
- scientific article; zbMATH DE number 3870568 (Why is no real title available?)
- scientific article; zbMATH DE number 3748393 (Why is no real title available?)
- scientific article; zbMATH DE number 527343 (Why is no real title available?)
- scientific article; zbMATH DE number 2107186 (Why is no real title available?)
- scientific article; zbMATH DE number 6755727 (Why is no real title available?)
- scientific article; zbMATH DE number 2209729 (Why is no real title available?)
- scientific article; zbMATH DE number 2221678 (Why is no real title available?)
- 11th international conference on geometry and applications
- A Max-Plus-Based Algorithm for a Hamilton--Jacobi--Bellman Equation of Nonlinear Filtering
- A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
- A numerical evaluation of several stochastic algorithms on selected continuous global optimization test problems
- A proof of the Kepler conjecture
- A synthesis of the procedural and declarative styles of interactive theorem proving
- A two-level approach towards lean proof-checking
- Algebra and Coalgebra in Computer Science
- Boundary value problems in weighted spaces of polyanalytic functions in half-plane
- Certification of bounds of non-linear functions: the templates method
- Certification of real inequalities: templates and sums of squares
- Computing sum of squares decompositions with rational coefficients
- Discrete and computational geometry
- Experimental mathematics and mathematical physics
- Extending Coq with Imperative Features and Its Application to SAT Verification
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
- Floating-point arithmetic in the Coq system
- Formal Global Optimisation with Taylor Models
- Formalization of Bernstein polynomials and applications to global optimization
- Global optimization with polynomials and the problem of moments
- GloptiPoly 3: moments, optimization and semidefinite programming
- Handbook of continued fractions for special functions. With contributions by Franky Backeljauw and Catherine Bonan-Hamada. Verified numerical output by Stefan Becuwe and Annie Cuyt
- Latest Developments in the SDPA Family for Solving Large-Scale SDPs
- Max-plus methods for nonlinear control and estimation.
- Mechanical geometry theorem proving
- MetiTarski: An automatic theorem prover for real-valued special functions
- On the Generation of Positivstellensatz Witnesses in Degenerate Cases
- Optimization of Polynomials on Compact Semialgebraic Sets
- Positivity and optimization for semi-algebraic functions
- Special cases
- Sums of Squares and Semidefinite Program Relaxations for Polynomial Optimization Problems with Structured Sparsity
- The Max-Plus Finite Element Method for Solving Deterministic Optimal Control Problems: Basic Properties and Convergence Analysis
- Theorem Proving in Higher Order Logics
- Topology
Cited in
(19)- Theorem Proving in Higher Order Logics
- Polynomials with bounds and numerical approximation
- Certification of real inequalities: templates and sums of squares
- Certifying solutions to overdetermined and singular polynomial systems over \(\mathbb{Q}\)
- Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis
- Formal Global Optimisation with Taylor Models
- A heuristic method for certifying isolated zeros of polynomial systems
- Primitive Floats in Coq
- Conic linear optimization for computer-assisted proofs. Abstracts from the workshop held April 10--16, 2022
- Efficient formal verification of bounds of linear programs
- Duality of sum of nonnegative circuit polynomials and optimal SONC bounds
- Pourchet’s theorem in action: decomposing univariate nonnegative polynomials as sums of five squares
- Dynamics of a parametrically excited system with two forcing terms
- Formalization of Bernstein polynomials and applications to global optimization
- Certification of bounds of non-linear functions: the templates method
- Verified reductions for optimization
- Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials
- NLCertify: a tool for formal nonlinear optimization
- Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems
This page was built for publication: Formal Proofs for Nonlinear Optimization
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5195260)
