Elamur Research⌕
☰
home / papers / 2018 / PaMpeR: Proof Method Recommendation System for Isabelle/HOL

PaMpeR: Proof Method Recommendation System for Isabelle/HOL

Paper · 2018 · Yutaka Nagashima and Yilun He

Summary

Isabelle/HOL offers a large toolbox of proof methods, with 159 in its standard library alone. Picking the right one for a given proof state takes experience that newcomers usually lack. PaMpeR tackles this by mining proofs that experts have already written. In a preparation phase, a feature extractor works through proof states taken from big proof collections, the Archive of Formal Proofs (AFP) being a prime example. It encodes each state as a boolean vector produced by 108 hand-written assertions in Standard ML. These assertions examine the goal, the chained facts and the background context, for example inferring how a constant was defined from automatically derived lemma names. The system then trains one regression tree per proof method, estimating how likely that method is to be applied to states with particular features. At proof time, users can request recommendations, explanations and rankings directly in Isabelle/jEdit. The evaluation shows that PaMpeR reproduces expert choices well, especially for special-purpose methods. This makes it a practical way to transfer expert know-how to new users.

Key points

  • Each proof state is abstracted into an array of booleans by 108 manually designed assertions. The mapping is many-to-one, so each vector stands for a group of similar proof states.
  • The training data comes from existing proof corpora, mainly the AFP. The data is split into one database per proof method, and a multi-output regression algorithm builds a separate regression tree for each method.
  • Assertions avoid depending on user-defined constants. Instead they rely on meta-information, such as whether a lemma like sep.elims exists, which signals a definition made with fun or function.
  • Three commands are provided:
    • which_method suggests methods.
    • why_method explains a particular suggestion.
    • rank_method shows where a given method ranks.
  • Recommendations are strongest for specialised methods (e.g., eventually_elim, intro_classes). The evaluation also covers user-defined methods such as refine_vcg, autoref, sepref and sep_auto. The implementation is available on GitHub.

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

🎓The University of SydneySydney · Australia52 works · 68,450 citations🎓Universität InnsbruckInnsbruck · Austria23 works · 1,475 citations🎓Czech Technical University in PraguePrague · Czechia16 works · 930 citations

 Fields, topics and concepts

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

Cite

Cite as Yutaka Nagashima and Yilun He. 2018. PaMpeR: Proof Method Recommendation System for Isabelle/HOL. arXiv:1806.07239.

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

@misc{nagashima2018pamper,
  title = {{PaMpeR: Proof Method Recommendation System for Isabelle/HOL}},
  author = {Yutaka Nagashima and Yilun He},
  year = {2018},
  doi = {10.48550/arxiv.1806.07239},
  eprint = {1806.07239},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1806.07239}
}

References

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

  1. Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel, Isabelle/HOL - A proof assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283, Springer, 2002, 3-540-43376-7 find
  2. Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood, seL4: formal verification of an operating-system kernel, Commu… find
  3. Xavier Leroy, Formal verification of a realistic compiler, Commun. ACM, vol. 52-7, pp. 107-115, 2009 find
  4. Ramana Kumar and Magnus O. Myreen and Michael Norrish and Scott Owens, CakeML: a verified implementation of ML, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, pp. 179-192 find
  5. Thomas C. Hales and Mark Adams and Gertrud Bauer and Dat Tat Dang and John Harrison and Truong Le Hoang and Cezary Kaliszyk and Victor Magron and Sean McLaughlin and Thang Tat Nguyen and Truong Quang Nguyen and Tobias Nipkow and Steven Obua and Joseph Pleso and Jason M. Rute and Alexey Solovyev and… — A formal proof of the Kepler conjecture
  6. Georges Gonthier, The four colour theorem: engineering of a formal proof, Computer Mathematics, 8th Asian Symposium, ASCM 2007, Singapore, December 15-17, 2007. Revised and Invited Papers, pp. 333 find
  7. Ren Thiemann and Christian Sternagel Certification of termination proofs using CeTA In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs ’09), Lecture Notes in Computer Science 5674, pp. 452468, 2009, Springer-Verlag find
  8. Lawrence C. Paulson, A mechanised proof of gödel’s incompleteness theorems using Nominal Isabelle, J. Autom. Reasoning, vol. 55-1, pp. 1-37, 2015, https://doi.org/10.1007/s10817-015-9322-8 — [doi:10.1007/s10817-015-9322-8](https://doi.org/10.1007/s10817-015-9322-8) ↗
  9. Pedregosa, F., Varoquaux, G., Gramfort, A., Michel, V., Thirion, B., Grisel, O., Blondel, M., Prettenhofer, P., Weiss, R., Dubourg, V. VanderPlas, J., Passos, A., Cournapeau, D., Brucher, M., Perrot, M., Duchesnay, E. Scikit-learn: Machine Learning in Python, Journal of Machine Learning Research, vo… find
  10. James, G., Witten, D., Hastie, T., Tibshirani R. An Introduction to Statistical Learning with Applications in R find
  11. Yutaka Nagashima and Ramana Kumar, A proof strategy language and proof script generation for Isabelle/HOL, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, pp. 528–545 find
  12. Geoffrey Irving and Christian Szegedy and Alexander A. Alemi and Niklas Eén and François Chollet and Josef Urban, Deep-Math - deep sequence models for premise selection, Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December… find
  13. Sarah M. Loos and Geoffrey Irving and Christian Szegedy and Cezary Kaliszyk, Deep network guided proof search, LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, pp. 85-105, http://www.easychair.org/publications/pa… ↗
  14. Ekaterina Komendantskaya and Jónathan Heras and Gudmund Grov, Machine learning in proof general: interfacing interfaces, Proceedings 10th International Workshop On User Interfaces for Theorem Provers, UITP 2012, Bremen, Germany, July 11th, 2012. pp. 15-41 find
  15. Gerwin Klein, Tobias Nipkow, Larry Paulson, Rene Thiemann, Archive of Formal Proofs, https://www.isa-afp.org/ ↗
  16. Thibault Gauthier and Cezary Kaliszyk and Josef Urban, TacticToe: learning to reason with HOL4 tactics, LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, pp. 125-143 find
  17. Jia Meng and Lawrence C. Paulson, Lightweight relevance filtering for machine-generated resolution problems, J. Applied Logic, vol. 7-1, pp. 41-57 2009 find
  18. Jasmin Christian Blanchette and David Greenaway and Cezary Kaliszyk and Daniel Kühlwein and Josef Urban, A learning-based fact selector for Isabelle/HOL, J. Autom. Reasoning, vol. 57-3, pp. 219-244 2016 find
  19. Markus Wenzel, Isar - a generic interpretative approach to readable formal proof documents, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99, Nice, France, September, 1999, Proceedings, pp. 167–184 find
  20. Haibo He and Edwardo A. Garcia, Learning from imbalanced data, IEEE Trans. Knowl. Data Eng., vol. 21. pp. 1263-1284. 2009, find
  21. https://github.com/data61/PSL/releases/tag/v0.1.1 To use PaMpeR, one first needs to install Isabelle/HOL, which is distributed at https://isabelle. in.tum.de/. PGT/Example.thy provides the example presented in this paper. ↗
  22. Breiman, Leo; Friedman, J. H.; Olshen, R. A.; Stone, C. J., 1984, Classification and regression trees. Monterey, CA: Wadsworth & Brooks/Cole Advanced Books & Software. find
  23. Jasmin Christian Blanchette and Maximilian P. L. Haslbeck and Daniel Matichuk and Tobias Nipkow, Mining the Archive of Formal Proofs, Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings, pp. 3 -17 find
  24. Daniel Matichuk and Toby C. Murray and June Andronick and D. Ross Jeffery and Gerwin Klein and Mark Staples, Empirical study towards a leading indicator for cost of formal software verification, 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16-24, 20… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/nagashima-2018-pamper-proof-method-recommendation-system/