A Unifying Framework for Global Optimization: From Theory to Formalization

TL;DR

This paper presents a measure-theoretic framework for analyzing stochastic global optimization algorithms, formalized in Lean, enabling rigorous proofs and a unified approach to algorithm analysis.

Contribution

It introduces a formal, implementation-independent measure-theoretic framework for stochastic global optimization, formalized in Lean, unifying analysis and ensuring correctness.

Findings

Framework applies to common algorithms

Provides rigorous proof of a general consistency theorem

Formalization in Lean enhances correctness and future proof automation

Abstract

We introduce an abstract measure___theoretic framework that serves as a tool to rigorously study stochastic iterative global optimization algorithms as a unified class. The framework is formulated in terms of probability kernels, which, via the Ionescu--Tulcea theorem, induce probability measures on the space of sequences of algorithm iterations, endowed with two intuitive properties. This framework answers the need for a general, implementation___independent formalism in the analysis of such algorithms, providing a starting point for formalizing global optimization results in proof-assistants. To illustrate the relevance of our tool, we show that common algorithms fit naturally in the framework, and we also use it to give a rigorous proof of a general consistency theorem for stochastic iterative global optimization algorithms (Proposition 3 of (Malherbe, et al., 2017). This proof and the entire framework are formalized in the Lean proof assistant. This formalization both ensures the correctness of the definitions and proofs, and provides a basis for future machine-assisted formalizations in the field.