Hammering Mizar by Learning Clause Guidance
This work addresses efficiency bottlenecks in automated theorem proving for formal mathematics, representing a strong incremental improvement.
The authors tackled the problem of automating theorem proving over large interactive theorem proving libraries by integrating machine learning into the E automated theorem prover, resulting in a 70% improvement in real-time performance on the Mizar library.
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.