A formal proof of the expressiveness of deep learning

A. Bentkamp, J.C. Blanchette, Dietrich Klakow

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

Deep learning has had a profound impact on computer science in recent
years, with applications to image recognition, language processing, bioinformatics,
and more. Recently, Cohen et al. provided theoretical evidence for the superiority
of deep learning over shallow learning. We formalized their mathematical
proof using Isabelle/HOL. The Isabelle development simplifies and generalizes
the original proof, while working around the limitations of the HOL type system.
To support the formalization, we developed reusable libraries of formalized
mathematics, including results about the matrix rank, the Borel measure, and
multivariate polynomials as well as a library for tensor analysis.
Original languageEnglish
Title of host publicationInteractive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017, Proceedings
PublisherSpringer
Pages46-64
Volume10499
Publication statusPublished - 2017

Publication series

NameLNCS

Fingerprint Dive into the research topics of 'A formal proof of the expressiveness of deep learning'. Together they form a unique fingerprint.

  • Cite this

    Bentkamp, A., Blanchette, J. C., & Klakow, D. (2017). A formal proof of the expressiveness of deep learning. In Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017, Proceedings (Vol. 10499, pp. 46-64). (LNCS). Springer.