Nie jesteś zalogowany | Zaloguj się

Automated Reasoning in Large Theories and Premise Selection with Machine Learning

Prelegent(ci)
Bartosz Piotrowski
Afiliacja
Uniwersytet Warszawski
Termin
14 marca 2018 14:15
Pokój
p. 5050
Seminarium
Seminarium „Teoria automatów”

In the talk I will briefly overview current state-of-the-art in the
fields of Formal Mathematics and Automated Theorem Proving and how
Machine Learning techniques can be fruitfully applied in these
domains. One of crucial problems when automatically proving theorems
in formal mathematical library is premise selection task, and machine
learning is very useful there. I will show the results of my recent
experiments of performing Premise Selection with use of Gradient
Boosted Trees, on Mizar Mathematical Library.

Preprint with the results: https://arxiv.org/abs/1802.03375 <--
submitted to a major conference in AI
Implementation of the system for experiments:
https://github.com/BartoszPiotrowski/ATPboost