Formalization of optimization algorithms

 Formalization of stochastic iterative optimization algorithm🔗

Gaëtan Serré

This documentation is associated with the paper A Unifying Framework for Global Optimization: From Theory to Formalization by Gaëtan Serré, Argyris Kalogeratos and Nicolas Vayatis. It presents an abstract definition of stochastic iterative optimization algorithms along with a construction of probability measures on the space of the iterations of the algorithm. This documentation describes the L∃∀N formalization of this framework. To illustrate the framework, we also present the formalization of two algorithms: Pure Random Search and LIPO  (Malherbe and Vayatis, 2017)Cédric Malherbe and Nicolas Vayatis, 2017. “Global optimization of Lipschitz functions”. In International conference on machine learning.. To see a more complete example of the use of the framework, see the formalization of Proposition 1 of Malherbe and Vayatis (2017)¹.

Contents

  1. 1. Abstract algorithm
  2. 2. Some examples