EasyChair Publications
Search
Paper Information
Paper:Cezary Kaliszyk and Josef Urban
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
Title:Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
Authors:Cezary Kaliszyk and Josef Urban
Keyphrases:automatic theorem provers, machine learning, large theories, strategy evolution, feature weighting, flyspeck, hol light, higher order logic
Paper:
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%.
Volume:Jasmin Christian Blanchette and Josef Urban (editors). PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Series:EPiC Series in Computing
Volume number:14
Pages:87-95
Editors:Jasmin Christian Blanchette and Josef Urban
Page views:15
Downloads:21
BibTeX entry:
@inproceedings{PxTP2013:Stronger_Automation_for_Flyspeck_by_Feature_Weighting_and_Strategy_Evolution,
  author    = {Cezary Kaliszyk and Josef Urban},
  title     = {Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution},
  booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EPiC Series in Computing},
  volume    = {14},
  pages     = {87-95},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}