Baví mě zjišťovat, proč věci fungují tak, jak fungují, říká oceněný doktorand z FIT VUT

Ačkoliv mu ze začátku téma nepřišlo nijak zásadní, nakonec ho nasměřovalo do vědy. „Neviděl jsem nějakou stěžejní hodnotu toho výzkumu, ale nakonec se z toho podařilo s velkou pomocí vedoucího práce doktora Lengála a jeho týmu vytvořit odbornou publikaci na konferenci International Conference on Computer-Aided Verification (CAV) 2024. A tak jsem se dostal do výzkumu,” popisuje Hečko. Podotýká ale, že už implementační práci kolem aritmetiky s automaty trochu nezvládal a byl z tématu celkově unavený. „Tehdy mi dal vedoucí zadání, ať zkusím řešit otevřené problémy v teorii řetězců. A to mě začalo hrozně bavit,” říká Michal Hečko.

Konkrétně se věnuje zkoumání logických formulí a jejich splnitelnosti. „Formální verifikace je proces, kdy chci ukázat, že můj software má a nebo nemá nějakou vlastnost. Například že nikdy nebude dělit nulou na určitém místě nebo se nedostane do chybového stavu. A popíšu, co je to ten chybový stav. Je to celý komplexní proces, v jehož úplných základech je matematická logika. Mě konkrétně pak zajímá, když na vstupu dostanu nějakou takovou logickou formuli, která popisuje vlastnost toho systému, tak zda existuje, nebo neexistuje řešení, nebo jak těžké je najít to řešení. Moje algoritmy musí být korektní. To znamená, že pokud říkají, že vlastnost platí, pak skutečně platí a není zde prostor pro ,možná platí´", objasňuje Michal Hečko s tím, že pracuje na úplných základech, na kterých následně celá formální verifikace může stavět.

Ačkoliv se na první pohled může jeho práce jevit velmi teoretická a běžnému životu vzdálená, opak je pravdou. „V dnešní době jsou počítače ve všech oblastech našeho života a za každým počítačem nebo automatizovaným strojem je software. Čím víc jsou počítače v našich životech, tím víc se zvyšuje cena, když počítač udělá chybu. Ta cena může být astronomicky velká. Příklad z historie je výbuch rakety, kdy škoda dosáhla k 370 milionům dolarů. Takže čím víc používáme počítače, tím častěji můžeme najít situace, kdy chyba v softwaru může vést k obrovským ztrátám. Proto je stále důležitější umět formálně dokázat, že chyba nenastane,” vysvětluje Hečko.

Oblast, které se v rámci formální verifikace Michal Hečko věnuje, je podle jeho slov velmi složitá. „Problém, na kterém momentálně pracuju, je šíleně komplikovaný. Ale právě proto, že je to tak namáhavé, tak pocit uspokojení, když se podaří nějaký posun, je o to větší,” říká s úsměvem.

Michal Hečko mezi oceněnými z VUT na letošním slavnostním vyhlášení cen stipendijního programu Brno Ph.D. Talent. | Autor: Václav Koníček
Projekt Michala Hečka je složen z několika částí. První tvoří právě práce na otevřených problémech v teorii řetězců. „Tam to jde skvěle. Podařilo se nám dokázat to, co jsme dokázat chtěli. Teď o části výzkumu vyjde článek,” říká. Další dvě části projektu jsou pak teprve před ním. „Vypadá to, že ty budou ještě namáhavější. Mám už hodně nápadů, jak na to, ale bohužel jsem dost vytížený, takže asi zapojím do spolupráce i studenty,” dodává. Na svém výzkumu pak spolupracuje i s odborníky ze světa. „Na článku o teorii řetězců s námi spolupracoval profesor Yu-Fang Chen z Tchaj-wanu. A vypadá to, že budeme ve spolupráci pokračovat. Rýsuje se ale i nějaká spolupráce s lidmi z univerzity ve švédské Uppsale, “ podotýká Hečko.

Ačkoliv si ocenění v rámci soutěže Brno Ph.D. Talent cení, upozorňuje, že pro ceny svůj výzkum nedělá. „Už během bakalářského studia jsem se naučil mít především interní motivaci a dělat věci, protože mě baví. Ale soutěž mi dala skvělou šanci obhájit si to, co dělám, před ostatními. A taky ukázat, že to má hodnotu. Protože prodávat matematiku či teoretickou informatiku v konkurenci takových projektů, jako je hledání nových proteinů za pomoci AI, je velmi těžké,” říká Michal Hečko, který by ve vědě alespoň částečně rád zůstal i v budoucnu.

Dodává pak, že za úspěch i motivaci působit ve vědě, vděčí také svému vedoucímu. „Vždycky mi byl ochotný pomoct. A je fajn mít někoho, s kým se o tom můžu bavit, kdo mě povzbudí, nabídne jinou perspektivu. Taky mě ovlivnil docent Kubáček, který má na internetu sérii přednášek a má takový komický přístup k matematické analýze. Díky němu jsem si uvědomil, co mě na teoretické informatice vlastně baví. Nejsou to ty výpočty. Ale zjišťovat, proč vlastně věci fungují tak, jak fungují,” dodává na závěr Michal Hečko.