Adversarial Learning to Reason in an Arbitrary Logic

TL;DR

This paper introduces a reinforcement learning-based Monte-Carlo simulation method for automated theorem proving that can operate across arbitrary logical systems without prior datasets or human knowledge.

Contribution

It presents a novel, generalizable approach to automated theorem proving applicable to any logic, including those without existing proof datasets.

Findings

Effective in multiple logical systems

Outperforms random data training

Enables theorem proving in previously unapproachable logics

Abstract

Existing approaches to learning to prove theorems focus on particular logics and datasets. In this work, we propose Monte-Carlo simulations guided by reinforcement learning that can work in an arbitrarily specified logic, without any human knowledge or set of problems. Since the algorithm does not need any training dataset, it is able to learn to work with any logical foundation, even when there is no body of proofs or even conjectures available. We practically demonstrate the feasibility of the approach in multiple logical systems. The approach is stronger than training on randomly generated data but weaker than the approaches trained on tailored axiom and conjecture sets. It however allows us to apply machine learning to automated theorem proving for many logics, where no such attempts have been tried to date, such as intuitionistic logic or linear logic.