en | de

Machine Learning for Theorem Proving

master program

VU3  WS 2023/2024  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 04.10. theorem proving systems pdf
2 11.10. machine learning problems pdf
3 18.10. naive Bayes and k-NN classifiers pdf
4 25.10. regression in theorem proving pdf
5 08.11 decision trees and random forests pdf
6 15.11 typing: blackboardno homework
722.11. type inference pdf
8 29.11. deep learning for premise selection pdf
9 06.12. no course
10 13.12. learning in superposition, enigma, state evaluation, introduction to tableaux pdf
11 10.01. presentations
12 17.01 indexing based internal guidance, deep inference guidance
13 24.01. Reinforcement Learning in Proving: Malarea, RLCoP pdf
14 31.01. final in-class assignments

Recommended Literature