Solving Hard Mizar Problems with Instantiation and Strategy Invention

TL;DR

This paper enhances automated theorem proving for Mizar problems by integrating instantiation heuristics, strategy invention, and clausification techniques, solving over 3000 previously unproved problems and significantly improving success rates.

Contribution

It introduces novel instantiation heuristics and automated strategy invention for cvc5, leading to a substantial increase in solved Mizar problems and advancing the state-of-the-art in large-theory theorem proving.

Findings

Solved over 3000 previously unproved Mizar problems.

Improved cvc5 performance with new strategies, solving 14 ext% more problems.

High impact of clausification methods on problem-solving success.

Abstract

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.