A formal proof of the expressiveness of deep learning

DOI10.1007/S10817-018-9481-5MaRDI QIDQ5919583zbMATH OpenOpenAlexWikidataFDO

Authors Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow

Publication date 21 August 2019

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10817-018-9481-5

zbMATH Keywords

convolutional arithmetic circuitsdeep learningformalizationIsabelle/HOLmachine learningtensors

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Artificial neural networks and deep learning (68T07) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• A formal proof of the expressiveness of deep learning
• Towards the automatic mathematician
• The unreasonable effectiveness of deep learning in artificial intelligence
• Deep network guided proof search
• Automated proof synthesis for the minimal propositional logic with deep neural networks

Cites work

• A formal proof of the expressiveness of deep learning
• A formulation of the simple theory of types
• A General Framework for the Analysis of Sets of Constraints
• A learning-based fact selector for Isabelle/HOL
• Algorithm 862
• Canonical Big Operators
• Concrete semantics. With Isabelle/HOL
• Edinburgh LCF. A mechanized logic of computation
• Fast LCF-Style Proof Reconstruction for Z3
• Formalization \textit{of} quantum protocols using Coq
• Gröbner bases of modules and Faugère's F₄ algorithm in Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• On the volume of tubular neighborhoods of real algebraic varieties
• Semi-intelligible Isar proofs from machine-generated proofs
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• The probability that a slightly perturbed numerical analysis problem is difficult
• Theorem Proving in Higher Order Logics
• Three chapters of measure theory in Isabelle/HOL

Cited in

(6)

• On the proof complexity of deep inference
• Formalization of operations of block matrix based on Coq
• An Algorithmic Interpretation of a Deep Inference System
• A formal proof of the expressiveness of deep learning
• Formal specification for deep neural networks
• Towards formal XAI: formally approximate minimal explanations of neural networks

Describes a project that uses

Uses Software

• Isabelle/HOL
• Metis
• Isar
• LCF
• Archive of Formal Proofs
• Groebner_Bases
• Deep_Learning
• Polynomials
• Group-Ring-Module
• Matrix_Tensor
• z3
• HOL
• Jordan Normal Forms
• Isabelle
• Sledgehammer
• Algorithm 862

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5919583)