A Unifying Framework for Global Optimization: From Theory to Formalization

TL;DR

This work introduces a unifying, measure‑theoretic framework based on probability kernels to analyze stochastic iterative global optimization algorithms. By leveraging the Ionescu–Tulcea theorem, it constructs probability measures on both finite and infinite sequences of iterations, yielding an implementation‑independent basis for proof‑assisted verification. It establishes core measure properties—equality on restricted domains and truncation monotonicity—and formalizes a key consistency result from Malherbe et al. in Lean, demonstrating the framework’s correctness and modularity. The approach enables machine‑assisted, reusable formalizations across algorithm families, with future directions including concrete algorithm instantiations within the framework.

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 general 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.

Figures (3)

• Figure 1: Distribution of samples generated by cma-es, when optimizing two different functions $f$ and $g$ that are equal outside the set $E$ (outside the highlighted area). In (a), we force all samples to lie outside $E$, and we observe that the distributions of samples for both functions are identical. In (b), we allow samples to lie anywhere in the search space, and we observe that the distributions of samples for both functions differ. This illustrates \ref{['thm:eq_restrict']}.
• Figure 2: Symbolic illustration of sequences of length $4$, representing algorithmic iterations starting from different initial conditions. For each sequence lying in $B$ connected by a yellow dashed line), its truncated sequence belongs to $E$ (subsequence with blue dots), but the converse does not hold. As a result, there is at least as many sequences of length $3$ in $E$ as there are sequences of length $4$ in $B$. This illustrates \ref{['thm:fin_measure_mono']}.
• Figure 3: Visualization of $\tilde{f}$ applied to the reverse Ackley function with $c \stackrel{\mathsmaller{\mathsf{def}}}{=} (0, 0)^\top$ and $\varepsilon_1 \stackrel{\mathsmaller{\mathsf{def}}}{=} 1$.

Theorems & Definitions (9)

• Proposition 1: Proposition 3 from Malherbe2017
• Definition 1: Stochastic iterative global optimization algorithm
• Theorem 1: Equality of restricted measures
• Theorem 2: Monotonicity by sequence truncation
• Theorem 3: Ionescu-Tulcea theorem Tulcea1949
• Definition 2: Pullback kernels on finite sequences
• proof
• proof
• proof