Verified reductions for optimization
Preprint
Abstract
Numerical and symbolic methods for optimization are used extensively in engineering, industry, and finance. Various methods are used to reduce problems of interest to ones that are amenable to solution by such software. We develop a framework for designing and applying such reductions, using the Lean programming language and interactive proof assistant. Formal verification makes the process more reliable, and the availability of an interactive framework and ambient mathematical library provides a robust environment for constructing the reductions and reasoning about them.Keywords
All Related Versions
This publication has 19 references indexed in Scilit:
- The Lean 4 Theorem Prover and Programming Language2021
- Formal Techniques for Verification and Testing of Cyber-Physical Systems2019
- A Formalization of Convex Polyhedra Based on the Simplex MethodJournal of Automated Reasoning, 2018
- Lectures on Convex Optimization2018
- A rewriting system for convex optimization problemsJournal of Control and Decision, 2017
- Verification of Numerical Programs: From Real Numbers to Floating Point Numbers2013
- Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOLThe Computer Journal, 2009
- New upper bounds for kissing numbers from semidefinite programmingJournal of the American Mathematical Society, 2007
- Verifying Nonlinear Real Formulas Via Sums of Squares2007
- Using SeDuMi 1.02, A Matlab toolbox for optimization over symmetric conesOptimization Methods and Software, 1999