A Unifying Framework for Global Optimization: From Theory to Formalization
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910037372305408 |
|---|---|
| author | Serré, Gaëtan Kalogeratos, Argyris Vayatis, Nicolas |
| author_facet | Serré, Gaëtan Kalogeratos, Argyris Vayatis, Nicolas |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_20671 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Unifying Framework for Global Optimization: From Theory to Formalization Serré, Gaëtan Kalogeratos, Argyris Vayatis, Nicolas Formal Languages and Automata Theory Logic in Computer Science Optimization and Control Probability 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. |
| title | A Unifying Framework for Global Optimization: From Theory to Formalization |
| topic | Formal Languages and Automata Theory Logic in Computer Science Optimization and Control Probability |
| url | https://arxiv.org/abs/2508.20671 |