Tým CIIRC ČVUT vedený Dr. J. Urbanem vyhrál mistrovství světa v automatickém usuzování

0
4476

Ve dnech 13. a 14. 7. 2018 se v Oxfordu na Federated Logic Conference (FLoC18) konalo Mistrovství světa v automatickém dokazování vět pro rok 2018 (CASC-J9). Byl to dvacátý třetí ročník této soutěže, která se koná každoročně od roku 1996. Více než dvacet systémů od týmů z USA, Asie a Evropy soutěžilo v šesti divizích.

Ve dvou divizích zvítězily systémy vyvíjené týmem CIIRC ČVUT pracujícím na ERC projektu AI4REASON Dr. Josefa Urbana a jeho spolupracovníků. V divizi LTB (rozsáhlé teorie) zvítězil systém „Machine Learner for Automated Reasoning“ (MaLARea 0.6) vyvíjený Urbanem a jeho kolegy. Tento systém vyřešil o 16% víc z 5000 problémů v této divizi než další systém.  V divizi THF (problémy v logice vyššího řádu) zvítězil systém Satallax 3.2 vyvíjený Dr. Chadem Brownem a jeho kolegy. Tento systém vyřešil o 14% víc z 500 problémů v této divizi než další systém.

Divize LTB obsahuje problémy vznikající ve velkých projektech verifikace matematiky a softwaru. Tento rok to byly problémy z projektu CakeML, který vyvíjí verifikovanou implementaci programovacího jazyka ML. Divize THF 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.