I recently started as 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 will work on improving automation for higher-order logic in proof assistants. My Ph.D. supervisor is Jasmin Christian Blanchette.
A formal proof of the expressiveness of deep learning
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow.
Draft paper (PDF)
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