Automated theorem proving (ATP) is a tool important in mathematics as well as integrated circuit design or software and hardware verification. However, current systems are still far from human capabilities.

A recent paper by DeepMind proposes hindsight experience replay for ATP. Researchers suggest turning clauses reached in proof attempts into goals in hindsight. That way, lots of “auxiliary” theorems with proofs are generated, even when no theorem from the original set can be proven. The approach starts from a simple given-clause algorithm and trains itself based on its own attempts. A transformer network using spectral features is trained to provide a scoring function for the prover.

It is shown that the proposed approach achieves comparable performance to state-of-the-art and generates shorter proofs. The method allows the learner to improve more smoothly than when learning from proven conjectures alone.

“Traditional automated theorem provers for first-order logic depend on speed-optimized search and many handcrafted heuristics that are designed to work best over a wide range of domains. Machine learning approaches in literature either depend on these traditional provers to bootstrap themselves or fall short on reaching comparable performance. In this paper, we propose a general incremental learning algorithm for training domain specific provers for first-order logic without equality, based only on a basic given-clause algorithm, but using a learned clause-scoring function. Clauses are represented as graphs and presented to transformer networks with spectral features. To address the sparsity and the initial lack of training data as well as the lack of a natural curriculum, we adapt hindsight experience replay to theorem proving, so as to be able to learn even when no proof can be found. We show that provers trained this way can match and sometimes surpass state-of-the-art traditional provers on the TPTP dataset in terms of both quantity and quality of the proofs.”

Research paper: Aygün, E., “Proving Theorems using Incremental Learning and Hindsight Experience Replay”, 2021. Link: https://arxiv.org/abs/2112.10664

Source: https://www.technology.org/2021/12/23/proving-theorems-using-incremental-learning-and-hindsight-experience-replay/