# Solving Hard Mizar Problems with Instantiation and Strategy Invention

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 56 references that are in the map.
- First posted on arXiv 25 Jun 2024.

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

- [SMAC3: A Versatile Bayesian Optimization Package for Hyperparameter Optimization](https://mlsanity.com/paper/2109.09831/) (2021)
- [ParamILS: An Automatic Algorithm Configuration Framework](https://mlsanity.com/paper/1401.3492/) (2014)
- [ENIGMA: Efficient Learning-based Inference Guiding Machine](https://mlsanity.com/paper/1701.06532/) (2017)
- [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)
- [Vampire With a Brain Is a Good ITP Hammer](https://mlsanity.com/paper/2102.03529/) (2021)
- [Fast and Slow Enigmas and Parental Guidance](https://mlsanity.com/paper/2107.06750/) (2021)
- [The Isabelle ENIGMA](https://mlsanity.com/paper/2205.01981/) (2022)
- [MizAR 60 for Mizar 50](https://mlsanity.com/paper/2303.06686/) (2023)
- [BliStrTune: Hierarchical Invention of Theorem Proving Strategies](https://mlsanity.com/paper/1611.08733/) (2016)
- [Graph Sequence Learning for Premise Selection](https://mlsanity.com/paper/2303.15642/) (2023)
- [Lash 1.0 (System Description)](https://mlsanity.com/paper/2205.06640/) (2022)
- [Fair and Adventurous Enumeration of Quantifier Instantiations](https://mlsanity.com/paper/2105.13700/) (2021)
- [On Solving Quantified Bit-Vectors using Invertibility Conditions](https://mlsanity.com/paper/1804.05025/) (2018)
- [Bitwuzla at the SMT-COMP 2020](https://mlsanity.com/paper/2006.01621/) (2020)

## Built on by (most cited first, 1 of 1)

- [Machine Learning for Quantifier Selection in cvc5](https://mlsanity.com/paper/2408.14338/) (2024)

## Abstract (arXiv)

In this work, we prove over 3000 previously ATP-unproved Mizar/MPTP problems by using several ATP and AI methods, raising the number of ATP-solved Mizar problems from 75% to above 80%. First, we start to experiment with the cvc5 SMT solver which uses several instantiation-based heuristics that differ from the superposition-based systems, that were previously applied to Mizar,and add many new solutions. Then we use automated strategy invention to develop cvc5 strategies that largely improve cvc5's performance on the hard problems. In particular, the best invented strategy solves over 14% more problems than the best previously available cvc5 strategy. We also show that different clausification methods have a high impact on such instantiation-based methods, again producing many new solutions. In total, the methods solve 3021 (21.3%) of the 14163 previously unsolved hard Mizar problems. This is a new milestone over the Mizar large-theory benchmark and a large strengthening of the hammer methods for Mizar.