A Formal Proof of the Expressiveness of Deep Learning
A Formal Proof of the Expressiveness of Deep Learning
复制标题
深度学习表现力的形式化证明
DOI：
10.1007/s10817-018-9481-5
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
D. Klakow
中科院分区：
文献类型：
--
作者：
Alexander Bentkamp;J. Blanchette;D. Klakow
近年来，深度学习对计算机科学产生了深远的影响，应用于图像识别、语言处理、生物信息学等领域。最近，Cohen等人为深度学习优于浅层学习提供了理论证据。我们使用Isabelle/HOL形式化了他们的数学证明。Isabelle的开发简化和推广了原始证明，同时解决了HOL类型系统的限制。为了支持形式化，我们开发了形式化数学的可重用库，包括矩阵秩，Borel测度和多元多项式以及张量分析库的结果。
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.
登录
查看更多内容
DOI：
10.1007/s10817-016-9362-8
发表时间：
2016-10-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Blanchette, Jasmin Christian;Greenaway, David;Urban, Josef
通讯作者：
Urban, Josef
《Isabelle/HOL》中的测度论三章
DOI：
10.1007/978-3-642-22863-6_12
发表时间：
2011
期刊：
影响因子：
--
作者：
Johannes Hölzl;Armin Heller
通讯作者：
Armin Heller
来自机器生成的证明的半可理解的 Isar 证明
DOI：
10.1007/s10817-015-9335-3
发表时间：
2016
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jasmin Christian Blanchette;Sascha Böhme;Mathias Fleury;Steffen Juilf Smolka;Albert Steckermeier
通讯作者：
Albert Steckermeier
DOI：
10.1090/s0025-5718-08-02060-7
发表时间：
2008
期刊：
Math. Comput.
影响因子：
--
作者：
P. Bürgisser;F. Cucker;M. Lotz
通讯作者：
M. Lotz