Martin Suda vylepšuje automatické dokazovače pomocí strojového učení

0
1218

Martin Suda získal juniorský grant Grantové agentury ČR, jehož cílem je zlepšování automatických dokazovačů vět pomocí strojového učení. Dokazovače mají široké uplatnění v průmyslu, kde se využívá formálních důkazů bezpečnosti systémů, speciálně v oblasti automotive, letectví nebo medicíny.

Grant GA ČR získal Martin Suda na tři roky a s jeho pomocí může na CIIRC ČVUT sestavit svůj mikrotým, který se bude na výzkumu podílet. Výzkum je zajímavý tím, že propojuje dvě oblasti, a to oblast strojového učení a automatického dokazování. „Nadneseně řečeno se ve svém výzkumu pokusím naplnit sen filozofa Leibnitze, jehož vizí bylo, aby o matematice mohly uvažovat stroje,“ popisuje Martin Suda svůj výzkum.  „Mým cílem je, abychom docílili značné univerzálnosti, tzn., aby jazyk dokazovače byl dost obecný na to, abychom jej mohli využít v různých aplikacích,“ dodává Suda.

Projekt bude systematicky zkoumat téma kombinování metod strojového učení s nejmodernějšími dokazovači teorémů (ATP). Konečným cílem je zlepšení výkonu ATP v celé řadě úkolů z oblasti automatického uvažování a v oblastech jako formalizovaná matematika a verifikace software. V minulosti se Suda zabýval například vylepšováním dokazovače Vampýr (Vampire), který se pravidelně umisťuje na předních příčkách na mistrovství světa v automatickém dokazování.