A formal proof of the expressiveness of deep learning

DOI10.1007/978-3-319-66107-0_4zbMath1468.68280OpenAlexW4213004508MaRDI QIDQ5915784

Jasmin Christian Blanchette, Alexander Bentkamp, Dietrich Klakow

Publication date: 4 January 2018

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-02296014/file/paper.pdf

Mathematics Subject Classification ID

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)

Related Items (1)

A formal proof of the expressiveness of deep learning

Uses Software

• Isabelle
• Isabelle/HOL
• Isar
• z3
• HOL
• Algorithm 862
• Jordan Normal Forms
• Groebner_Bases
• Deep_Learning
• Polynomials
• Group-Ring-Module

Cites Work

• Unnamed Item
• Unnamed Item
• Semi-intelligible Isar proofs from machine-generated proofs
• A learning-based fact selector for Isabelle/HOL
• Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL
• 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

This page was built for publication: A formal proof of the expressiveness of deep learning