Machine Learning and Reasoning (Summer 2020)
The course is registered at MFF and taking place either at CIIRC (Dejvicka) or in Karlin. Please fill in the form if you are interested in participating.
Abstract: 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, conjecturing and systems for automating computer understanding of math. The course is organized by Josef Urban and guest lectures will be given by ARG researchers working on the particular topics: Jan Jakubuv, Martin Suda, Mikolas Janota, Karel Chvalovsky, Chad Brown, Bob Veroff and Thibault Gauthier. For a brief overview of the area, see this talk at AGI'18 . In more detail, we plan to cover the following topics:
Topics
- Theorem proving systems - Automated and interactive theorem proving, SMT
- Reasoning and learning over very large knowledge bases (Premise selection, Hammers for interactive proof assistants HOL, Mizar and Isabelle).
- Guiding saturation-style and connection-style reasoners (ENIGMA, Hints, ProofWatch, MaLeCoP, Deep guidance).
- Guiding tactical interactive provers (TacTicToe).
- Feedback loops between obtaining new knowledge by proving and learning, reinforcement learning and positive/negative proof mining (MaLARea, rlCoP, DeepMath, ATPBoost)
- Learning for SAT, QBF, SMT and model finding.
- Machine learning and reasoning for translation and alignment between different math corpora.
- Topics in representation and conjecturing - hand-engineered features, neural and semantic representations, EnigmaWatch.~