Mgr. Josef Urban, Ph.D.

Školitel-specialista: Lasse Blaauwbroek, MSc.

Strojové učení pro interaktivní dokazování vět je téma, o které je rostoucí zájem. Je řada individuálních projektů, které v posledních letech zaznamenaly značný úspěch. Stále však zbývá mnoho práce, aby se strojové učení stalo prakticky užitečným. Jednou z překážek je, že většina projektů existuje v rámci svého individuálního sila a nelze je přímo porovnávat s ostatními. Tento problém se již řeší v širší oblasti strojového učení prostřednictvím iniciativ, jako je platforma OpenML [1, 2], která umožňuje vytvářet datové sady a odpovídající úlohy a nahrávat je na platformu. Po nahrání datové sady a úlohy může kdokoli vytvořit a nahrát modely, které se pokusí úlohu vyřešit. Platforma pak automaticky vyhodnotí a porovná všechny odeslané modely a vytvoří interaktivní vizualizace, které zdůrazní relativní silné a slabé stránky modelů. Kolaborativní platformy přinášejí značné výhody, z nichž nejdůležitější je možnost snadno porovnávat různé modely učení prostřednictvím spravedlivých a konzistentních srovnávacích testů, které reprezentují reálné podmínky. V současné době si každý projekt strojového učení vyvíjí vlastní techniku hodnocení, z nichž mnohé nereprezentují reálné podmínky. Výzkumy v oblasti spolupráce člověka s počítačem navíc ukázaly, že "gamifikace" obtížných problémů výrazně napomáhá kompetitivnímu zapojení komunity [3]. Bohužel data, metody vyhodnocování a modely spojené s dokazováním vět jsou příliš složité na to, aby se vešly do obecného rámce iniciativ, jako je OpenML. Proto vyvineme speciální platformu pro interaktivní dokazování vět. Předchozí pokusy o vývoj centrálizované platformy pro dokazování tvrzení [4, 5, 14] se příliš neujaly kvůli absenci interaktivní složky. Poskytují jedinou statickou sadu dat a kód k provedení vyhodnocení, ale chybí jim možnost automaticky, spravedlivě a interaktivně porovnávat různé modely. Tato práce je na pomezí několika témat, včetně strojového učení, dokazování vět, interakce člověka s počítačem, webových technologií a počítačového inženýrství. Vývoj úspěšné platformy zahrnuje různé výzkumné úhly pohledu a různé technické komponenty.

Více informací:

• DocsGoogle

Školitel-specialista: RNDr. Martin Suda, Ph.D.

Cílem automatizovaného dokazování tvrzení je automatizace matematicky přesného deduktivního usuzování s aplikacemi ve formální verifikaci kritických bezpečnostních systémů nebo ve formalizaci matematiky. Výzkum praktických automatických dokazovačů kombinuje vývoj logických kalkulů s jejich efektivní implementací a empirickým vyhodnocením na relevantních množinách problémů. Neméně důležitou roli hrají účinné heuristiky, které pomáhají řídit hledání důkazu. Nedávné pokroky v umělé inteligenci, zejména strojové učení a neuronové sítě, umožňují automatické objevování takových heuristik, a to buď na základě předchozích zkušeností s dokazováním, nebo v rámci zpětnovazebního učení (reinforcement learning). Cílem práce bude posunout stav poznání v této oblasti a vyvinout nové metody pro automatické objevování heuristik pro hledání důkazů.

Školitel-specialista: Dr. Adam Pease

Budete trénovat moderní jazykové modely, které budou překládat výroky přirozeného jazyka, jako například "Šálek je na stole", na výroky formální logiky. Ty budou nakonec použity dnešními automatizovanými dokazovači vět (ATP), jako jsou Vampire a E prover, k odvození závěrů z těchto výroků. V tomto výzkumu budeme používat jazyk a formální ontologii SUMO (https://www.ontologyportal.org/). Například předchozí výrok bude v SUMO vypadat následovně:

(exists (?X ?Y)
   (a
      (instance ?X Table)
      (instance ?Y Cup)
      (orientace ?Y ?X On)))

Jazykový překlad bude doplněn sémantickými nástroji, jako je např. syntaktická a sémantická kontrola v SUMO. Dále budou vyvinuty metody rozšiřování dat s cílem zvětšit velikost trénovacího korpusu pro NLP metody. To zahrnuje například generování syntetických dat pomocí tzv. logic-to-language překladače SUMO, přímého překladu do různých přirozených jazyků a generování tranzitivních dat prostřednictvím NLP metod, jako je překladač Google Translate. Konečným cílem je automatické obohacování znalostní báze SUMO o velké množství comon-sense faktů vyjádřených v přirozeném jazyce. To následně umožní automatizované uvažování o rostoucím množství každodenních témat.