APPM Department Colloquium - Christian Szegedy
Christian Szegedy, Staff 91ÃÛÌÒ¸ó Scientist, Google
Machine Learning for Mathematical Reasoning
Ìý
In this talk I will discuss the application of transformer based language 91ÃÛÌÒ¸ó 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 91ÃÛÌÒ¸ó various generative reasoning tasks: type inference, conjecturing, assumption and equation completion. Also we give an overview on graph encodings of formulas and their uses.