@inproceedings{d64986e45d484f6b9f7ca329ddd4c6e8,

title = "A Neurally-Guided, Parallel Theorem Prover",

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.",

keywords = "ATP, Graph Convolutional Network, Tableaux, MCTS",

author = "Michael Rawson and Giles Reger",

year = "2019",

doi = "10.1007/978-3-030-29007-8_3",

language = "English",

series = "Lecture Notes in Computer Science ",

booktitle = "FroCoS 2019: Frontiers of Combining Systems",

note = "The 12th International Symposium on Frontiers of Combining Systems , FroCoS 2019 ; Conference date: 04-09-2019 Through 06-09-2019",

}