Machine Learning and Reasoning (Summer 2019)

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:


  • 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.~

Lectures - TBA

8th March 2019
Josef Urban
Machine Learning and Automated Reasoning - Introduction
15th March 2019
Michael Rawson and Martin Suda
First-order saturation-style theorem proving and ML, Vampire, orderings and their influence on proof search
22nd March 2019
Josef Urban, Jan Jakubuv, Karel Chvalovsky and Martin Suda
Machine learning for internal guidance of first-order saturation-style theorem proving, E prover
29th March 2019
5th April 2019
26th April 2019
Prover9, Symbolic Guidance with Proof Sketches and Hints
3rd May 2019
Josef Urban
Reinforcement learning for connection calculus, other feedback loops
10th May 2019
Josef Urban
Premise selection, ITP/ATP hammers, overview of features used for learning
17th May 2019
Thibault Gauthier
Guiding tactical interactive provers, HOL4, HOLyHammer, TacticToe
24th May 2019
Karel Chvalovsky
Neural representation of formulas