Portrait of Ankit Anand is unavailable

Ankit Anand

Alumni

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-05
ArXiv (preprint)
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… (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.
2020-06-19
ArXiv (preprint)
arxiv.org
arxiv.org