Content
The course on learning problems in theorem proving introduces the design of automated and interactive theorem proving systems as well as proof certifiers and discusses the various machine learning problems that correspond to the built in heuristics. First, the course will focus on the high-level learning problems in proof assistants and techniques for the selection of relevant lemmas in large libraries. Next the focus of the course will be on strategy selection and strategy tuning using learning. Finally internal guidance of automated reasoning systems, including prediction of useful inference steps and tactics, as well as the evaluation of intermediate proof states will be discussed.
Schedule
| week | date | topics | slides |
|---|---|---|---|
| 1 | 06.03. | theorem proving systems | |
| 2 | 09.03. | machine learning problems | |
| 3 | 13.03. | naive Bayes and k-NN classifiers | |
| 4 | 16.03. | regression in theorem proving | |
| 5 | 20.03(HSB 7) | decision trees and random forests | |
| 6 | 23.03(HSB 4) | deep learning for premise selection | |
| 7 | 10.04. | introduction to ATPs | |
| 8 | 13.04. | learning in superposition, deep learning in ATPs | |
| 9 | 17.04. | enigma, state evaluation, introduction to tableaux | |
| 10 | 20.04. | indexing based internal guidance, deep inference guidance | |
| 11 | 24.04. | Reinforcement Learning in Proving: Malarea, RLCoP | |
| 12 | 27.04. | learning choices in HOLyHammer | |
| 13 | 04.05. | theorem proving features | |
| 14 | 08.05. | matching concepts and aligning libraries | |
| 15 | (additional slides) | generative methods, learning formalization | |
| 16 | 11.05. | first exam, May 11, HSB 03, 9:15 |
Registration for the exams is mandatory, 5-2 weeks before the exam.
Recommended Literature
- J. Harrison et al: History of Interactive Theorem Proving
- A. Alemi et al. DeepMath - Deep Sequence Models for Premise Selection
- S. Schulz: E Prover manual
- M.Wang et al: Graph Embeddings for premise selection
- C.Sutton et al: Continuous representation of formulae
- Jakubuv, Urban: ENIGMA
- Machine Learning Connection Prover
- Thinking Fast and Slow with Deep Learning and Tree Search
- Hammer for Coq: Automation for Dependent Type Theory
- A. Alemi. Segmented Articles On The Arxiv
- S. Ross et al. Dagger
- T. Sekiyama and K. Suenaga. Automated Proof Synthesis
- R. Evans et al. Possible Worlds
- K. Kristovski et al. Equation Embeddings
- D. Selsam et al. NeuroSAT
- Kucik and Korovin: Premise Selection