A formal proof of the expressiveness of deep learning

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

doi:10.1007/978-3-319-66107-0_4

A formal proof of the expressiveness of deep learning

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

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

29 Downloads (Pure)

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
Title of host publication	Interactive Theorem Proving
Subtitle of host publication	8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings
Editors	Mauricio Ayala-Rincón, César A. Muñoz
Publisher	Springer
Pages	46-64
Number of pages	19
ISBN (Electronic)	9783319661070
ISBN (Print)	9783319661063
DOIs	https://doi.org/10.1007/978-3-319-66107-0_4
Publication status	Published - 2017

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Publisher	Springer
Volume	10499

Funding

Acknowledgment. We thank Lukas Bentkamp, 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 under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka).

Funders	Funder number
European Union’s Horizon 2020 research and innovation program
Horizon 2020 Framework Programme	713999
European Research Council

UN SDGs

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

Access to Document

10.1007/978-3-319-66107-0_4

A formal proof of the expressiveness of deep learningFinal published version, 368 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Copy link address

Cite this

Bentkamp, A., Blanchette, J. C., & Klakow, D. (2017). A formal proof of the expressiveness of deep learning. In M. Ayala-Rincón, & C. A. Muñoz (Eds.), Interactive Theorem Proving: 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings (pp. 46-64). (Lecture Notes in Computer Science (LNCS); Vol. 10499). Springer. https://doi.org/10.1007/978-3-319-66107-0_4

@inproceedings{5ea6bde83fbe4e2487f3f82897ec973b,

title = "A formal proof of the expressiveness of deep learning",

abstract = "Deep learning has had a profound impact on computer science in recentyears, with applications to image recognition, language processing, bioinformatics,and more. Recently, Cohen et al. provided theoretical evidence for the superiorityof deep learning over shallow learning. We formalized their mathematicalproof using Isabelle/HOL. The Isabelle development simplifies and generalizesthe original proof, while working around the limitations of the HOL type system.To support the formalization, we developed reusable libraries of formalizedmathematics, including results about the matrix rank, the Borel measure, andmultivariate polynomials as well as a library for tensor analysis.",

author = "A. Bentkamp and J.C. Blanchette and Dietrich Klakow",

year = "2017",

doi = "10.1007/978-3-319-66107-0_4",

language = "English",

isbn = "9783319661063",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "46--64",

editor = "Mauricio Ayala-Rinc{\'o}n and Mu{\~n}oz, {C{\'e}sar A.}",

booktitle = "Interactive Theorem Proving",

}

Bentkamp, A, Blanchette, JC & Klakow, D 2017, A formal proof of the expressiveness of deep learning. in M Ayala-Rincón & CA Muñoz (eds), Interactive Theorem Proving: 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings. Lecture Notes in Computer Science (LNCS), vol. 10499, Springer, pp. 46-64. https://doi.org/10.1007/978-3-319-66107-0_4

A formal proof of the expressiveness of deep learning. / Bentkamp, A.; Blanchette, J.C.; Klakow, Dietrich.
Interactive Theorem Proving: 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings. ed. / Mauricio Ayala-Rincón; César A. Muñoz. Springer, 2017. p. 46-64 (Lecture Notes in Computer Science (LNCS); Vol. 10499).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A formal proof of the expressiveness of deep learning

AU - Bentkamp, A.

AU - Blanchette, J.C.

AU - Klakow, Dietrich

PY - 2017

Y1 - 2017

N2 - Deep learning has had a profound impact on computer science in recentyears, with applications to image recognition, language processing, bioinformatics,and more. Recently, Cohen et al. provided theoretical evidence for the superiorityof deep learning over shallow learning. We formalized their mathematicalproof using Isabelle/HOL. The Isabelle development simplifies and generalizesthe original proof, while working around the limitations of the HOL type system.To support the formalization, we developed reusable libraries of formalizedmathematics, including results about the matrix rank, the Borel measure, andmultivariate polynomials as well as a library for tensor analysis.

AB - Deep learning has had a profound impact on computer science in recentyears, with applications to image recognition, language processing, bioinformatics,and more. Recently, Cohen et al. provided theoretical evidence for the superiorityof deep learning over shallow learning. We formalized their mathematicalproof using Isabelle/HOL. The Isabelle development simplifies and generalizesthe original proof, while working around the limitations of the HOL type system.To support the formalization, we developed reusable libraries of formalizedmathematics, including results about the matrix rank, the Borel measure, andmultivariate polynomials as well as a library for tensor analysis.

U2 - 10.1007/978-3-319-66107-0_4

DO - 10.1007/978-3-319-66107-0_4

M3 - Conference contribution

SN - 9783319661063

T3 - Lecture Notes in Computer Science (LNCS)

SP - 46

EP - 64

BT - Interactive Theorem Proving

A2 - Ayala-Rincón, Mauricio

A2 - Muñoz, César A.

PB - Springer

ER -

Bentkamp A, Blanchette JC, Klakow D. A formal proof of the expressiveness of deep learning. In Ayala-Rincón M, Muñoz CA, editors, Interactive Theorem Proving: 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings. Springer. 2017. p. 46-64. (Lecture Notes in Computer Science (LNCS)). Epub 2017 Sept 4. doi: 10.1007/978-3-319-66107-0_4

A formal proof of the expressiveness of deep learning

Abstract

Publication series

Funding

UN SDGs

Access to Document

Persistent URL (handle)

Fingerprint

Cite this