The Mathematical Game

TL;DR

This paper explores enhancing the Holophrasm neural theorem prover, which uses Monte Carlo Tree Search, by integrating alternative game tree search algorithms to improve its performance.

Contribution

It introduces the use of different game tree search algorithms to improve the performance of the neural theorem prover Holophrasm.

Findings

Improved theorem proving performance with new search algorithms

Enhanced neural theorem prover efficiency

Potential for broader application in automated reasoning

Abstract

Monte Carlo Tree Search can be used for automated theorem proving. Holophrasm is a neural theorem prover using MCTS combined with neural networks for the policy and the evaluation. In this paper we propose to improve the performance of the Holophrasm theorem prover using other game tree search algorithms.