en | de

Machine Learning for Theorem Proving

master program

VO2  SS 2018  703819

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 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, HH, RLCoP
12 27.04. strategy selection, theorem proving features
13 04.05. learning for dependent type theory
14 08.05. generative methods, learning formalization
15 11.05. first exam, May 11, HSB 03, 9:15

Registration for the exams is mandatory, 5-2 weeks before the exam!

Literature

Will be given in the course.