Ankit Anand and Abbas Mehrabian | From Theorem Proving to Disproving
CMSA Mathematics and Machine Learning Closing Workshop
10/28/2024
Ankit Anand, Google Deepmind Montreal, Abbas Mehrabian, Google Deepmind Montreal
Title: From Theorem Proving to Disproving: Modern machine learning versus classical heuristic search in automated theorem proving and extremal graph theory
Abstract: Machine learning is widely believed to outperform classical methods, but this is not always the case. Firstly, we describe how we adapted the idea of hindsight experience replay from reinforcement learning to the automated theorem proving domain, so as to use the intermediate data generated during unsuccessful proofs. We show that provers trained in this way can outperform previous machine learning approaches and compete with the state-of-the-art heuristic-based theorem prover E in its best configuration, on the popular benchmarks MPTP2078, M2k and Mizar40. The proofs generated by our algorithm are also almost always significantly shorter than E’s proofs. Based on this paper, which was presented at ICML 2022: https://proceedings.mlr.press/v162/ay.... Secondly, we study a central extremal graph theory problem inspired by a 1975 conjecture of Erdős, which aims to find graphs with a given size (number of nodes) that maximize the number of edges without having 3- or 4-cycles. We formulate this problem as a sequential decision-making problem and compare AlphaZero, a neural network-guided tree search, with tabu search, a heuristic local search method. Using either method, by introducing a curriculum—jump-starting the search for larger graphs using good graphs found at smaller sizes—we improve the state-of-the-art lower bounds for several sizes. Joint work with Tudor Berariu, Joonkyung Lee, Anurag Murty Naredla, Adam Zsolt Wagner, and other colleagues at Google DeepMind. Based on this paper, which was presented at IJCAI 2024: https://arxiv.org/abs/2311.03583.