zbMATH — the first resource for mathematics

A neurally-guided, parallel theorem prover. (English) Zbl 1435.68374
Herzig, Andreas (ed.) et al., Frontiers of combining systems. 12th international symposium, FroCoS 2019, London, UK, September 4–6, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11715, 40-56 (2019).
Summary: 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.
For the entire collection see [Zbl 1428.68022].
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Full Text: DOI