Elamur Research⌕
☰
home / papers / 2017 / ENIGMA: Efficient Learning-based Inference Guiding Machine

ENIGMA: Efficient Learning-based Inference Guiding Machine

Paper · 2017 · Jan Jakubův and Josef Urban

Summary

Saturation-based provers such as E must constantly decide which generated clause to process next (given clause selection). Their hand-designed heuristics for this choice fall well short of human mathematical intuition. ENIGMA learns this choice from earlier proof searches. In each successful run, selected clauses that appear in the final proof are labelled positive, and the remaining selected clauses negative. Each clause is encoded as a count vector of length-3 term walks through its literal trees, with variables and Skolem symbols replaced by placeholder symbols. A linear L2-SVM from LIBLINEAR is trained on these vectors. Its prediction, plus a clause-length term scaled by γ, forms a new clause weight function inside E that can run alone or alongside an existing strategy. Training takes seconds, and evaluation costs roughly ten microseconds per clause. On the 200 CASC 2016 AIM competition problems, ENIGMA strategies raised the count from 22 (baseline strategy S0) to 52, and to 57 after boosting positive examples. Vampire solved 47. The authors present this as the first practical learning-based internal guidance for a state-of-the-art ATP.

Key points

  • Pipeline: proof-derived positive/negative clauses → term-walk features → LIBLINEAR L2-SVM classifier → weight function in the E prover.
  • Classifier M1 was trained on proofs of 337 solved training problems (6821 positive, 219,012 negative examples) in about 7 s. It reached 97.6% accuracy on the training data.
  • With a 180 s limit, the best single strategy (S0 combined with the classifier, frequency 30, γ = 0.2) solved 41 of 200 AIM problems, compared with 22 for S0 alone. Three strategies together solved 52, versus 47 for Vampire given 3×180 s.
  • Repeating positive examples ten times produced M2. Its overall accuracy fell (93% vs. 98%), but accuracy on positives rose from 12.5% to 81.8%. M2 added 5 more problems, for 57 in total.
  • In total, ENIGMA proved 16 problems that Vampire did not solve. Proposed future work includes learning during the proof search and richer features and learners.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Czech Technical University in PraguePrague · Czechia16 works · 930 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Jan Jakubův and Josef Urban. 2017. ENIGMA: Efficient Learning-based Inference Guiding Machine. arXiv:1701.06532.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.1701.06532 · arXiv 1701.06532

@misc{jakubuv2017enigma,
  title = {{ENIGMA: Efficient Learning-based Inference Guiding Machine}},
  author = {Jan Jakubův and Josef Urban},
  year = {2017},
  doi = {10.48550/arxiv.1701.06532},
  eprint = {1701.06532},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1701.06532}
}

References

24 references, 3 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, and J. Urban. A learning-based fact selector for Isabelle/HOL. J. Autom. Reasoning, 57(3):219–244, 2016. find
  2. J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban. Hammering towards QED. J. Formalized Reasoning, 9(1):101–148, 2016.
  3. B. E. Boser, I. Guyon, and V. Vapnik. A training algorithm for optimal margin classifiers. In COLT, pages 144–152. ACM, 1992. find
  4. R. Fan, K. Chang, C. Hsieh, X. Wang, and C. Lin. LIBLINEAR: A library for large linear classification. Journal of Machine Learning Research, 9:1871–1874, 2008. find
  5. M. Färber, C. Kaliszyk, and J. Urban. Monte Carlo connection prover. CoRR, abs/1611.05990, 2016. 5 In an initial experiment, a simple nearest-neighbor selection of training problems for the learning further decreases the solving times and proves one more AIM problem unsolved by Prover9. — [arXiv:1611.05990](https://arxiv.org/abs/1611.05990) find
  6. G. Gottlob, G. Sutcliffe, and A. Voronkov, editors. Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015, volume 36 of EPiC Series in Computing. EasyChair, 2015. find
  7. T. Gransden, N. Walkinshaw, and R. Raman. SEPIA: search for proofs using inferred automata. In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 246–255, 2015. find
  8. C. Hsieh, K. Chang, C. Lin, S. S. Keerthi, and S. Sundararajan. A dual coordinate descent method for large-scale linear SVM. In ICML, volume 307 of ACM International Conference Proceeding Series, pages 408–415. ACM, 2008. find
  9. J. Jakubuv and J. Urban. BliStrTune: hierarchical invention of theorem proving strategies. In Y. Bertot and V. Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pages 43–52. ACM, 2017. find
  10. C. Kaliszyk and J. Urban. Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning, 53(2):173–213, 2014.
  11. C. Kaliszyk and J. Urban. FEMaLeCoP: Fairly efficient machine learning connection prover. In M. Davis, A. Fehnker, A. McIver, and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proce… find
  12. C. Kaliszyk and J. Urban. MizAR 40 for Mizar 40. J. Autom. Reasoning, 55(3):245–256, 2015.
  13. C. Kaliszyk, J. Urban, and J. Vyskočil. Machine learner for automated reasoning 0.4 and 0.5. CoRR, abs/1402.2359, 2014. Accepted to PAAR’14. — [arXiv:1402.2359](https://arxiv.org/abs/1402.2359) find
  14. C. Kaliszyk, J. Urban, and J. Vyskočil. Efficient semantic features for automated reasoning over large theories. In Q. Yang and M. Wooldridge, editors, IJCAI’15, pages 3084–3090. AAAI Press, 2015. find
  15. L. Kovács and A. Voronkov. First-order theorem proving and Vampire. In N. Sharygina and H. Veith, editors, CAV, volume 8044 of LNCS, pages 1–35. Springer, 2013. find
  16. D. Kühlwein and J. Urban. MaLeS: A framework for automatic tuning of automated theorem provers. J. Autom. Reasoning, 55(2):91–116, 2015. find
  17. C. Lin, R. C. Weng, and S. S. Keerthi. Trust region newton method for logistic regression. Journal of Machine Learning Research, 9:627–650, 2008. find
  18. J. Otten and W. Bibel. leanCoP: lean connection-based theorem proving. J. Symb. Comput., 36(1-2):139–161, 2003. find
  19. S. Schäfer and S. Schulz. Breeding theorem proving heuristics with genetic algorithms. In Gottlob et al. [6], pages 263–274. find
  20. S. Schulz. E - A Brainiac Theorem Prover. AI Commun., 15(2-3):111–126, 2002. find
  21. G. Sutcliffe. The 8th IJCAR automated theorem proving system competition - CASC-J8. AI Commun., 29(5):607–619, 2016. find
  22. J. Urban. BliStr: The Blind Strategymaker. In Gottlob et al. [6], pages 312–319. find
  23. J. Urban, G. Sutcliffe, P. Pudlák, and J. Vyskočil. MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In A. Armando, P. Baumgartner, and G. Dowek, editors, IJCAR, volume 5195 of LNCS, pages 441–456. Springer, 2008. find
  24. J. Urban, J. Vyskočil, and P. Štěpánek. MaLeCoP: Machine learning connection prover. In K. Brünnler and G. Metcalfe, editors, TABLEAUX, volume 6793 of LNCS, pages 263–277. Springer, 2011. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/jakubuv-2017-enigma-efficient-learning-based-inference/