2025/08/28 by Gaëtan Serré, Kalogeratos, Argyris, Serré, Gaëtan +1
Computer Science · #Computability, Logic, AI Algorithms #Constraint Satisfaction and Optimization #FOS: Computer and information sciences #FOS: Mathematics #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Optimization and Control (math.OC) #Probability (math.PR)
paper · pdf · doi:10.48550/arxiv.2508.20671
openalex publication_date 2025/08/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/30
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.