A formal proof of the expressiveness of deep learning
From MaRDI portal
Publication:5919583
DOI10.1007/s10817-018-9481-5zbMath1468.68281OpenAlexW2747942685MaRDI QIDQ5919583
Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow
Publication date: 21 August 2019
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-018-9481-5
Artificial neural networks and deep learning (68T07) Learning and adaptive systems in artificial intelligence (68T05) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Uses Software
Cites Work
- Unnamed Item
- Semi-intelligible Isar proofs from machine-generated proofs
- A learning-based fact selector for Isabelle/HOL
- Isabelle/HOL. A proof assistant for higher-order logic
- Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL
- Edinburgh LCF. A mechanized logic of computation
- Concrete Semantics
- Three Chapters of Measure Theory in Isabelle/HOL
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- A General Framework for the Analysis of Sets of Constraints
- Canonical Big Operators
- Algorithm 862
- The probability that a slightly perturbed numerical analysis problem is difficult
- On the volume of tubular neighborhoods of real algebraic varieties
- Theorem Proving in Higher Order Logics
- Fast LCF-Style Proof Reconstruction for Z3
- A formulation of the simple theory of types
- A formal proof of the expressiveness of deep learning
This page was built for publication: A formal proof of the expressiveness of deep learning
