Vědci z týmu Dr. J. Urbana získali cenné trofeje na šampionátu v automatickém uvažování

0
1138

V celosvětové konkurenci univerzit a výzkumných týmů se skvěle umístili vědci ze skupiny automatické uvažování na CIIRC ČVUT, kteří se podílí na vývoji systémů Vampire, MaLARea, Enigma nebo Satallax. Šampionát v automatickém uvažování (The CADE ATP System Competition) se konal online v červenci letošního roku.

Nejlépe se umístil systém Vampire, který zvítězil hned ve 3 kategoriích (Typed First Order Theorems, First Order Theorems a First Order Non-theorems), na jehož vývoji se podílel developer Martin Suda z CIIRC ČVUT společně s kolegy z univerzit v Manchesteru a ve Vídni.

Druhé místo v kategorii First Order Theorems získal systém Enigma Jana Jakubův. Enigma je navíc unikátní tím, že rozšířil již existující systém E o strojové učení a díky němu dokázal vyřešit o 50 z 500 problémů více, což je významné zlepšení v rámci systému, ze kterého je odvozen.

Velmi zajímavá je z pohledu automatického dokazování a CIIRC ČVUT kategorie Large Theory Batch Problems (rozsáhlé teorie), kterou definoval přímo Dr. Josef Urban v v posledních dvou letech společně s Chadem Brownem a Thibaultem Gauthierem tuto divizi na šampionátu připravovali (tzv. GRUNGE data set). Urbanem vyvinutý systém MaLARea (jehož součástí je např. i Enigma Jana Jakubův) dokázal v daném časovém rámci vyřešit více než 7 tisíc z 10 tisíc problémů a s přehledem by s více než tři a půl tisícovým náskokem získal první místo. Z etických důvodů však zůstal systém MaLARea mimo soutěž, demonstruje však sílu strojového učení v oblasti automatického dokazování a také fakt, že na CIIRC ČVUT pracují opravdu celosvětové vědecké špičky v daném oboru.

Jak to na takovém šampionátu funguje? V rámci každé kategorie jsou do soutěže vybrány náhodné matematické problémy, každý soutěžní systém má na řešení pevně daný časový rámec (3 nebo 5 minut, mimo kategorii Large Theory Batch Problems, viz dále). Systém, kterému se v daném časovém rámci podaří vyřešit největší počet problémů ze zadaného maxima, se pak stává vítězem.

Již zmiňovaná kategorie Large Theory Batch problems je určena především pro strojové učení. Na řešení problému je velký časový limit až 24 hodin, systém se může vracet a postupovat od nejsnazších úkolů ke složitějším a zároveň umožňuje využívat systém učení se z úspěchu či neúspěchu. Tato kategorie obsahuje problémy vznikající ve velkých projektech verifikace matematiky a softwaru.

Kategorie Typed First Order Theorems  (problémy v logice vyššího řádu) obsahuje výběr problémů formulovaných v logice vyššího řádu. To je jeden z nejběžnějších formalizmů používaných pro verifikaci velkých matematických důkazů a komplikovaného softwaru.

Na šampionátu jsou využívány příklady problémů ze standardní knihovny HOL4 (GRUNGE: A Grand Unified ATP Challenge). Velmi zjednodušeně by se dalo říci, že soutěžní systémy se naučí pokročilou matematiku a postupně se přibližují k „automatickému matematikovi“, což může v různých aplikacích vést k zásadním výsledkům.

Více informací o šampionátu naleznete zde: http://www.tptp.org/CASC/J10/

 

Systémy, na kterých se podíleli výzkumníci z CIIRC

MaLARea:

Urban, J. (CIIRC, CTU, Prague, Czech Republic)
(Zahrnuje ENIGMA, E-prover, SPASS, Vampire, Paradox, Mace – Jan Jakubuv, Cezary Kaliszyk, Bartosz Piotrowski, Stephan Schulz, Mirek Olšák)

Enigma:

Jakubuv, J. (CIIRC, CTU, Prague, Czech Republic)
Urban, J. (CIIRC, CTU, Prague, Czech Republic)
Chvalovský, K. (CIIRC, CTU, Prague, Czech Republic)
Piotrowski, B. (CIIRC, CTU, Prague, Czech Republic)
Olšák, M. (University of Innsbruck, Innsbruck, Austria)
Suda, M. (CIIRC, CTU, Prague, Czech Republic)
(Zahrnuje E-prover (http://www.eprover.org/)
Schulz, S. (DHBW Stuttgart, Germany))

Vampire:

R. Giles Reger (University of Manchester, Manchester, UK)
Suda, M. (CIIRC, CTU, Prague, Czech Republic)
Voronkov, A. (University of Manchester, Manchester, UK)
Kovacs, L. (TU Wien, Vienna, Austria)
Evgeny Kotelnikov, Martin Riener, Michael Rawson, Bernhard Gleiss,
Jakob Rath, Ahmed Bhayat, Petra Hozzova, Johannes Schoisswohl

Satallax:

Brown, C. (CIIRC, CTU, Prague, Czech Republic)
Färber, M. (University of Innsbruck, Innsbruck, Austria)

ATPBoost:

Piotrowski, B. (CIIRC, CTU, Prague, Czech Republic)
Josef Urban, Stephan Schulz