2 Search Results for "Trager, Barry"

Document
DOI: 10.4230/LIPIcs.ITP.2022.31
Formalization of a Stochastic Approximation Theorem

Authors: Koundinya Vajjha, Barry Trager, Avraham Shinnar, and Vasily Pestun

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

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.
Cite as

Koundinya Vajjha, Barry Trager, Avraham Shinnar, and Vasily Pestun. Formalization of a Stochastic Approximation Theorem. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 31:1-31:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.31},
  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}
}
Document
DOI: 10.4230/DagSemRep.179
Computational Aspects of Commutative Algebra and Algebraic Geometry (Dagstuhl Seminar 9722)

Authors: Eberhard Becker, Wolfram Decker, David Eisenbud, Hendrik W. Lenstra, and Barry Trager

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Eberhard Becker, Wolfram Decker, David Eisenbud, Hendrik W. Lenstra, and Barry Trager. Computational Aspects of Commutative Algebra and Algebraic Geometry (Dagstuhl Seminar 9722). Dagstuhl Seminar Report 179, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1999)

Copy BibTex To Clipboard

@TechReport{becker_et_al:DagSemRep.179,
  author =	{Becker, Eberhard and Decker, Wolfram and Eisenbud, David and Lenstra, Hendrik W. and Trager, Barry},
  title =	{{Computational Aspects of Commutative Algebra and Algebraic Geometry (Dagstuhl Seminar 9722)}},
  pages =	{1--15},
  ISSN =	{1619-0203},
  year =	{1999},
  type = 	{Dagstuhl Seminar Report},
  number =	{179},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.179},
  URN =		{urn:nbn:de:0030-drops-150668},
  doi =		{10.4230/DagSemRep.179},
}
  • Refine by Author
  • 2 Trager, Barry
  • 1 Becker, Eberhard
  • 1 Decker, Wolfram
  • 1 Eisenbud, David
  • 1 Lenstra, Hendrik W.
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Optimization algorithms
  • 1 Mathematics of computing → Nonlinear equations
  • 1 Mathematics of computing → Stochastic processes

  • Refine by Keyword
  • 1 Formal Verification
  • 1 Optimization Algorithms
  • 1 Probability Theory
  • 1 Stochastic Approximation
  • 1 Stochastic Processes

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 1999
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact