Abstract:
We have a lot of tools (static analyzers, type systems, proof assistants, linters) for analysing and proving things about programs written as source code in traditional languages. However, we are currently poorly equipped to analyze and prove things about machine learning models, simply because the resulting programs are represented as a bunch of weights instead of source code. I propose to generate source code from the weights of trained machine learning models, and to prove things about that code.
In this tech talk, I will run a live demo: I will train a toy model, I will generate source code from that model, I will use a sat-solver to find an input which contradicts the specification, and I will use this counter-example to improve the model and the generated source code. I will then discuss possible directions for scaling this proof of concept to more interesting models and programs.
Bio:
Samuel Gélineau studied under Brigitte Pientka and Jörg Kienzle at McGill University, where he did a master’s thesis on Aspect-Oriented Programming. In it, he argued that aspects could be represented as endo-functions (f :: a -> a), and that the property f∘g = g∘f captured the otherwise-vague notion of whether two aspects were compatible with each other. As a young research assistant, he then explored how the then-nascent multi-touch technologies could revolutionize user interfaces, especially on large screens. Sadly, the industry did not adopt his idea to zoom in and out of a giant static page with zero sub-menus.
Samuel then joined the industry, most recently as the lead architect of a Haskell codebase with half a million lines of code. He continues to do research in his free time, with various collaborators over the web and locally in Montreal. His two most recent publications are both on the topic of macros and type systems. If we also look at his blog (gelisam.com), his open source projects (github.com/gelisam), and his YouTube channel (haskellcat.com), we see a much broader set of interests, including generalizing Theorems For Free to dependent types, writing functions which are commutative by construction, composing recursion-schemes, and compiling premonoidal categories in order to implement sub-structural type systems. Most relevant for this talk is his recent collaboration with Torsten Scholak on a gradually-typed version of HaskTorch.