A Formal Proof of the Expressiveness of Deep Learning

Alexander Bentkamp; Jasmin Christian Blanchette; Dietrich Klakow

doi:10.1007/s10817-018-9481-5

A Formal Proof of the Expressiveness of Deep Learning

Alexander Bentkamp^*, Jasmin Christian Blanchette, Dietrich Klakow

^*Corresponding author for this work

Research output: Contribution to Journal › Article › Academic › peer-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 language	English
Pages (from-to)	347-368
Number of pages	22
Journal	Journal of Automated Reasoning
Volume	63
Issue number	2
DOIs	https://doi.org/10.1007/s10817-018-9481-5
Publication status	Published - Aug 2019

Funding

We thank Lukas Bentkamp, Johannes Hölzl, Robert Lewis, Anders Schlichtkrull, Mark Summerfield, and the anonymous reviewers for suggesting many textual improvements. The work has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 Research and Innovation Program (Grant Agreement No. 713999, Matryoshka).

Funders	Funder number
Horizon 2020 Framework Programme	713999
European Research Council

Keywords

Isabelle
HOL
Deep learning
Machine learning
Convolutional arithmetic circuits
Formalization
Tensors

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1007/s10817-018-9481-5

Persistent URL (handle)

Persistent link

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 = "Isabelle, HOL, Deep learning, Machine learning, Convolutional arithmetic circuits, Formalization, Tensors",

author = "Alexander Bentkamp and Blanchette, {Jasmin Christian} and Dietrich Klakow",

year = "2019",

month = aug,

doi = "10.1007/s10817-018-9481-5",

language = "English",

volume = "63",

pages = "347--368",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "2",

}

TY - JOUR

T1 - A Formal Proof of the Expressiveness of Deep Learning

AU - Bentkamp, Alexander

AU - Blanchette, Jasmin Christian

AU - Klakow, Dietrich

PY - 2019/8

Y1 - 2019/8

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 - Isabelle

KW - HOL

KW - Deep learning

KW - Machine learning

KW - Convolutional arithmetic circuits

KW - Formalization

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

AN - SCOPUS:85053776418

SN - 0168-7433

VL - 63

SP - 347

EP - 368

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 2

ER -

A Formal Proof of the Expressiveness of Deep Learning

Abstract

Funding

Keywords

UN SDGs

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this