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.

翻译：斯托切近似算法是一种迭接程序,用来在目标未知、直接观测被噪音破坏的环境中估计目标值,例如,当目标函数或模型不直接为人所知时,这些算法对根查和功能最小化有用。最初在Robbins和Monro1951年的论文中引入了斯托切近似法,这个领域已经大为发展,已经影响到从适应信号处理到人工智能等应用领域。举例来说,在机器学习的各个子领域普遍存在的斯托切特梯源算法是基于随机近似理论的。在本文中,我们(在科克验证助理)正式证明,由于Aryeh Dvoretzky,一个普遍的趋同理论,这意味着Robbins-Monro和Kiefer-Wolfowitz算法等重要古典方法的结合。在这个过程中,我们建立了一个测量理论理论和研究过程的综合性 Coq 库。