Elamur Research⌕
☰
home / papers / 2019 / Property Invariant Embedding for Automated Reasoning

Property Invariant Embedding for Automated Reasoning

Paper · 2019 · Miroslav Olšák, Cezary Kaliszyk and Josef Urban

Summary

Machine-learned guidance for theorem provers depends on turning formulas into vectors. Most existing encoders, including the graph-based FormulaNet, learn a separate representation for each symbol name. They therefore cope poorly with the many fresh symbols that Skolemization and definitional clausification produce, and with libraries where names are used inconsistently. The authors propose a new encoding. A set of first-order clauses becomes a hypergraph with nodes for clauses, shared subterms/literals and symbols, where symbols carry no label information. A purpose-built graph neural network then passes messages over this structure. Its output stays the same when symbols are renamed, when a predicate is swapped for its negation, and when clauses or literals are reordered. The network was tested in three settings: guiding the leanCoP connection-tableau prover, premise selection, and a new task of guessing symbol names from structure. It beat earlier characterizations in all of them. This matters because representations that ignore names let learned knowledge carry over to unseen symbols and across theories.

Key points

  • Function and predicate symbols are hypergraph nodes connected to their arguments through ordered argument pairs. Predicate nodes start as zero vectors, and a max+min reduction keeps the model symmetric under negation.
  • In real clausal datasets, roughly 40% of symbols are problem-specific ones introduced during clausification.
  • Guiding rlCoP/leanCoP with the network gave a 45.6% gain over the earlier XGBoost-guided rlCoP on the test set in the first learning iteration.
  • The model outperformed previous methods on premise-selection data. On the new symbol guessing task it named 65% of symbols correctly.
  • Aligning similar concepts produced new conjectures on Mizar examples, such as moving from subtraction to division of complex numbers (MEMBER_1:77 → MEMBER_1:130) and pairing the FinJoin and FinMeet lattice theorems in LATTICE4.

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

🎓Universität InnsbruckInnsbruck · Austria23 works · 1,475 citations🎓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 Miroslav Olšák, Cezary Kaliszyk and Josef Urban. 2019. Property Invariant Embedding for Automated Reasoning. arXiv:1911.12073 (ECAI 2020 - 24th European Conference on Artificial Intelligence).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.3233/faia200244 · arXiv 1911.12073

@misc{olsak2019property,
  title = {{Property Invariant Embedding for Automated Reasoning}},
  author = {Miroslav Olšák, Cezary Kaliszyk and Josef Urban},
  year = {2019},
  doi = {10.3233/faia200244},
  eprint = {1911.12073},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.3233/faia200244}
}

References

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

  1. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban, ‘Premise selection for mathematics by corpus analysis and kernel methods’, J. Autom. Reasoning, 52(2), 191–213, (2014).
  2. Alexander A. Alemi, François Chollet, Niklas Eén, Geoffrey Irving, Christian Szegedy, and Josef Urban, ‘DeepMath - deep sequence models for premise selection’, in Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2…
  3. Miltiadis Allamanis, Pankajan Chanthirasegaran, Pushmeet Kohli, and Charles A. Sutton, ‘Learning continuous semantic representations of symbolic expressions’, in Proceedings of the 34th International Conference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6-11 August 2017, eds., Doina Pre…
  4. Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban, ‘A learning-based fact selector for Isabelle/HOL’, J. Autom. Reasoning, 57(3), 219–244, (2016). find
  5. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban, ‘Hammering towards QED’, J. Formalized Reasoning, 9(1), 101–148, (2016).
  6. Karel Chvalovský, Jan Jakubuv, Martin Suda, and Josef Urban, ‘ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E’, in Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, ed., Pascal Fontaine, vo…
  7. Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, eds. Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science. Springer, 2015. find
  8. Jrg Denzinger, Matthias Fuchs, Christoph Goller, and Stephan Schulz, ‘Learning from Previous Proof Experience’, Technical Report AR99-4, Institut für Informatik, Technische Universität München, (1999). find
  9. David Duvenaud, Dougal Maclaurin, Jorge Aguilera-Iparraguirre, Rafael Gómez-Bombarelli, Timothy Hirzel, Alán Aspuru-Guzik, and Ryan P. Adams, ‘Convolutional networks on graphs for learning molecular fingerprints’, in Advances in Neural Information Processing Systems 28: Annual Conference on Neural…
  10. Wolfgang Ertel, Johann Schumann, and Christian B. Suttner, ‘Learning heuristics for a theorem prover using back propagation’, in 5. Österreichische Artificial Intelligence-Tagung, Igls, Tirol, 28. bis 30. September 1989, Proceedings, eds., Johannes Retti and Karl Leidlmair, volume 208 of Informatik… find
  11. Michael Färber, Cezary Kaliszyk, and Josef Urban, ‘Monte Carlo tableau proof search’, in Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, ed., Leonardo de Moura, volume 10395 of Lecture Notes in Computer Scienc… find
  12. Thibault Gauthier and Cezary Kaliszyk, ‘Premise selection and external provers for HOL4’, in Certified Programs and Proofs (CPP’15), LNCS. Springer, (2015). http://dx.doi.org/10.1145/2676724.2693173. — [doi:10.1145/2676724.2693173](https://doi.org/10.1145/2676724.2693173) ↗
  13. Thibault Gauthier and Cezary Kaliszyk, ‘Sharing HOL4 and HOL light proof knowledge’, In Davis et al. [7], pp. 372–386. find
  14. Thibault Gauthier and Cezary Kaliszyk, ‘Aligning concepts across proof assistant libraries’, J. Symb. Comput., 90, 89–123, (2019). find
  15. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban, ‘Initial experiments with statistical conjecturing over large formal corpora’, in Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-loca… find
  16. Christoph Goller and Andreas Küchler, ‘Learning task-dependent distributed representations by backpropagation through structure’, in Proceedings of International Conference on Neural Networks (ICNN’96), Washington, DC, USA, June 3-6, 1996, pp. 347–352. IEEE, (1996). find
  17. Georg Gottlob, Geoff Sutcliffe, and Andrei Voronkov, eds. Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015, volume 36 of EPiC Series in Computing. EasyChair, 2015. find
  18. Jan Jakubův and Josef Urban, ‘Hierarchical invention of theorem proving strategies’, AI Commun., 31(3), 237–250, (2018). find
  19. Jan Jakubuv and Josef Urban, ‘ENIGMA: efficient learning-based inference guiding machine’, in Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings, eds., Herman Geuvers, Matthew England, Osman Hasan, Florian Rabe, and Olaf Teschke,…
  20. Jan Jakubuv and Josef Urban, ‘Hammering Mizar by learning clause guidance’, in 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, eds., John Harrison, John O’Leary, and Andrew Tolmach, volume 141 of LIPIcs, pp. 34:1–34:8. Schloss Dagstuhl… find
  21. Cezary Kaliszyk, François Chollet, and Christian Szegedy, ‘HolStep: A machine learning dataset for higher-order logic theorem proving’, in 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. OpenReview.net, (2017).
  22. Cezary Kaliszyk and Josef Urban, ‘Learning-assisted automated reasoning with Flyspeck’, J. Autom. Reasoning, 53(2), 173–213, (2014).
  23. Cezary Kaliszyk and Josef Urban, ‘FEMaLeCoP: Fairly efficient machine learning connection prover’, In Davis et al. [7], pp. 88–96. find
  24. Cezary Kaliszyk and Josef Urban, ‘HOL(y)Hammer: Online ATP service for HOL Light’, Mathematics in Computer Science, 9(1), 5–22, (2015).
  25. Cezary Kaliszyk and Josef Urban, ‘MizAR 40 for Mizar 40’, J. Autom. Reasoning, 55(3), 245–256, (2015).
  26. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák, ‘Reinforcement learning of theorem proving’, in Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3-8 December 2018, Montréal, Canada., pp. 8836…
  27. Cezary Kaliszyk, Josef Urban, and Jirı́ Vyskocil, ‘Efficient semantic features for automated reasoning over large theories’, in IJCAI, pp. 3084–3090. AAAI Press, (2015). find
  28. Kriste Krstovski and David M. Blei, ‘Equation embeddings’, CoRR, abs/1803.09123, (2018). find
  29. Andrzej Stanislaw Kucik and Konstantin Korovin, ‘Premise selection with neural networks and distributed representation of features’, CoRR, abs/1807.10268, (2018). — [arXiv:1807.10268](https://arxiv.org/abs/1807.10268) find
  30. Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes, ‘Overview and evaluation of premise selection techniques for large theory mathematics’, in IJCAR, eds., Bernhard Gramlich, Dale Miller, and Uli Sattler, volume 7364 of LNCS, pp. 378– 392. Springer, (2012). find
  31. Reinhold Letz, Klaus Mayr, and Christoph Goller, ‘Controlled integration of the cut rule into connection tableau calculi’, Journal of Automated Reasoning, 13, 297–337, (1994). find
  32. Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk, ‘Deep network guided proof search’, in LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, eds., Thomas Eiter and David Sands, volume 46 of EPiC Series in Computing, pp. 85–105. E…
  33. Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk, ‘Deep network guided proof search’, in LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, eds., Thomas Eiter and David Sands, volume 46 of EPiC…
  34. Jia Meng and Lawrence C. Paulson, ‘Translating higher-order clauses to first-order clauses’, J. Autom. Reasoning, 40(1), 35–60, (2008). find
  35. Jens Otten, ‘Restricting backtracking in connection calculi’, AI Commun., 23(2-3), 159–182, (2010). find
  36. Jens Otten and Wolfgang Bibel, ‘leanCoP: lean connection-based theorem proving’, J. Symb. Comput., 36(1-2), 139–161, (2003). find
  37. Ross A. Overbeek, ‘A new class of automated theorem-proving algorithms’, J. ACM, 21(2), 191–200, (April 1974). find
  38. Handbook of Automated Reasoning (in 2 volumes), eds., John Alan Robinson and Andrei Voronkov, Elsevier and MIT Press, 2001. find
  39. Simon Schäfer and Stephan Schulz, ‘Breeding theorem proving heuristics with genetic algorithms’, In Gottlob et al. [17], pp. 263–274. find
  40. Stephan Schulz, Learning search control knowledge for equational deduction, volume 230 of DISKI, Infix Akademische Verlagsgesellschaft, 2000. find
  41. Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill, ‘Learning a SAT solver from single-bit supervision’, in 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, (2019).
  42. David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al., ‘Mastering the game of go without human knowledge’, Nature, 550(7676), 354, (2017). find
  43. Geoff Sutcliffe, ‘The TPTP world - infrastructure for automated reasoning’, in LPAR (Dakar), eds., Edmund M. Clarke and Andrei Voronkov, volume 6355 of LNCS, pp. 1–12. Springer, (2010). find
  44. Josef Urban, ‘MPTP - Motivation, Implementation, First Experiments’, J. Autom. Reasoning, 33(3-4), 319–339, (2004). find
  45. Josef Urban, ‘MPTP 0.2: Design, implementation, and initial experiments’, J. Autom. Reasoning, 37(1-2), 21–43, (2006). find
  46. Josef Urban, ‘BliStr: The Blind Strategymaker’, In Gottlob et al. [17], pp. 312–319. find
  47. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiřı́ Vyskočil, ‘MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance’, in IJCAR, eds., Alessandro Armando, Peter Baumgartner, and Gilles Dowek, volume 5195 of LNCS, pp. 441–456. Springer, (2008). find
  48. Josef Urban, Jiřı́ Vyskočil, and Petr Štěpánek, ‘MaLeCoP: Machine learning connection prover’, in TABLEAUX, eds., Kai Brünnler and George Metcalfe, volume 6793 of LNCS, pp. 263–277. Springer, (2011). find
  49. Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng, ‘Premise selection for theorem proving by deep graph embedding’, in Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, 4-9 December 2017, Long Beach, CA, USA, eds., Isabelle Guyon, U…

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/olsak-2019-property-invariant-embedding-automated-reasoning/