Syllabus
- The course will introduce modern AI methods and architectures that combine reasoning and learning. We will briefly introduce the main ideas behind today's automated and interactive theorem proving systems and other solvers, and the main reasoning corpora. Then we will go through several machine learning problems that correspond to the reasoning tasks, ranging from high-level knowledge selection and representation of the reasoning state and knowledge, to low-level guidance of reasoning. In more detail, we plan to cover the following topics: -
1. Reasoning and learning over very large knowledge bases (Premise selection, Hammers for interactive proof assistants HOL, Mizar and Isabelle). -
2. Guiding saturation-style and connection-style reasoners (ENIGMA, Hints, ProofWatch, MaLeCoP, Deep guidance). -
3. Guiding tactical interactive provers (TacTicToe). -
4. Feedback loops between obtaining new knowledge by proving and learning, reinforcement learning and positive/negative proof mining (MaLARea, rlCoP, DeepMath, ATPBoost) -
5. Learning for SAT, QBF, SMT and model finding. -
6. Machine learning and reasoning for translation and alignment between different math corpora. -
7. Topics in representation and conjecturing - hand-engineered features, neural and semantic representations, EnigmaWatch.
Annotation
The course will introduce modern AI methods and architectures that combine reasoning and learning.