# Formalization of a Stochastic Approximation Theorem

arXiv: https://arxiv.org/abs/2202.05959 · HTML: https://mlsanity.com/paper/2202.05959/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 42 references that are in the map.
- First posted on arXiv 12 Feb 2022.

## Builds on (most cited first, 6 of 6)

- [Developing Bug-Free Machine Learning Systems With Formal Mathematics](https://mlsanity.com/paper/1706.08605/) (2017)
- [CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq](https://mlsanity.com/paper/2009.11403/) (2020)
- [A formally verified proof of the Central Limit Theorem](https://mlsanity.com/paper/1405.7012/) (2014)
- [A Separation Logic for Concurrent Randomized Programs](https://mlsanity.com/paper/1802.02951/) (2018)
- [Verification of ML Systems via Reparameterization](https://mlsanity.com/paper/2007.06776/) (2020)
- [A Coq Formalization of Lebesgue Integration of Nonnegative Functions](https://mlsanity.com/paper/2104.05256/) (2021)

## Built on by (most cited first, 5 of 5)

- [Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach](https://mlsanity.com/paper/2511.03618/) (2025)
- [Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral](https://mlsanity.com/paper/2503.19605/) (2025)
- [Formalized Hopfield Networks and Boltzmann Machines](https://mlsanity.com/paper/2512.07766/) (2025)
- [An abstract effective convergence theorem for stochastic processes, with applications to stochastic approximation](https://mlsanity.com/paper/2504.12922/) (2025)
- [Decentralized Online Learning for Random Inverse Problems Over Graphs](https://mlsanity.com/paper/2303.11789/) (2023)

## Abstract (arXiv)

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.