Automated theorem proving agent with memory
Heling Zhang · Illinois Digital Environment for Access to Learning and Scholarship (University of Illinois at Urbana-Champaign) · 2020
Proof assistants are interactive software tools that performs automatic proof checking. Training deep learning agents that are capable of interacting with proof assistants provide a novel way of developing automated theorem proving (ATP) systems. We observe that existing methods in this field, either supervised learning methods or RL, are all based on locality assumptions–the agent generates proof tactics conditioning only on the information in the most recent time step, discarding any information in previous time steps. However, the correctness of such assumptions has never been verified. We propose a method that introduces global information in training deep-learning based ATP models. Our contributions can be summarized as follows: (a) we construct a LSTM-like memory mechanism across time steps for deep learning-based ATP agents, and (b) we build a pipeline for end-to-end training by constructing a differentiable estimation of the proof assistant, which can be viewed as a discrete function. We show the effectiveness of our method by building on the state-of-the-art ATP model, ASTatics.