AUTOMATED THEOREM PROVING AGENT WITH MEMORY

Zhang, Heling

Permalink

https://hdl.handle.net/2142/125047 Copy

Description

Title

AUTOMATED THEOREM PROVING AGENT WITH MEMORY

Author(s)

Zhang, Heling

Issue Date

2020

Keyword(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.

Type of Resource

text

Language

eng

Owning Collections