A Neurally-Guided, Parallel Theorem Prover

Michael Rawson, Giles Reger

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

267 Downloads (Pure)

Abstract

We present a prototype of a neurally-guided automatic theorem prover for first-order logic with equality. The prototype uses a neural network trained on previous proof search attempts to evaluate subgoals based directly on their structure, and hence bias proof search toward success. An existing first-order theorem prover is employed to dispatch easy subgoals and prune branches which cannot be solved. Exploration of the search space is asynchronous with respect to both the evaluation network and the existing prover, allowing for efficient batched neural network execution and for natural parallelism within the prover. Evaluation on the MPTP dataset shows that the prover can improve with learning.
Original languageEnglish
Title of host publicationFroCoS 2019: Frontiers of Combining Systems
DOIs
Publication statusPublished - 2019
EventThe 12th International Symposium on Frontiers of Combining Systems - London, United Kingdom
Duration: 4 Sept 20196 Sept 2019

Publication series

NameLecture Notes in Computer Science
Volume11715

Conference

ConferenceThe 12th International Symposium on Frontiers of Combining Systems
Abbreviated titleFroCoS 2019
Country/TerritoryUnited Kingdom
CityLondon
Period4/09/196/09/19

Keywords

  • ATP
  • Graph Convolutional Network
  • Tableaux
  • MCTS

Fingerprint

Dive into the research topics of 'A Neurally-Guided, Parallel Theorem Prover'. Together they form a unique fingerprint.

Cite this