Expressiveness of Deep Learning

Title:	Expressiveness of Deep Learning
Author:	Alexander Bentkamp (bentkamp /at/ gmail /dot/ com)
Submission date:	2016-11-10
Abstract:	Deep learning has had a profound impact on computer science in recent years, with applications to search engines, image recognition and language processing, bioinformatics, and more. Recently, Cohen et al. provided theoretical evidence for the superiority of deep learning over shallow learning. This formalization of their work simplifies and generalizes the original proof, while working around the limitations of the Isabelle type system. To support the formalization, I developed reusable libraries of formalized mathematics, including results about the matrix rank, the Lebesgue measure, and multivariate polynomials, as well as a library for tensor analysis.
BibTeX:	@article{Deep_Learning-AFP, author = {Alexander Bentkamp}, title = {Expressiveness of Deep Learning}, journal = {Archive of Formal Proofs}, month = nov, year = 2016, note = {\url{http://isa-afp.org/entries/Deep_Learning.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Jordan_Normal_Form, Polynomial_Interpolation, Polynomials, VectorSpace
Used by:	QHLProver
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.