Adversarial Learning to Reason in an Arbitrary Logic
This enables machine learning-based automated theorem proving for many logics where no prior attempts exist, such as intuitionistic or linear logic, though it is incremental compared to tailored methods.
The authors tackled the problem of automated theorem proving across arbitrary logical systems without requiring training datasets, proposing a Monte-Carlo simulation method guided by reinforcement learning that works in multiple logics like intuitionistic and linear logic. The result is a method that outperforms training on random data but is weaker than approaches using tailored axiom sets, enabling machine learning applications in logics previously untried.
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.