MaLARea 0.6

J. Urban, J. Jakubuv, C. Kaliszyk, S. Schulz
Czech Technical University in Prague, University of Innsbruck, DHBW Stuttgart

Architecture

MaLARea 0.6 [Urb07, USPV08, KUV15] is a metasystem for ATP in large theories where symbol and formula names are used consistently. It uses several deductive systems (now E,SPASS,Vampire, Paradox, Mace), as well as complementary AI techniques like machine learning (the SNoW system) based on symbol-based similarity, model-based similarity, term-based similarity, and obviously previous successful proofs. The version for CASC 2017 will mainly use E prover with the BliStr(Tune) [Urb13, JU17] large-theory strategies, possibly also Prover9, Mace and Paradox. The premise selection methods will likely also use the distance-weighted k-nearest neighbor [KU13] and E's implementation of SInE.

Strategies

The basic strategy is to run ATPs on problems, then use the machine learner to learn axiom relevance for conjectures from solutions, and use the most relevant axioms for next ATP attempts. This is iterated, using different timelimits and axiom limits. Various features are used for learning, and the learning is complemented by other criteria like model-based reasoning, symbol and term-based similarity, etc.

Implementation

The metasystem is implemented in ca. 2500 lines of Perl. It uses many external programs - the above mentioned ATPs and machine learner, TPTP utilities, LADR utilities for work with models, and some standard Unix tools. MaLARea is available at 
    https://github.com/JUrban/MPTP2/tree/master/MaLARea
The metasystem's Perl code is released under GPL2.

Expected Competition Performance

Thanks to machine learning, MaLARea is strongest on batches of many related problems with many redundant axioms where some of the problems are easy to solve and can be used for learning the axiom relevance. MaLARea is not very good when all problems are too difficult (nothing to learn from), or the problems (are few and) have nothing in common. Some of its techniques (selection by symbol and term-based similarity, model-based reasoning) could however make it even there slightly stronger than standard ATPs. MaLARea has a very good performance on the MPTP Challenge, which is a predecessor of the LTB division, and on several previous LTB competitions.

References

Urb07
Urban J. (2007), MaLARea: a Metasystem for Automated Reasoning in Large Theories., In Sutcliffe G., Urban J., Schulz S., Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories (Bremen, Germany), CEUR Workshop Proceedings,.
USPV08
Urban J., Sutcliffe G., Pudlak P., Vyskocil J. (2007), MaLARea SG1: Machine Learner for Automated Reasoning with Semantic Guidance, In Baumgartner P., Armando A., Gilles D., Proceedings of the 4th International Joint Conference on Automated Reasoning (Sydney, Australia), Lecture Notes in Artificial Intelligence (To appear).
KUV15
Cezary Kaliszyk, Josef Urban and Jiri Vyskocil (2015), Machine Learner for Automated Reasoning 0.4 and 0.5,, PAAR 2014, 60-66
Urb13
Urban J. (2013), BliStr: The Blind Strategymaker., CoRR abs/1301.2683 (2013)
JU17
Jan Jakubuv, Josef Urban (2017), BliStrTune: hierarchical invention of theorem proving strategies, CPP 2017: 43-52
KU13
Kaliszyk C., Urban J. (2013) Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution, In Blanchette J.C., Urban J., Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving (Lake Placid, USA), EasyChair Proceedings in Computing (To appear).