mlsanityData to 7 Oct 2026

Vampire With a Brain Is a Good ITP Hammer

arXiv 2102.03529 ↗First posted 6 Feb 2021cs.AIcited by 10

Not on the map. Why?

Abstract (arXiv)

Vampire has been for a long time the strongest first-order automatic theorem prover, widely used for hammer-style proof automation in ITPs such as Mizar, Isabelle, HOL, and Coq. In this work, we considerably improve the performance of Vampire in hammering over the full Mizar library by enhancing its saturation procedure with efficient neural guidance. In particular, we employ a recently proposed recursive neural network classifying the generated clauses based only on their derivation history. Compared to previous neural methods based on considering the logical content of the clauses, our architecture makes evaluating a single clause much less time consuming. The resulting system shows good learning capability and improves on the state-of-the-art performance on the Mizar library, while proving many theorems that the related ENIGMA system could not prove in a similar hammering evaluation.

Key facts. Cited by 10 papers in the map (data through 7 Oct 2026). Builds on 16 of its 46 references that are in the map. First posted on arXiv 6 Feb 2021.

Builds on

16 of 46 references.

References · 16

  1. 2017Attention Is All You Needcited by 59,932
  2. 2019PyTorch: An Imperative Style, High-Performance Deep Learning Librarycited by 20,160
  3. 2015Cyclical Learning Rates for Training Neural Networkscited by 627
  4. 2017Super-Convergence: Very Fast Training of Neural Networks Using Large Learning Ratescited by 196
  5. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 80
  6. 2017Deep Network Guided Proof Searchcited by 47
  7. 2017Premise Selection for Theorem Proving by Deep Graph Embeddingcited by 44
  8. 2017ENIGMA: Efficient Learning-based Inference Guiding Machinecited by 26
  9. 2020ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)cited by 26
  10. 2019ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for Ecited by 24
  11. 2013MizAR 40 for Mizar 40cited by 23
  12. 2019Hammering Mizar by Learning Clause Guidancecited by 20
4 more
  1. 2020Stateful Premise Selection by Recurrent Neural Networkscited by 11
  2. 2013HOL(y)Hammer: Online ATP Service for HOL Lightcited by 8
  3. 2016Monte Carlo Tableau Proof Searchcited by 1
  4. 2020Layered Clause Selection for Theory Reasoningcited by 1

Built on by

Cited by year

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

10 papers.

  1. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  2. 2024Learning Guided Automated Reasoning: A Brief Surveycited by 7
  3. 2023MizAR 60 for Mizar 50cited by 6
  4. 2023An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representationscited by 4
  5. 2025Learning Conjecturing from Scratchcited by 3
  6. 2024Application of AI to formal methods - an analysis of current trendscited by 2
  7. 2021Improving ENIGMA-Style Clause Selection While Learning From Historycited by 1
  8. 2024Solving Hard Mizar Problems with Instantiation and Strategy Inventioncited by 1
  9. 2024Machine Learning for Quantifier Selection in cvc5cited by 0
  10. 2025Efficient Neural Clause-Selection Reinforcementcited by 0