BliStr: The Blind Strategymaker

TL;DR

BliStr is an automated system that iteratively develops and refines strategies for the E theorem prover by leveraging local search and problem similarity, leading to significant performance improvements in automated theorem proving competitions.

Contribution

It introduces a novel iterative strategy development method that combines local search with global evaluation to enhance theorem prover performance.

Findings

Significant improvement in E prover strategies for CASC@Turing 2012.

Enhanced performance on Flyspeck problems.

Effective automatic strategy evolution method.

Abstract

BliStr is a system that automatically develops strategies for E prover on a large set of problems. The main idea is to interleave (i) iterated low-timelimit local search for new strategies on small sets of similar easy problems with (ii) higher-timelimit evaluation of the new strategies on all problems. The accumulated results of the global higher-timelimit runs are used to define and evolve the notion of "similar easy problems", and to control the selection of the next strategy to be improved. The technique was used to significantly strengthen the set of E strategies used by the MaLARea, PS-E, E-MaLeS, and E systems in the CASC@Turing 2012 competition, particularly in the Mizar division. Similar improvement was obtained on the problems created from the Flyspeck corpus.