First-Order Problem Solving through Neural MCTS based Reinforcement Learning
This work is significant for researchers in AI and logic programming who are interested in automated problem solving and the application of reinforcement learning to formal systems.
This paper tackles the problem of solving combinatorial problems described by interpreted first-order logic (FOL) statements by mapping them to two-player semantic games. The authors adapt the AlphaZero algorithm to learn to play these semantic games, aiming to solve specific instances of combinatorial problems.
The formal semantics of an interpreted first-order logic (FOL) statement can be given in Tarskian Semantics or a basically equivalent Game Semantics. The latter maps the statement and the interpretation into a two-player semantic game. Many combinatorial problems can be described using interpreted FOL statements and can be mapped into a semantic game. Therefore, learning to play a semantic game perfectly leads to the solution of a specific instance of a combinatorial problem. We adapt the AlphaZero algorithm so that it becomes better at learning to play semantic games that have different characteristics than Go and Chess. We propose a general framework, Persephone, to map the FOL description of a combinatorial problem to a semantic game so that it can be solved through a neural MCTS based reinforcement learning algorithm. Our goal for Persephone is to make it tabula-rasa, mapping a problem stated in interpreted FOL to a solution without human intervention.