Files in this item



application/pdfSP20-ECE499-Thesis-Zhang, Heling.pdf (720kB)Restricted to U of Illinois
(no description provided)PDF


Title:Automated theorem proving agent with memory
Author(s):Zhang, Heling
Contributor(s):Koyejo, Oluwasanmi
Subject(s):automated theorem proving
deep learning
artificial intellegence
Abstract: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.
Issue Date:2020-05
Date Available in IDEALS:2020-06-12

This item appears in the following Collection(s)

Item Statistics