License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.31
URN: urn:nbn:de:0030-drops-167402
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16740/
Go to the corresponding LIPIcs Volume Portal

Vajjha, Koundinya ; Trager, Barry ; Shinnar, Avraham ; Pestun, Vasily

Formalization of a Stochastic Approximation Theorem

pdf-format:
LIPIcs-ITP-2022-31.pdf (0.9 MB)

Abstract

Stochastic approximation algorithms are iterative procedures which are used to approximate a target value in an environment where the target is unknown and direct observations are corrupted by noise. These algorithms are useful, for instance, for root-finding and function minimization when the target function or model is not directly known. Originally introduced in a 1951 paper by Robbins and Monro, the field of Stochastic approximation has grown enormously and has come to influence application domains from adaptive signal processing to artificial intelligence. As an example, the Stochastic Gradient Descent algorithm which is ubiquitous in various subdomains of Machine Learning is based on stochastic approximation theory. In this paper, we give a formal proof (in the Coq proof assistant) of a general convergence theorem due to Aryeh Dvoretzky [Dvoretzky, 1956] (proven in 1956) which implies the convergence of important classical methods such as the Robbins-Monro and the Kiefer-Wolfowitz algorithms. In the process, we build a comprehensive Coq library of measure-theoretic probability theory and stochastic processes.

BibTeX - Entry

@InProceedings{vajjha_et_al:LIPIcs.ITP.2022.31,
  author =	{Vajjha, Koundinya and Trager, Barry and Shinnar, Avraham and Pestun, Vasily},
  title =	{{Formalization of a Stochastic Approximation Theorem}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{31:1--31:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16740},
  URN =		{urn:nbn:de:0030-drops-167402},
  doi =		{10.4230/LIPIcs.ITP.2022.31},
  annote =	{Keywords: Formal Verification, Stochastic Approximation, Stochastic Processes, Probability Theory, Optimization Algorithms}
}

Keywords: Formal Verification, Stochastic Approximation, Stochastic Processes, Probability Theory, Optimization Algorithms
Collection: 13th International Conference on Interactive Theorem Proving (ITP 2022)
Issue Date: 2022
Date of publication: 03.08.2022
Supplementary Material: Software: https://github.com/IBM/FormalML/releases/tag/ITP2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI