Projekt Vampire, na němž pracuje i Martin Suda z CIIRC, neustále prochází vývojem a inovacemi, aby zůstal na špičce v rychle se vyvíjejícím poli automatizovaného dokazování, podoboru klasické umělé inteligence. V minulém roce dokazovač Vampire uspěl na světovém šampionátu v automatickém dokazovaní CASC se svou verzí Vampire 4.8 a na letošní prestižní konferenci IJCAR 2024, která se bude konat na začátku července 2024 ve francouzském Nancy, má Martin Suda dokonce tři želízka v ohni v podobě tří přijatých vědeckých článků, z nichž každý se zlepšováním dokazovače Vampire nějakým způsobem souvisí. Gratulujeme!
Výzkumný tým Martin Sudy se v poslední době zaměřuje hlavně na zdokonalování automatických dokazovačů prostřednictvím integrace technik statistické umělé inteligence, tedy především strojového učení. Ony tři přijaté články se však svým zaměřením tentokrát hlásí spíše k tradičnějším postupům v oboru.
Co je nového v týmu automatického uvažování?
Martin Suda a jeho spolupracovníci nezahálejí a posouvají výzkum automatického dokazování dále. Společně s kolegou Ahmedem Bhayatem (dříve působil na Univerzitě v Manchesteru, nyní se vydal zužitkovat nabyté zkušenosti do komerční sféry) nedávno dokončili sedmistránkový vědecký článek, který byl přijat na prezentaci na mezinárodní konferenci IJCAR 2024 – International Joint Conference on Automated Reasoning a představili novou verzi automatického dokazovače Vampire, do něhož byla implementována klíčová inovace: rozšíření jeho schopností o podporu dokazování v logice vyššího řádu. V hlavní divizi soutěže CASC, která se zaměřuje na dokazování logiky prvního řádu, patří Vampire mezi pravidelné a dlouhodobě dominantní účastníky. Martin Suda doufá, že inovace v této sféře zajistí opakování tohoto úspěchu i v letošním roce.
Dalším přijatým příspěvkem na konferenci IJCAR 2024 je společný článek Martina Sudy a jeho kolegů: Sólrún Einarsdóttir, Nicholase Smallbonea a Moy Johansson z Chalmers Univerzity v Göteborgu ve Švédsku a Martona Hajdu z TU Wien v Rakousku. Společnými silami se snaží o zlepšování podpory pro matematickou indukci v dokazovači Vampire tak, aby se matematická indukce dala zautomatizovat úplně.
Třetím přijatým článkem pro prezentaci na konferenci IJCAR 2024 je společná práce se studentem Filipem Bártkem (CIIRC a FEL ČVUT) a Karlem Chvalovským (CIIRC), kteří podnikli rozsáhlou analýzu na téma dokazovacích strategií a jakým způsobem se dají strategie skládat do celých rozvrhů tak, aby bylo dosaženo co nejlepšího výkonu na neznámých úlohách, a aby tyto rozvrhy byly co možná nejkompaktnější v čase. Součástí výzkumu bylo i zkoumání algoritmu, který umí strategie skládat do rozvrhu se specifickými vlastnostmi. Jednou z těchto vlastností je to, že si má systém zapamatovat řešení, která byla objevena při tréninku. Dále musí systém dobře fungovat i za přítomnosti šumu, chyb, odlehlých hodnot nebo jiných nedokonalostí v datech, se kterými pracuje tak, aby byla dobře přenositelná na problémy neviděné při tréninku. V odevzdaném článku byla řešena také pravděpodobnost očekávání dobrého výkonu i při takovémto scénáři.
Dokazovač Vampire, na jehož vývoji se spolupodílí Martin Suda (vedoucí týmu automatického uvažování na CIIRC), představuje špičku v oblasti automatizovaného dokazování teorémů. Vampire je známý pro svou efektivitu v řešení komplexních problémů v logice prvního řádu a jeho význam v oblasti informatiky, matematiky a umělé inteligence je nepopiratelný. Tento nástroj vyniká svou pokročilou implementací algoritmů a technik, což umožňuje efektivní řešení i velmi náročných úloh. Jeho flexibilita a široké uplatnění v různých oblastech, jako je informatika, matematika a umělá inteligence, ukazují na jeho význam jako nástroje pro automatizované dokazování teorémů. V minulém roce Vampire vyhrál kategorie First-order Non-theorems, Typed First-Order Non-Theorems, Typed First-order Theorems a také kategorii Higher-order Theorems. Poslední zmiňovaná kategorie aktuálně představuje pro vědce zajímavou výzvu. Logika vyššího řádu je daleko výrazově bohatší než standardně studovaná logika prvního řádu, zároveň je ale uvažování v ní o tolik složitější, že byla do nedávné doby považována za pro automatizaci nevhodnou.
O konferenci IJCAR:
IJCAR 2024, Mezinárodní konference o automatickém uvažování, je prestižní událost ve vědecké komunitě, která se zaměřuje na nejnovější výzkum a vývoj v oblasti automatizovaného uvažování a příbuzných výzev. Tato konference představuje platformu pro prezentaci pokročilých výzkumných prací, diskusi o inovacích a sdílení znalostí mezi expertními komunitami. Jde o klíčové setkání pro vědce, akademiky a profesionály z oblasti informatiky, matematiky a umělé inteligence. Pro více informací navštivte web konference. Konference se koná na začátku července v Nancy, France v výzkumném centru INRIA pod univerzitiu v Lotrinsku.
O soutěži CASC:
Soutěž CASC (CADE ATP System Competition) je každoroční hodnocení plně automatických systémů pro dokazování vět (ATP) v klasické logice, což je v podstatě světové mistrovství pro takové systémy. CASC je součástí každé konference CADE a IJCAR, které jsou hlavními fóry pro prezentaci nového výzkumu ve všech aspektech automatizované dedukce. Tato soutěž je důležitou platformou pro vyhodnocení schopností ATP systémů a motivací pro výzkum a vývoj robustních ATP systémů, které jsou snadno a užitečně použitelné v aplikacích.
