Neural modelling of mathematical structures and their extensions
| Název práce v češtině: | Neuronové modelování matematických struktur a jejich rozšíření |
|---|---|
| Název v anglickém jazyce: | Neural modelling of mathematical structures and their extensions |
| Klíčová slova: | Umělá inteligence Automatické uvažovaní Strojové učení Teorie modelů |
| Klíčová slova anglicky: | Artificial Intelligence Automated Reasoning Machine Learning Model theory |
| Akademický rok vypsání: | 2016/2017 |
| Typ práce: | diplomová práce |
| Jazyk práce: | angličtina |
| Ústav: | Katedra algebry (32-KA) |
| Vedoucí / školitel: | Mgr. Josef Urban, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 19.05.2017 |
| Datum zadání: | 19.05.2017 |
| Datum potvrzení stud. oddělením: | 25.05.2017 |
| Datum a čas obhajoby: | 18.06.2019 12:00 |
| Datum odevzdání elektronické podoby: | 09.05.2019 |
| Datum odevzdání tištěné podoby: | 10.05.2019 |
| Datum proběhlé obhajoby: | 18.06.2019 |
| Oponenti: | doc. Mgr. Štěpán Holub, Ph.D. |
| Zásady pro vypracování |
| Obsahem práce bude:
1. Seznámení se současnými metodami umělé inteligence a strojového učení používanými pro automatické uvažování. 2. Zaměření se na konkrétní podproblém, jako např. selekce premis, řízení dokazovačů na různých úrovních, navrhování a vyhodnocování lemat, pojmů, domněnek a modelů, atd. 3. Experimenty se současnými metodami nad vhodnými matematickými korpusy. 4. Vylepšování současných metod. |
| Seznam odborné literatury |
| High-level interview for MIRI about the AI/reasoning field: http://intelligence.org/2013/12/21/josef-urban-on-machine-learning-and-automated-reasoning/
Video of Tom Hales's talk on formalization: https://www.youtube.com/watch?v=wgfbt-X28XQ Popular article on formalization: http://www.cl.cam.ac.uk/~jrh13/papers/cacm.pdf General talk on the topics of AI & theorem proving: https://slideslive.com/38899958/artificial-intelligence-and-theorem-proving Alan Bundy's old book on computational modelling of reasoning: http://www.inf.ed.ac.uk/teaching/courses/ar/book/book_2010.06.23.pdf Book chapter on history of interactive theorem proving: http://www.cl.cam.ac.uk/~jrh13/papers/joerg.html Longer paper introducing the AI/reasoning field and the opportunities: http://arxiv.org/abs/1209.3914 Prover9 manual: https://www.cs.unm.edu/~mccune/prover9/manual-examples.html More technical papers: http://link.springer.com/article/10.1007%2Fs10817-014-9303-3 , https://jfr.unibo.it/article/view/4593, http://arxiv.org/abs/1701.06532, http://papers.nips.cc/paper/6280-deepmath-deep-sequence-models-for-premise-selection , http://arxiv.org/abs/1611.09703, http://arxiv.org/abs/1611.08733, http://dx.doi.org/10.1007/978-3-540-71070-7_37 . Our course on formal math and proof assistants: http://arg.ciirc.cvut.cz/fmpa/ Useful slides about the topics from the AITP conference: http://aitp-conference.org/2016/ , http://aitp-conference.org/2017/ |
| Předběžná náplň práce |
| Toto téma se soustředí na vývoj metod umělé inteligence pro automatické uvažování. Výzkumné
oblasti zahrnují strojové učení pro vedení automatických a interaktivních dokazovačů na různých úrovních, automatické navrhování vhodných dokazovacích strategií a procedur pro různé třídy problémů, automatické nacházení vhodných lemat, domněnek a pojmů, které jsou důležité pro delší důkazy a vývoj zajímavých teorií, metody jako je Monte-Carlo prohledávání a reinforcement learning nad mnoha problémy a důkazy, metody pro propojování a překlad velkých formálních, poloformálních a neformálních důkazových korpusů a knihoven, a podobná témata. Více informací lze nalézt na http://ai4reason.org/ . |
| Předběžná náplň práce v anglickém jazyce |
| The focus of this work is development of Artificial Intelligence methods for automation of
reasoning. The research areas include machine learning guidance of automated and interactive theorem provers on various levels, automated invention of suitable theorem proving strategies and procedures for classes of problems, automated discovery of suitable lemmas, conjectures and concepts that are important for finding longer proofs and developing interesting theories, methods such as Monte-Carlo proof search and reinforcement learning over many problems and proofs, methods for aligning and translating large formal, semiformal and informal proof corpora and libraries, and similar topics. For further information see http://ai4reason.org/. |