SubjectsSubjects(version: 945)
Course, academic year 2023/2024
   Login via CAS
Machine Learning and Reasoning - NMMB562
Title: Strojové učení a uvažování
Guaranteed by: Department of Algebra (32-KA)
Faculty: Faculty of Mathematics and Physics
Actual: from 2022
Semester: summer
E-Credits: 3
Hours per week, examination: summer s.:2/0, Ex [HT]
Capacity: unlimited
Min. number of students: unlimited
4EU+: no
Virtual mobility / capacity: no
State of the course: not taught
Language: English, Czech
Teaching methods: full-time
Teaching methods: full-time
Additional information:
Guarantor: Mgr. Josef Urban, Ph.D.
RNDr. Martin Suda, Ph.D.
Mgr. Mikoláš Janota, Ph.D.
Class: M Mgr. MMIB
M Mgr. MMIB > Volitelné
Classification: Mathematics > Algebra
Annotation -
Last update: doc. Mgr. Petr Kaplický, Ph.D. (19.02.2019)
The course will introduce modern AI methods and architectures that combine reasoning and learning.
Course completion requirements - Czech
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (11.06.2019)

Předmět je zakončen ústní zkouškou.

Literature -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)

Cezary Kaliszyk, Josef Urban: Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reasoning 53(2): 173-213 (2014)

John Harrison, Josef Urban, Freek Wiedijk: History of Interactive Theorem Proving. Computational Logic 2014: 135-214

John Harrison: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press 2009, ISBN 978-0-521-89957-4, pp. I-XIX, 1-681

Ian Goodfellow and Yoshua Bengio and Aaron Courville: Deep Learning. MIT Press 2016.

Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák: Reinforcement Learning of Theorem Proving. NeurIPS 2018: 8836-8847

Alexander A. Alemi, François Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection. NIPS 2016: 2235-2243

Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish: Learning to Prove with Tactics. CoRR abs/1804.00596 (2018)

Jan Jakubuv, Josef Urban: ENIGMA: Efficient Learning-Based Inference Guiding Machine. CICM 2017: 292-302

Mikolás Janota: Towards Generalization in QBF Solving via Machine Learning. AAAI 2018: 6607-6614

Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban: Hammering towards QED. J. Formalized Reasoning 9(1): 101-148 (2016)

Josef Urban, Jirí Vyskocil: Theorem Proving in Large Formal Mathematics as an Emerging AI Field. Automated Reasoning and Mathematics 2013: 240-257

Mikolas Janota, Martin Suda: Towards Smarter MACE-style Model Finders. LPAR 2018: 454-470

Cezary Kaliszyk, Josef Urban, Jirí Vyskocil: Efficient Semantic Features for Automated Reasoning over Large Theories. IJCAI 2015: 3084-3090

Cezary Kaliszyk, Josef Urban, Jirí Vyskocil: Automating Formalization by Statistical and Semantic Parsing of Mathematics. ITP 2017: 12-27

Qingxiang Wang, Cezary Kaliszyk, Josef Urban: First Experiments with Neural Translation of Informal to Formal Mathematics. CoRR abs/1805.06502 (2018)

Karel Chvalovsky: Top-Down Neural Model For Formulae. ICLR 2019,

Jan Jakubuv, Josef Urban: Hierarchical invention of theorem proving strategies. AI Commun. 31(3): 237-250 (2018)

Josef Urban, Geoff Sutcliffe, Petr Pudlák, Jirí Vyskocil: MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance. IJCAR 2008: 441-456

Requirements to the exam -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (27.02.2021)

Will be specified later.

Syllabus -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)
  • 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.

Charles University | Information system of Charles University |