A Formal Proof of the Expressiveness of Deep Learning

被引：2

作者：

Bentkamp, Alexander ^{[1
,2
]}

Blanchette, Jasmin Christian ^{[1
,3
]}

Klakow, Dietrich ^{[2
]}

机构：

[1] Vrije Univ Amsterdam, Amsterdam, Netherlands

[2] Univ Saarland, Saarland Informat Campus, Saarbrucken, Germany

[3] Max Planck Inst Informat, Saarland Informat Campus, Saarbrucken, Germany

来源：

INTERACTIVE THEOREM PROVING (ITP 2017) | 2017年 / 10499卷

基金：

欧洲研究理事会;

关键词：

RECONSTRUCTION;

D O I：

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

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：46 / 64

页数：19

共 50 条

[1] A Formal Proof of the Expressiveness of Deep Learning
Alexander Bentkamp
Jasmin Christian Blanchette
Dietrich Klakow
Journal of Automated Reasoning, 2019, 63 : 347 - 368
[2] A Formal Proof of the Expressiveness of Deep Learning
Bentkamp, Alexander
Blanchette, Jasmin Christian
Klakow, Dietrich
JOURNAL OF AUTOMATED REASONING, 2019, 63 (02) : 347 - 368
[3] Improving the Expressiveness of Deep Learning Frameworks with Recursion
Jeong, Eunji
Jeong, Joo Seong
Kim, Soojeong
Yu, Gyeong-In
Chun, Byung-Gon
EUROSYS '18: PROCEEDINGS OF THE THIRTEENTH EUROSYS CONFERENCE, 2018,
[4] Controlling the emotional expressiveness of synthetic speech: a deep learning approach
Tits, Noe
4OR-A QUARTERLY JOURNAL OF OPERATIONS RESEARCH, 2022, 20 (01): : 165 - 166
[5] Controlling the emotional expressiveness of synthetic speech: a deep learning approach
Noé Tits
4OR, 2022, 20 : 165 - 166
[6] Balancing expressiveness in formal approaches to concurrency
Jones, Cliff B.
Hayes, Ian J.
Colvin, Robert J.
FORMAL ASPECTS OF COMPUTING, 2015, 27 (03) : 475 - 497
[7] Formal proof
Atkinson, Ti-Grace
ARTFORUM INTERNATIONAL, 2008, 46 (09): : 111 - +
[8] A Methodology for Controlling the Emotional Expressiveness in Synthetic Speech - a Deep Learning approach
Tits, Noe
2019 8TH INTERNATIONAL CONFERENCE ON AFFECTIVE COMPUTING AND INTELLIGENT INTERACTION WORKSHOPS AND DEMOS (ACIIW), 2019, : 6 - 10
[9] A Formal Treatment of Expressiveness and Relevance of Digital Evidence
Gruber, Jan
Humml, Merlin
DIGITAL THREATS: RESEARCH AND PRACTICE, 2023, 4 (03):
[10] FORMAL PROOF LEARNING AND IDENTITY CONSTRUCTION IN THE ENTRANCE TO A COMMUNITY OF PRACTICE
Leticia Losano, Ana
Ester Villarreal, Monica
PME 34 BRAZIL: PROCEEDINGS OF THE 34TH CONFERENCE OF THE INTERNATIONAL GROUP FOR THE PSYCHOLOGY OF MATHEMATICS EDUCATION, VOL 2: MATHEMATICS IN DIFFERENT SETTINGS, 2010, : 63 - 63

← 1 2 3 4 5 →