Poslední úprava: 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.
Poslední úprava: doc. Mgr. Petr Kaplický, Ph.D. (19.02.2019)
The course will introduce modern AI methods and architectures that combine reasoning and learning.
Podmínky zakončení předmětu
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (11.06.2019)
Předmět je zakončen ústní zkouškou.
Literatura -
Poslední úprava: 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/
Poslední úprava: 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/
Požadavky ke zkoušce -
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (27.02.2021)
Požadavky budou upřesněny.
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (27.02.2021)
Will be specified later.
Sylabus -
Poslední úprava: 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.
Poslední úprava: 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).
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.
