Applications of Reinforcement Learning to Automated Theorem Proving

In recent years many fields have had their research accelerated through the addition of computers in the research process. Pure mathematics is one such field, and this combination of computers with traditional mathematical research led to the creation of proof assistants. Proof assistants provide mathematicians with tools to ensure that steps taken in logically proving theorems are consistent and do not contain any errors. The rise in artificial intelligence (AI) methods eventually led to the birth of automated theorem proving (ATP), where computers would solve mathematical theorems without requiring human interaction or guidance.\ With the advent of deep learning, computers have become capable at performing highly complex tasks that have previously been seen as impossible for machines to complete. Thanks to this, automated theorem proving is slowly gaining awareness as a potential area for deep learning methods to be applied. Reinforcement learning is a machine learning paradigm that works by learning the optimal action or strategy in certain states or scenarios and has shown to be successful in fields such as game playing and robotics control.\ Current state of the art methods for automated theorem proving employ language modelling techniques for automated theorem proving, though these methods are limited by a lack of planning and search. The motivation of this work is to employ reinforcement learning techniques and algorithms as a means of performing automated theorem proving with better strategies.

Master’s Thesis, Trinity College Dublin