---
title: "PaMpeR: Proof Method Recommendation System for Isabelle/HOL"
description: "Isabelle/HOL offers a large toolbox of proof methods, with 159 in its standard library alone. 24 references, cited by 5 papers here."
authors: ["Yutaka Nagashima", "Yilun He"]
year: 2018
venue: "arXiv:1806.07239"
source: "https://arxiv.org/abs/1806.07239"
doi: "10.48550/arxiv.1806.07239"
arxiv: "1806.07239"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/nagashima-2018-pamper-proof-method-recommendation-system/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/nagashima-2018-pamper-proof-method-recommendation-system/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2018](https://md.research.elamur.ai/free/en/papers/2018/page/6/) / PaMpeR: Proof Method Recommendation System for Isabelle/HOL

# PaMpeR: Proof Method Recommendation System for Isabelle/HOL

**Authors:** Yutaka Nagashima and Yilun He · **Year:** 2018 · **Venue:** arXiv:1806.07239 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/1806.07239) · [PDF](https://arxiv.org/pdf/1806.07239v1) · [DOI 10.48550/arxiv.1806.07239](https://doi.org/10.48550/arxiv.1806.07239) · [arXiv 1806.07239](https://arxiv.org/abs/1806.07239) · [OpenAlex](https://openalex.org/W2809147512)

**Citations:** 24 citations (OpenAlex, 2026-10-14) · [5](https://md.research.elamur.ai/free/en/papers/nagashima-2018-pamper-proof-method-recommendation-system/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## 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 Sydney](https://md.research.elamur.ai/free/en/universities/the-university-of-sydney/) — University, Sydney, Australia · 52 works · 68,450 citations
- [Universität Innsbruck](https://md.research.elamur.ai/free/en/universities/universitat-innsbruck/) — University, Innsbruck, Austria · 23 works · 1,475 citations
- [Czech Technical University in Prague](https://md.research.elamur.ai/free/en/universities/czech-technical-university-in-prague/) — University, Prague, Czechia · 16 works · 930 citations

📚 Shelves (4): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🗄️ Information Systems](https://md.research.elamur.ai/free/en/shelves/computer-science/information-systems/) · 1,888 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-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.

```bibtex
@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}
}
```

- [← previous Normalizing Early English Letters to Present-day English Spelling](https://md.research.elamur.ai/free/en/papers/hamalainen-2018-normalizing-early-english-letters-present/)
- [next → Primary and secondary discourse connectives: definitions and lexicons](https://md.research.elamur.ai/free/en/papers/danlos-2018-primary-secondary-discourse-connectives-definitions/)
- [↑ back to papers of 2018](https://md.research.elamur.ai/free/en/papers/2018/page/6/)

## 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](https://scholar.google.com/scholar?q=Tobias+Nipkow+and+Lawrence+C%2E+Paulson+and+Markus+Wenzel%2C+Isabelle%2FHOL+%2D+A+proof+assistant+for+Higher%2DOrder+Logic%2C+Lecture+Notes+in+Computer+Science%2C+vol%2E+2283%2C+Springer%2C+2002%2C+3%2D540%2D43376%2D7)
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](https://scholar.google.com/scholar?q=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+Sewe)
3. Xavier Leroy, Formal verification of a realistic compiler, Commun. ACM, vol. 52-7, pp. 107-115, 2009 [find](https://scholar.google.com/scholar?q=Xavier+Leroy%2C+Formal+verification+of+a+realistic+compiler%2C+Commun%2E+ACM%2C+vol%2E+52%2D7%2C+pp%2E+107%2D115%2C+2009)
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](https://scholar.google.com/scholar?q=Ramana+Kumar+and+Magnus+O%2E+Myreen+and+Michael+Norrish+and+Scott+Owens%2C+CakeML%3A+a+verified+implementation+of+ML%2C+The+41st+Annual+ACM+SIGPLAN%2DSIGACT+Symposium+on+Principles+of+Programming+Languages%2C+POP)
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](https://md.research.elamur.ai/free/en/papers/hales-2015-formal-proof-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](https://scholar.google.com/scholar?q=Georges+Gonthier%2C+The+four+colour+theorem%3A+engineering+of+a+formal+proof%2C+Computer+Mathematics%2C+8th+Asian+Symposium%2C+ASCM+2007%2C+Singapore%2C+December+15%2D17%2C+2007%2E+Revised+and+Invited+Papers%2C+pp%2E+333)
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](https://scholar.google.com/scholar?q=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+%28TPHOLs+%E2%80%9909%29%2C+Lecture+)
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) [↗](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](https://scholar.google.com/scholar?q=Pedregosa%2C+F%2E%2C+Varoquaux%2C+G%2E%2C+Gramfort%2C+A%2E%2C+Michel%2C+V%2E%2C+Thirion%2C+B%2E%2C+Grisel%2C+O%2E%2C+Blondel%2C+M%2E%2C+Prettenhofer%2C+P%2E%2C+Weiss%2C+R%2E%2C+Dubourg%2C+V%2E+VanderPlas%2C+J%2E%2C+Passos%2C+A%2E%2C+Cournapeau%2C+D%2E%2C+Brucher%2C+M%2E%2C+Perrot%2C+)
10. James, G., Witten, D., Hastie, T., Tibshirani R. An Introduction to Statistical Learning with Applications in R [find](https://scholar.google.com/scholar?q=James%2C+G%2E%2C+Witten%2C+D%2E%2C+Hastie%2C+T%2E%2C+Tibshirani+R%2E+An+Introduction+to+Statistical+Learning+with+Applications+in+R)
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](https://scholar.google.com/scholar?q=Yutaka+Nagashima+and+Ramana+Kumar%2C+A+proof+strategy+language+and+proof+script+generation+for+Isabelle%2FHOL%2C+Automated+Deduction+%2D+CADE+26+%2D+26th+International+Conference+on+Automated+Deduction%2C+Gothenb)
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](https://scholar.google.com/scholar?q=Geoffrey+Irving+and+Christian+Szegedy+and+Alexander+A%2E+Alemi+and+Niklas+Ee%CC%81n+and+Franc%CC%A7ois+Chollet+and+Josef+Urban%2C+Deep%2DMath+%2D+deep+sequence+models+for+premise+selection%2C+Advances+in+Neural+Informati)
13. Sarah M. Loos and Geoffrey Irving and Christian Szegedy and Cezary Kaliszyk, [Deep network guided proof search](https://md.research.elamur.ai/free/en/papers/loos-2017-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…](http://www.easychair.org/publications/pa…) [↗](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](https://scholar.google.com/scholar?q=Ekaterina+Komendantskaya+and+Jo%CC%81nathan+Heras+and+Gudmund+Grov%2C+Machine+learning+in+proof+general%3A+interfacing+interfaces%2C+Proceedings+10th+International+Workshop+On+User+Interfaces+for+Theorem+Provers)
15. Gerwin Klein, Tobias Nipkow, Larry Paulson, Rene Thiemann, Archive of Formal Proofs, [https://www.isa-afp.org/](https://www.isa-afp.org/) [↗](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](https://scholar.google.com/scholar?q=Thibault+Gauthier+and+Cezary+Kaliszyk+and+Josef+Urban%2C+TacticToe%3A+learning+to+reason+with+HOL4+tactics%2C+LPAR%2D21%2C+21st+International+Conference+on+Logic+for+Programming%2C+Artificial+Intelligence+and+Rea)
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](https://scholar.google.com/scholar?q=Jia+Meng+and+Lawrence+C%2E+Paulson%2C+Lightweight+relevance+filtering+for+machine%2Dgenerated+resolution+problems%2C+J%2E+Applied+Logic%2C+vol%2E+7%2D1%2C+pp%2E+41%2D57+2009)
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](https://scholar.google.com/scholar?q=Jasmin+Christian+Blanchette+and+David+Greenaway+and+Cezary+Kaliszyk+and+Daniel+Ku%CC%88hlwein+and+Josef+Urban%2C+A+learning%2Dbased+fact+selector+for+Isabelle%2FHOL%2C+J%2E+Autom%2E+Reasoning%2C+vol%2E+57%2D3%2C+pp%2E+219%2D244+2)
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](https://scholar.google.com/scholar?q=Markus+Wenzel%2C+Isar+%2D+a+generic+interpretative+approach+to+readable+formal+proof+documents%2C+Theorem+Proving+in+Higher+Order+Logics%2C+12th+International+Conference%2C+TPHOLs%E2%80%9999%2C+Nice%2C+France%2C+September%2C+1)
20. Haibo He and Edwardo A. Garcia, Learning from imbalanced data, IEEE Trans. Knowl. Data Eng., vol. 21. pp. 1263-1284. 2009, [find](https://scholar.google.com/scholar?q=Haibo+He+and+Edwardo+A%2E+Garcia%2C+Learning+from+imbalanced+data%2C+IEEE+Trans%2E+Knowl%2E+Data+Eng%2E%2C+vol%2E+21%2E+pp%2E+1263%2D1284%2E+2009%2C)
21. [https://github.com/data61/PSL/releases/tag/v0.1.1](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. [↗](https://github.com/data61/PSL/releases/tag/v0.1.1)
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](https://scholar.google.com/scholar?q=Breiman%2C+Leo%3B+Friedman%2C+J%2E+H%2E%3B+Olshen%2C+R%2E+A%2E%3B+Stone%2C+C%2E+J%2E%2C+1984%2C+Classification+and+regression+trees%2E+Monterey%2C+CA%3A+Wadsworth+%26+Brooks%2FCole+Advanced+Books+%26+Software%2E)
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](https://scholar.google.com/scholar?q=Jasmin+Christian+Blanchette+and+Maximilian+P%2E+L%2E+Haslbeck+and+Daniel+Matichuk+and+Tobias+Nipkow%2C+Mining+the+Archive+of+Formal+Proofs%2C+Intelligent+Computer+Mathematics+%2D+International+Conference%2C+CICM+)
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](https://scholar.google.com/scholar?q=Daniel+Matichuk+and+Toby+C%2E+Murray+and+June+Andronick+and+D%2E+Ross+Jeffery+and+Gerwin+Klein+and+Mark+Staples%2C+Empirical+study+towards+a+leading+indicator+for+cost+of+formal+software+verification%2C+37th+)

*Updated 3 November 2026*