Verified Optimization

TL;DR

This paper presents a framework using the Lean proof assistant to reliably design and apply problem reductions in optimization, enhancing the trustworthiness and flexibility of optimization solutions.

Contribution

It introduces a novel framework leveraging Lean for formal verification of optimization problem reductions, improving reliability and adaptability.

Findings

Framework enables formal verification of optimization reductions

Enhances reliability of optimization problem transformations

Provides flexible, trustworthy reduction methods

Abstract

Optimization is used extensively in engineering, industry, and finance, and various methods are used to transform problems to the point where they are amenable to solution by numerical methods. We describe progress towards developing a framework, based on the Lean interactive proof assistant, for designing and applying such reductions in reliable and flexible ways.