MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers

MaLeS is a framework that develops strategies for automated theorem provers (ATPs) and learns suitable schedules of strategies for specific problems. The framework can be used in a push-button way to develop such strategies and schedules for an arbitrary ATP. This paper describes the tool and the methods used in it, and evaluates its performance for three automated theorem provers: E, LEO-II and Satallax. It is shown, that the MaLeS version performs at least comparably to manual tuning. On average, MaLeS solves 8.67% more problems than the default setting.