mlsanityData to 7 Oct 2026

Learning Equational Theorem Proving

arXiv 2102.05547 ↗First posted 10 Feb 2021cs.LG cs.AI cs.LOcited by 5

On the map: Offline RL and imitation learning from data → Imitation learning methods

Abstract (arXiv)

We develop Stratified Shortest Solution Imitation Learning (3SIL) to learn equational theorem proving in a deep reinforcement learning (RL) setting. The self-trained models achieve state-of-the-art performance in proving problems generated by one of the top open conjectures in quasigroup theory, the Abelian Inner Mapping (AIM) Conjecture. To develop the methods, we first use two simpler arithmetic rewriting tasks that share tree-structured proof states and sparse rewards with the AIM problems. On these tasks, 3SIL is shown to significantly outperform several established RL and imitation learning methods. The final system is then evaluated in a standalone and cooperative mode on the AIM problems. The standalone 3SIL-trained system proves in 60 seconds more theorems (70.2%) than the complex, hand-engineered Waldmeister system (65.5%). In the cooperative mode, the final system is combined with the Prover9 system, proving in 2 seconds what standalone Prover9 proves in 60 seconds.

Key facts. Cited by 5 papers in the map (data through 7 Oct 2026). Placed in Imitation learning methods, one of 13 directions in Offline RL and imitation learning from data. Builds on 14 of its 44 references that are in the map. First posted on arXiv 10 Feb 2021.

Builds on

14 of 44 references.

Closest ancestors · 2

Same direction, newest first

  1. 2018Self-Imitation Learning14 Jun
  2. 2018Behavioral Cloning from Observation4 May

Other references · 12

  1. 2015Deep Residual Learning for Image Recognitioncited by 51,809
  2. 2017Proximal Policy Optimization Algorithmscited by 14,441
  3. 2016Asynchronous Methods for Deep Reinforcement Learningcited by 2,218
  4. 2019Dota 2 with Large Scale Deep Reinforcement Learningcited by 1,084
  5. 2019Deep Learning for Symbolic Mathematicscited by 266
  6. 2016Sample Efficient Actor-Critic with Experience Replaycited by 185
  7. 2018Reinforcement Learning of Theorem Provingcited by 69
  8. 2018TacticToe: Learning to Prove with Tacticscited by 43
  9. 2019ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for Ecited by 24
  10. 2019Can Neural Networks Learn Symbolic Rewriting?cited by 12
  11. 2019Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logiccited by 8
  12. 2020Tree Neural Networks in HOL4cited by 2

Built on by

Cited by year

Citing papers per year: 2021: 1; 2022: 1; 2023: 0; 2024: 2; 2025: 1.

5 papers.

  1. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  2. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 9
  3. 2021Similarity-Based Equational Inference in Physicscited by 4
  4. 2022PhysNLU: A Language Resource for Evaluating Natural Language Understanding and Explanation Coherence in Physicscited by 3
  5. 2024Application of AI to formal methods - an analysis of current trendscited by 2

Similar, not cited

Close in wording, no citation either way

  1. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
  2. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
  3. 2021Proof Artifact Co-training for Theorem Proving with Language Models
  4. 2025DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
  5. 2025ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
  6. 2026VERIFY-RL: Verifiable Recursive Decomposition for Reinforcement Learning in Mathematical Reasoning
  7. 2026Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers
  8. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience