Guiding Automated Theorem Proving with Machine Learning

Mathematics can be formalized to allow a computer to execute proof steps and recognize whether a statement has been proven. Computer systems that automate mathematics are called automated theorem provers (ATP). The system has inference rules, which prescribe how the axioms and conjecture may be handled during a search for a proof. The number of possible choices at each point in the process can become very large. It would be useful to have a system that can predict which choices are better than other ones, so that a proof may be reached earlier. In this study, automated theorem proving is combined with machine learning, a field concerned with learning patterns in data. The machine learning component, a graph neural network, is tasked with learning to predict which choices are useful and which ones are not. This information can be learned from already finished proofs. The overall goal is to improve the performance of the automated theorem proving systems in terms of theorems proven in a particular time period. It is shown that instantiation and rewriting-based proving systems can be integrated with machine learning and that the systems improve on benchmark datasets.