Abstract

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%.

BibTeX

inproceedings{CKJU-PxTP13,
  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
}