First-Order Problem Solving through Neural MCTS based Reinforcement Learning

TL;DR

This paper introduces Persephone, a framework that uses neural MCTS and reinforcement learning to solve combinatorial problems modeled as semantic games derived from first-order logic, aiming for autonomous problem solving.

Contribution

It presents Persephone, a novel framework that maps interpreted FOL problems to semantic games and employs an adapted AlphaZero algorithm for autonomous problem solving.

Findings

Successfully maps FOL problems to semantic games

Learns to play semantic games using neural MCTS

Achieves autonomous problem solving without human intervention

Abstract

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.