# Adversarial Learning to Reason in an Arbitrary Logic

arXiv: https://arxiv.org/abs/2204.02737 · HTML: https://mlsanity.com/paper/2204.02737/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 31 references that are in the map.
- First posted on arXiv 6 Apr 2022.

## Builds on (most cited first, 15 of 15)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Graph Attention Networks](https://mlsanity.com/paper/1710.10903/) (2017)
- [Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm](https://mlsanity.com/paper/1712.01815/) (2017)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Learning to Reason in Large Theories without Imitation](https://mlsanity.com/paper/1905.10501/) (2019)
- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [MizAR 40 for Mizar 40](https://mlsanity.com/paper/1310.2805/) (2013)
- [Property Invariant Embedding for Automated Reasoning](https://mlsanity.com/paper/1911.12073/) (2019)
- [Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic](https://mlsanity.com/paper/1910.11797/) (2019)
- [Training a First-Order Theorem Prover from Synthetic Data](https://mlsanity.com/paper/2103.03798/) (2021)
- [Self-Learned Formula Synthesis in Set Theory](https://mlsanity.com/paper/1912.01525/) (2019)
- [Improving Expressivity of Graph Neural Networks](https://mlsanity.com/paper/2004.05994/) (2020)
- [Internal Guidance for Satallax](https://mlsanity.com/paper/1605.09293/) (2016)
- [The ILLTP Library for Intuitionistic Linear Logic](https://mlsanity.com/paper/1904.06850/) (2019)

## Built on by (most cited first, 1 of 1)

- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)

## Abstract (arXiv)

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.