Christian Szegedy, Staff Research Scientist, Google
Machine Learning for Mathematical Reasoning
In this talk I will discuss the application of transformer based language models and graph neural networks on automated reasoning tasks in first-order and higher-order logic. After a short introduction of the type of problems addressed and the general search procedure, we give applications of graph neural networks on premise selection and tactic prediction, Also we demonstrate the power of language models various generative reasoning tasks: type inference, conjecturing, assumption and equation completion. Also we give an overview on graph encodings of formulas and their uses.