Portrait de Ankit Anand

Ankit Anand

Membre industriel associé
Professeur associé
Chercheur scientifique principal, Google DeepMind
Site web
Google Scholar

Biographie

Ankit est actuellement chercheur principal chez Google DeepMind Montréal et membre industriel associé à Mila - Institut québécois d'intelligence artificielle. Ses intérêts de recherche se situent à l'intersection du raisonnement et de l'apprentissage par renforcement. Il s'intéresse également à l'application de méthodes d'IA contemporaines pour réaliser des avancées en mathématiques et en informatique théorique (démonstration automatisée de théorèmes et génération de contre-exemples). Récemment, il a également travaillé sur les modèles LearnLM pour développer des modèles génératifs d'IA spécialement entraînés pour la pédagogie et les applications d'enseignement et sur la façon dont l'IA pourrait avoir un impact pour une éducation équitable.

Auparavant, il a terminé son doctorat à l'IIT Delhi en travaillant avec les professeurs Mausam et Parag Singla. Au cours de son doctorat, il a travaillé sur la symétrie des algorithmes d'IA dans le contexte des modèles graphiques probabilistes et des algorithmes de recherche arborescente de Monte Carlo.

Publications

Training a First-Order Theorem Prover from Synthetic Data
Vlad Firoiu
Eser Aygün
Ankit Anand
Zafarali Ahmed
Xavier Glorot
Laurent Orseau
Lei Zhang
Doina Precup
Shibl Mourad
2021-03-04
ArXiv (prépublication)
arxiv.org
arxiv.org
Learning to Prove from Synthetic Theorems
Eser Aygün
Zafarali Ahmed
Ankit Anand
Vlad Firoiu
Xavier Glorot
Laurent Orseau
Doina Precup
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… (voir plus)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.
2020-06-18
ArXiv (prépublication)
arxiv.org
arxiv.org
Learning representations of Logical Formulae using Graph Neural Networks
Xavier Glorot
Ankit Anand
Eser Aygün
Shibl Mourad
Pushmeet Kohli
Doina Precup
We explore the use of Graph Neural Networks(GNNs) for learning representations of propositional and first-order logical formulae. Tradition… (voir plus)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.
2018-12-31
(publié)
www.semanticscholar.org