mlsanityData to 7 Oct 2026

Hammering Mizar by Learning Clause Guidance

arXiv 1904.01677 ↗First posted 2 Apr 2019cs.AI cs.LG cs.LOcited by 20

Not on the map. Why?

Abstract (arXiv)

We describe a very large improvement of existing hammer-style proof automation over large ITP libraries by combining learning and theorem proving. In particular, we have integrated state-of-the-art machine learners into the E automated theorem prover, and developed methods that allow learning and efficient internal guidance of E over the whole Mizar library. The resulting trained system improves the real-time performance of E on the Mizar library by 70% in a single-strategy setting.

Key facts. Cited by 20 papers in the map (data through 7 Oct 2026). First posted on arXiv 2 Apr 2019.

Builds on

No reference list yet.

Built on by

Cited by year

Citing papers per year: 2021: 8; 2022: 1; 2023: 3; 2024: 5; 2025: 3.

20 papers.

Sort:

By area:

  1. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  2. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  3. 2021Learning to Guide a Saturation-Based Theorem Provercited by 15
  4. 2021Proving Theorems using Incremental Learning and Hindsight Experience Replaycited by 13
  5. 2021Vampire With a Brain Is a Good ITP Hammercited by 10
  6. 2023Alien Codingcited by 9
  7. 2021The Role of Entropy in Guiding a Connection Provercited by 8
  8. 2021Fast and Slow Enigmas and Parental Guidancecited by 8
  9. 2022The Isabelle ENIGMAcited by 8
  10. 2021Learning Theorem Proving Componentscited by 7
  11. 2024Learning Guided Automated Reasoning: A Brief Surveycited by 7
  12. 2023MizAR 60 for Mizar 50cited by 6
8 more
  1. 2025Learning Conjecturing from Scratchcited by 3
  2. 2025Towards AI-assisted Neutrino Flavor Theory Designcited by 3
  3. 2024Application of AI to formal methods - an analysis of current trendscited by 2
  4. 2021Improving ENIGMA-Style Clause Selection While Learning From Historycited by 1
  5. 2024Solving Hard Mizar Problems with Instantiation and Strategy Inventioncited by 1
  6. 2023Translating SUMO-K to Higher-Order Set Theorycited by 0
  7. 2024Machine Learning for Quantifier Selection in cvc5cited by 0
  8. 2025Efficient Neural Clause-Selection Reinforcementcited by 0