en | de

Machine Learning for Theorem Proving

master program

VO2  SS 2018  703819


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.


week date topics slides
1 06.03. theorem proving systems pdf
2 09.03. machine learning problems pdf
3 13.03. naive Bayes and k-NN classifiers pdf
4 16.03. regression in theorem proving pdf
5 20.03(HSB 7) decision trees and random forests pdf
6 23.03(HSB 4) deep learning for premise selection pdf
7 10.04. introduction to ATPs pdf
8 13.04. learning in superposition, deep learning in ATPs pdf
9 17.04. enigma, state evaluation, introduction to tableaux pdf
10 20.04. indexing based internal guidance, deep inference guidance pdf
11 24.04. Reinforcement Learning in Proving: Malarea, RLCoP pdf
12 27.04. learning choices in HOLyHammer pdf
13 04.05. theorem proving features pdf
14 08.05. matching concepts and aligning libraries pdf
15 (additional slides) generative methods, learning formalization pdf
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