A Formal Proof of the Expressiveness of Deep Learning

Research output: Contribution to JournalArticleAcademicpeer-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
Pages (from-to)1-22
Number of pages22
JournalJournal of Automated Reasoning
DOIs
Publication statusAccepted/In press - 22 Sep 2018

Fingerprint

Image recognition
Bioinformatics
Computer science
Tensors
Polynomials
Processing
Deep learning

Keywords

  • Convolutional arithmetic circuits
  • Deep learning
  • Formalization
  • Isabelle/HOL
  • Machine learning
  • Tensors

Cite this

@article{a9bfccf4670d4715bd7dc9214b784650,
title = "A Formal Proof of the Expressiveness of Deep Learning",
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.",
keywords = "Convolutional arithmetic circuits, Deep learning, Formalization, Isabelle/HOL, Machine learning, Tensors",
author = "Alexander Bentkamp and Blanchette, {Jasmin Christian} and Dietrich Klakow",
year = "2018",
month = "9",
day = "22",
doi = "10.1007/s10817-018-9481-5",
language = "English",
pages = "1--22",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",

}

A Formal Proof of the Expressiveness of Deep Learning. / Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich.

In: Journal of Automated Reasoning, 22.09.2018, p. 1-22.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - A Formal Proof of the Expressiveness of Deep Learning

AU - Bentkamp, Alexander

AU - Blanchette, Jasmin Christian

AU - Klakow, Dietrich

PY - 2018/9/22

Y1 - 2018/9/22

N2 - 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.

AB - 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.

KW - Convolutional arithmetic circuits

KW - Deep learning

KW - Formalization

KW - Isabelle/HOL

KW - Machine learning

KW - Tensors

UR - http://www.scopus.com/inward/record.url?scp=85053776418&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85053776418&partnerID=8YFLogxK

U2 - 10.1007/s10817-018-9481-5

DO - 10.1007/s10817-018-9481-5

M3 - Article

SP - 1

EP - 22

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

ER -