Hammering Mizar by Learning Clause Guidance

TL;DR

This paper presents a significant enhancement in proof automation for large ITP libraries by integrating machine learning into the E theorem prover, achieving a 70% performance boost on the Mizar library.

Contribution

It introduces a novel method of combining machine learning with theorem proving to improve proof automation efficiency over large libraries.

Findings

70% performance improvement in real-time E prover on Mizar library

Successful integration of state-of-the-art machine learning into theorem proving

Enhanced internal guidance of E for large proof libraries

Abstract

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.