Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution

Cezary Kaliszyk and Josef Urban

Proceedings of the 3rd International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), EasyChair Proceedings in Computing 14, pp. 87 – 95, 2013.


Two complementary AI methods are used to improve the strength of the AI/ATP service for proving conjectures over the HOL Light and Flyspeck corpora. First, several schemes for frequency-based feature weighting are explored in combination with distance-weighted k-nearest-neighbor classifier. This results in 16% improvement (39.0% to 45.5% Flyspeck problems solved) of the overall strength of the service when using 14 CPUs and 30 seconds. The best premise-selection/ATP combination is improved from 24.2% to 31.4%, i.e. by 30%. A smaller improvement is obtained by evolving targetted E prover strategies on two particular premise selections, using the Blind Strategymaker (BliStr) system. This raises the performance of the best AI/ATP method from 31.4% to 34.9%, i.e. by 11%, and raises the current 14-CPU power of the service to 46.9%.




author = "Cezary Kaliszyk and Josef Urban",
title = "Stronger Automation for {F}lyspeck by Feature Weighting and Strategy Evolution",
booktitle = "Proceedings of the 3rd International Workshop on Proof
Exchange for Theorem Proving",
series = "EasyChair Proceedings in Computing",
volume = 14,
pages = "87--95",
year = 2013
Nach oben scrollen