I am a Ph.D. candidate in the Theoretical Computer Science section of the Vrije Universiteit Amsterdam, Netherlands. Coming from a mathematics and computational linguistics background, I formalized a mathematical proof about deep learning using the Isabelle/HOL proof assistant for my M.Sc. thesis. My Ph.D. is part of the Matryoshka project, where I work on extending the superposition calculus to higher-order logic. My Ph.D. supervisor is Jasmin Christian Blanchette.
Phone: +31 20 598 7770
Vrije Universiteit Amsterdam
Department of Computer Science
Section Theoretical Computer Science
De Boelelaan 1081, 1081 HV Amsterdam, The Netherlands
A formal proof of the expressiveness of deep learning
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. Accepted at 8th Conference on Interactive Theorem Proving (ITP 2017).
An Isabelle formalization of the expressiveness of deep learning (extended abstract)
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. Accepted at 2nd Conference on Artificial Intelligence and Theorem Proving (AITP 2017).
Abstract (PDF), Slides (PDF)
An Isabelle formalization of the expressiveness of deep learning
Alexander Bentkamp. M.Sc. thesis, Universität des Saarlandes, 2016.
Expressiveness of deep learning
Alexander Bentkamp. In Klein, G., Nipkow, T., Paulson, L. (eds.), Archive of Formal Proofs, 2016.
Formal proof development