Portrait of Ankit Anand

Ankit Anand

Associate Industry Member
Adjunct professor
Senior Research Scientist, Google DeepMind

Biography

Ankit is currently a Senior Research Scientist at Google DeepMind Montreal and an Associate Industry Member at Mila - Quebec Artificial Intelligence Institute. His research interests lie at the intersection of reasoning and reinforcement learning . He is also interested in applying contemporary AI methods to make advances in Mathematics and Theoretical Computer Science (automated theorem proving and counterexample generation). Recently, he also worked on LearnLM models to develop generative AI models especially trained for pedagogy and teaching applications and how AI could make an impact for equitable Education.

Previously, he completed his Ph.D at IIT Delhi working with Prof. Mausam and Prof. Parag Singla. During his Ph.D, he worked on making symmetry aware A.I algorithms in context of probabilistic graphical models and Monte Carlo Tree Search algorithms.

Publications

Training a First-Order Theorem Prover from Synthetic Data
Vlad Firoiu
Eser Aygün
Laurent Orseau
Lei Zhang
Shibl Mourad
Learning to Prove from Synthetic Theorems
Eser Aygün
Vlad Firoiu
Laurent Orseau
Shibl Mourad
A major challenge in applying machine learning to automated theorem proving is the scarcity of training data, which is a key ingredient in t… (see more)raining successful deep learning models. To tackle this problem, we propose an approach that relies on training with synthetic theorems, generated from a set of axioms. We show that such theorems can be used to train an automated prover and that the learned prover transfers successfully to human-generated theorems. We demonstrate that a prover trained exclusively on synthetic theorems can solve a substantial fraction of problems in TPTP, a benchmark dataset that is used to compare state-of-the-art heuristic provers. Our approach outperforms a model trained on human-generated problems in most axiom sets, thereby showing the promise of using synthetic data for this task.
Learning representations of Logical Formulae using Graph Neural Networks
Eser Aygün
Shibl Mourad
Pushmeet Kohli
We explore the use of Graph Neural Networks(GNNs) for learning representations of propositional and first-order logical formulae. Tradition… (see more)al non-graphical based approaches like CNNs and LSTMs do not exploit invariant properties like variable renaming and order invariance predominantly present in logical formulae. In this work, we explicitly try to encode these logical invariances using GNNs. We use the task of entailment proposed in Evans et al. [2018] for propositional logic. We also explore our approach for the task of proof length prediction in first-order logic. We use the Mizar-40 dataset to evaluate several representation learning approaches for proof length prediction task. We observe that GNNs significantly outperform the other traditional approaches on both these tasks.