论文标题
随机近似定理的形式化
Formalization of a Stochastic Approximation Theorem
论文作者
论文摘要
随机近似算法是迭代过程，用于在目标未知且直接观察结果被噪声损坏的环境中近似目标值。例如，当目标函数或模型不直接知道时，这些算法对于根找到和最小化是有用的。随机近似领域最初是在1951年的1951年论文中引入的，它已经巨大增长，并且已经影响了从自适应信号处理到人工智能的应用领域。例如，在机器学习的各个子域中无处不在的随机梯度下降算法是基于随机近似理论。在本文中，由于Aryeh dvoretzky，我们给出了正式的证明（在COQ证明助手）中，这意味着重要的经典方法（例如Robbins-Monro和Kiefer-Wolfowitz算法）的收敛性。在此过程中，我们构建了一个综合的COQ库库理论概率理论和随机过程。
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.
