{"ID":2877132,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2508.20671","arxiv_id":"2508.20671","title":"A Unifying Framework for Global Optimization: From Theory to Formalization","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.","short_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 sequen...","url_abs":"https://arxiv.org/abs/2508.20671","url_pdf":"https://arxiv.org/pdf/2508.20671v3","authors":"[\"Gaëtan Serré\",\"Argyris Kalogeratos\",\"Nicolas Vayatis\"]","published":"2025-08-28T11:23:10Z","proceeding":"cs.FL","tasks":"[\"cs.FL\",\"cs.LO\",\"math.OC\",\"math.PR\"]","methods":"[]","has_code":false}