Formalization of a Stochastic Approximation Theorem
This work formalizes a foundational theorem for stochastic approximation, which is incremental as it provides a verified proof using the Coq proof assistant, benefiting researchers in mathematics and theoretical computer science.
The paper tackled the problem of providing a formal proof for a general convergence theorem in stochastic approximation, originally due to Aryeh Dvoretzky, which implies the convergence of classical methods like Robbins-Monro and Kiefer-Wolfowitz algorithms, by developing a comprehensive Coq library of measure-theoretic probability theory and stochastic processes.
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, 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.