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: http://arg.ciirc.cvut.cz/teaching/mlr20
• 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

English

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.

Czech

Last update: doc. Mgr. Petr Kaplický, Ph.D. (19.02.2019)

Přednáška uvede moderní metody a architektury pro strojové uvažování a jeho kombinace s učením.

Course completion requirements

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

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

Literature

English

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, https://openreview.net/pdf?id=Byg5QhR5FQ

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

http://arg.ciirc.cvut.cz/teaching/mlr19/

Czech

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, https://openreview.net/pdf?id=Byg5QhR5FQ

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

starší kurz: http://arg.ciirc.cvut.cz/teaching/mlr19/

Requirements to the exam

English

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

Will be specified later.

Czech

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

Požadavky budou upřesněny.

Syllabus

English

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.

Czech

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

• Přednáška uvede moderní metody a architektury, které kombinují strojové uvažování a učení. Stručně představíme dnešní hlavní systémy pro automatické a interaktivní dokazování vět, SMT solvery a velké formální knihovny. Dále probereme typické úlohy strojového učení, které odpovídají automatickému uvažování, od výběru znalostí z velkých znalostních bází, reprezentace znalostí a prohledávání, po detailní vedení dokazování. Podrobněji plánujeme pokrýt následující témata:

• 1. Dokazování a učení v rozsáhlých znalostních bázích (výběr předpokladů, “hammer” systémy pro interaktivní dokazovače HOL, Mizar a Isabelle).

• 2. Vedení saturačních a tableau dokazovačů (ENIGMA, metoda hintů, ProofWatch, MaLeCoP, Deep guidance).

• 3. Vedení interaktivních dokazovačů (TacTicToe).

• 4. Zpětné vazby mezi dokazováním a učením, reinforcement learning, pozitivní / negativní boosting (MaLARea, rlCoP, DeepMath, ATPBoost)

• 5. Učení pro SAT, QBF, SMT a hledání modelů.

• 6. Strojové učení a dokazování pro překlad a propojení mezi různými matematickými korpusy.

7. Reprezentace a tvorba domněnek - standardní symbolické reprezentace, neuronové a sémantické reprezentace, EnigmaWatch.