Efficient Neural Clause-Selection Reinforcement

Martin Suda

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-d…