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.
Type de document :
Communication dans un congrès
ITP 2017: 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. 〈10.1007/3-540-48256-3_12〉
Liste complète des métadonnées

Littérature citée [35 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01599172
Contributeur : Jasmin Christian Blanchette <>
Soumis le : dimanche 1 octobre 2017 - 18:49:15
Dernière modification le : lundi 20 novembre 2017 - 15:14:02

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow. A Formal Proof of the Expressiveness of Deep Learning. ITP 2017: 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. 〈10.1007/3-540-48256-3_12〉. 〈hal-01599172〉

Partager

Métriques

Consultations de la notice

43

Téléchargements de fichiers

13