# Efficient Neural Clause-Selection Reinforcement

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 22 of its 51 references that are in the map.
- First posted on arXiv 10 Mar 2025.

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

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [Layer Normalization](https://mlsanity.com/paper/1607.06450/) (2016)
- [Playing Atari with Deep Reinforcement Learning](https://mlsanity.com/paper/1312.5602/) (2013)
- [A* Sampling](https://mlsanity.com/paper/1411.0030/) (2014)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [ENIGMA: Efficient Learning-based Inference Guiding Machine](https://mlsanity.com/paper/1701.06532/) (2017)
- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019)
- [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)
- [Hammering Mizar by Learning Clause Guidance](https://mlsanity.com/paper/1904.01677/) (2019)
- [An operator view of policy gradient methods](https://mlsanity.com/paper/2006.11266/) (2020)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [Vampire With a Brain Is a Good ITP Hammer](https://mlsanity.com/paper/2102.03529/) (2021)
- [The Role of Entropy in Guiding a Connection Prover](https://mlsanity.com/paper/2105.14706/) (2021)
- [Learning Theorem Proving Components](https://mlsanity.com/paper/2107.10034/) (2021)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations](https://mlsanity.com/paper/2305.08676/) (2023)
- [Regularization in Spider-Style Strategy Discovery and Schedule Construction](https://mlsanity.com/paper/2403.12869/) (2024)

## Abstract (arXiv)

Clause selection is arguably the most important choice point in saturation-based theorem proving. Framing it as a reinforcement learning (RL) task is a way to challenge the human-designed heuristics of state-of-the-art provers and to instead automatically evolve -- just from prover experiences -- their potentially optimal replacement. In this work, we present a neural network architecture for scoring clauses for clause selection that is powerful yet efficient to evaluate. Following RL principles to make design decisions, we integrate the network into the Vampire theorem prover and train it from successful proof attempts. An experiment on the diverse TPTP benchmark finds the neurally guided prover improve over a baseline strategy, from which it initially learns -- in terms of the number of in-training-unseen problems solved under a practically relevant, short CPU instruction limit -- by 20%.