MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers

TL;DR

MaLeS is an automatic framework that optimizes automated theorem provers' strategies, significantly improving their problem-solving performance across multiple provers and problem sets.

Contribution

Introduces MaLeS, a novel framework for automatic strategy tuning and scheduling in automated theorem proving, with demonstrated performance improvements.

Findings

MaLeS-tuned provers solve 8.67% more problems on average.

Effective on three different theorem provers: E, LEO-II, and Satallax.

Performance gains shown on TPTP library subset.

Abstract

MaLeS is an automatic tuning framework for automated theorem provers. It provides solutions for both the strategy finding as well as the strategy scheduling problem. This paper describes the tool and the methods used in it, and evaluates its performance on three automated theorem provers: E, LEO-II and Satallax. An evaluation on a subset of the TPTP library problems shows that on average a MaLeS-tuned prover solves 8.67% more problems than the prover with its default settings.