Automatický dokazovač Vampire, jehož vývoj vede Martin Suda – vedoucí týmu automatického uvažování na CIIRC ČVUT a držitel RICAIP Tenure Track pozice, dosáhl letos mimořádného úspěchu. Na jubilejním 30. ročníku soutěže CADE ATP System Competition (CASC) 2025 poprvé v historii zvítězil ve všech osmi kategoriích – výkon, který se dosud žádnému jinému systému nepodařil.
Soutěž CASC-30, která proběhla 30. července 2025 ve Stuttgartu, byla pro systém Vampire naprosto výjimečná. Nejenže obhájil své loňské vítězství, ale letos jako vůbec první dokazovač v celé historii soutěže zvítězil ve všech osmi vypsaných divizích. včetně obnovené kategorie Effectively Propositional CNF, která se do soutěže vrátila po pětileté pauze.
Výrazné zlepšení bylo letos patrné zejména v kategoriích zaměřených na aritmetické uvažování (Typed First-order Theorems +-/) a rovnostní uvažování (Unit Equality CNF), kde se uplatnily i optimalizace vyvinuté ve spolupráci s kolegy z TU Wien, zejména Mártonem Hajduem. Za výjimečným výkonem stojí systematická příprava, nové strategie a úzká spolupráce vývojářů z několika evropských institucí.
Martin Suda, vedoucí týmu automatického uvažování na CIIRC ČVUT, byl letos již podruhé odpovědný za přípravu tzv. portfolia strategií – klíčového prvku soutěže. Každý problém je totiž potřeba řešit s omezeným množstvím předem naplánovaných strategií, které musí pokrýt co nejširší spektrum obtížných případů a navzájem se doplňovat.
„Příprava portfolia strategií je trochu jako plánování šachového turnaje – každá strategie hraje roli jiného mistra a musí zapadnout do celkové taktiky. Letos se nám podařilo vytvořit sestavu, která dokázala reagovat na všechny typy problémů,“ říká Martin Suda, vedoucí týmu automatického uvažování na CIIRC ČVUT.
V další fázi vývoje tým Vampire plánuje využít techniky strojového učení a rozšířit strategii o přístupy naváděné neuronovými sítěmi. „Naším cílem pro příští rok je integrovat do Vampire strategie naváděné neuronovými sítěmi. Pracujeme na tom už několik let a začínáme vidět skutečné výsledky,“ dodává Suda.
Kdo stojí za dokazovačem Vampire?
Na vývoji dokazovače Vampire se podílí mezinárodní tým výzkumníků z několika předních evropských univerzit. Tato spolupráce propojuje odborníky na logiku, formální verifikaci, softwarové inženýrství i strojové učení a umožňuje systému udržet si náskok na světové úrovni.
Mezi hlavní vývojáře patří:
- Martin Suda, Filip Bártek a Petra Hozzová (CIIRC ČVUT)
- Ahmed Bhayat, Giles Reger, Andrei Voronkov (University of Manchester)
- Laura Kovács, Márton Hajdu, Matthias Hetzenberger, Jakob Rath, Robin Coutelier, Johannes Schoisswohl (TU Wien)
- Michael Rawson (University of Southampton)
Další mezinárodní ocenění – článek „The Vampire Diary“ získal „Distinguished Paper Award“
Rok 2025 byl pro tým Vampire výjimečný nejen soutěžními výsledky. Na prestižní konferenci CAV 2025 získal tým ocenění Distinguished Paper Award za článek The Vampire Diary, který mapuje vývoj dokazovače za posledních deset let.
O soutěži CASC a konferenci CADE
CADE ATP System Competition (CASC) je každoroční mezinárodní soutěž v automatickém dokazování, která se koná jako součást konferencí CADE (Conference on Automated Deduction) nebo IJCAR. Představuje prestižní klání nejlepších automatizovaných systémů pro dokazování v klasické logice a je považována za světový šampionát v této oblasti.
Cílem soutěže je objektivně porovnat schopnosti jednotlivých systémů. Hodnotí se především počet správně vyřešených problémů v daném časovém limitu (obvykle 3 až 5 minut), ale také kvalita a úplnost výstupu. CASC zároveň slouží jako motivace pro výzkum, vývoj robustních nástrojů a jako platforma pro výměnu zkušeností v rámci odborné komunity.
Třicátý ročník soutěže, CASC-30, se uskutečnil 30. července 2025 ve Stuttgartu, jako součást jubilejní konference CADE-30, která proběhla vtermínu 28. 7. – 2. 8. 2025. Organizátorem soutěže byl tradičně Dr. Geoff Sutcliffe (University of Miami). Na regulérnost a transparentnost průběhu soutěže dohlížela nezávislá porota ve složení Aart Middeldorp, Cláudia Nalon a Tjark Weber.
