Dokazuje, da se goljufati ne splača

Dr. Anja Petković Komel je raziskovalka v ekipi za formalno preverjanje pravilnosti pri neprofitni organizaciji Argot Collective, ki je namenjena podpori platformi ethereum in sorodnih tehnologij.

Predstavite nam instrument, ki ga najpogosteje ali najraje uporabljate pri delu.

Najraje uporabljam avtomatski dokazovalnik. To je programska oprema, ki (namesto matematikov) išče matematične dokaze. V datoteko zapišem svoje aksiome in predpostavke ter trditev/lastnost/domnevo, za katero upam, da je resnična in dokazljiva, avtomatski dokazovalnik pa to potrdi, ovrže ali v doglednem času ne najde rešitve. Moje področje ni omejeno le na dokazovanje matematičnih lastnosti, temveč se je razširilo na dokazovanje pravilnosti programske opreme, algoritmov in varnostnih protokolov.

Kako bi povprečno razgledanemu v največ sto besedah razložili, kaj raziskujete?

Z eno besedno zvezo, raziskujem dokazovanje z računalnikom. Na primer dokazujemo, da so ekonomske spodbude na blockchain protokolih varne: po domače, dokazujemo, da se ne splača goljufati in da če upoštevamo pravila, nam drugi ne morejo ukrasti sredstev z računa s kriptovaluto.

Pri tem uporabljamo dve vrsti orodij: dokazovalni pomočniki nas (matematike/računalničarje) pri izpeljavi dokazov vodijo in za nas skrbno preverijo vse sklepe v dokazu, avtomatski dokazovalniki pa včasih namesto nas sami poiščejo dokaz. Ta orodja s pomočjo matematične teorije razvijamo in raziskujemo, kako lahko med seboj pravilno in učinkovito komunicirajo.

Zakaj imate radi znanost?

Ker mi pomaga odstirati tančico (meni/človeštvu) neznanega in z znanstvenimi metodami čim bolj objektivno razumeti nekatera področja sveta.

Želela bi si prelom v miselnosti v smer skrbi za sočloveka in okolje

Kaj dobrega bi vaše delo lahko prineslo človeštvu?

Ne glede na izkušenost programerja velja, da je verjetnost prisotnosti napake v programski opremi skoraj stoodstotna, saj smo ljudje po naravi zmotljivi. V nekritičnih sistemih se te napake odpravljajo sproti, ko se pokažejo med uporabo. V kritičnih sistemih – v medicinski opremi, letalstvu in vesoljski opremi, na finančnem trgu (npr. pri kriptovalutah), v računalniških prevedbah v strojno kodo itd. – pa si tega ne moremo oziroma ne želimo privoščiti, kajti posledice so lahko izguba življenj, visoke finančne izgube ali uničen ugled.

Moje delo prispeva k večji transparentnosti in varnosti računalniških programov: formalno (matematično) dokazovanje pravilnosti računalniških programov je zahteven in drag proces, zato se uporablja predvsem tam, kjer so posledice ne(pravilnega) delovanja kritične.

Kdaj ste vedeli, da boste raziskovalka?

Ko sem imela 12 let, sem vprašala mamo, katera je najvišja stopnja izobrazbe v našem izobraževalnem sistemu. In ko sem izvedela, da je to doktorat in da takrat raziskujemo meje znanega, sem bila navdušena.

Kaj zanimivega poleg raziskovanja še počnete?

Nekaj let sem sodelovala pri ustvarjanju oddaje Ugriznimo znanost na RTV SLO, kjer sem postavljala in razlagala matematične uganke. Ukvarjam se tudi s spodbudami za enakost spolov v znanosti. Pred kratkim sem postala mama in v tem obdobju življenja je materinstvo pomembna in zahtevna naloga. Sicer pa se ukvarjam tudi s petjem v zboru, igranjem košarke, kolesarjenjem, branjem knjig in meditacijo.

Matematika je kraljica in sužnja drugih ved

Kaj je ključna lastnost dobrega znanstvenika?

Radovednost, vztrajnost, sposobnost učinkovitega komuniciranja idej. Najbolj pa pogum, da se ne ustraši, ko nima odgovorov, temveč ga to še dodatno vzpodbudi k iskanju. Živimo v svetu, kjer velja veliko zakonitosti, ki jih danes še ne poznamo, zato se moramo vsak dan počutiti kot raziskovalci tega sveta.

Katero bo najbolj prelomno odkritje ali spoznanje v znanosti, ki bo spremenilo tok zgodovine v času vašega življenja?

Znanost je zelo obširna, toda na področju matematike in računalništva bo to verjetno umetna inteligenca.

Bi odpotovali na Mars, če bi se vam ponudila priložnost?

Na MaRS-u sem bila že večkrat. MaRS je namreč Matematično raziskovalno srečanje, ki ga organizira Društvo matematikov, fizikov in astronomov Slovenije. Tam je res zanimivo, še posebej za tiste, ki imamo radi matematiko. Pa verjetno je tudi bolj prijetno bivati tam kot na planetu Mars, zato mi to za zdaj zadostuje.

Na kateri vir energije bi stavili za prihodnost?

Trenutno povsem obnovljivi viri energije ne zadostujejo energetskim potrebam tega sveta, zato se mi zdi jedrska energija najboljša alternativa, ki je na voljo. Želim pa si, da bi v prihodnosti zmanjšali potrebe po energiji in nekoliko upočasnili tempo življenja.

S katerim znanstvenikom v vsej zgodovini človeštva bi šli na kavo?

Z Ado Lovelace, angleško matematičarko, ki je prva razvila model sodobnega računalnika, in z Mario Montessori, italijansko zdravnico, ki je razvijala znanstveno pedagogiko.

Katero knjigo, film, predavanje, spletno stran s področja znanosti priporočate bralcu?

Knjigo Scale avtorja Geoffreyja Westa, ki opisuje razmerja količin, ki se pojavljajo v naravi in družbi.

S področja kriptovalut in tehnologije blockchain pa priporočam knjigo Bitcoin and Cryptocurrency Technologies (avtorji Arvind Narayanan in drugi) in pripadajoča predavanja z Univerze Princeton (dostopno na spletni strani https://bitcoinbook.cs.princeton.edu/).

Česa ne vemo o vašem področju, pa bi nas presenetilo?

Ko matematiki dokažejo izreke in jih objavijo v (dobro recenzirani) znanstveni reviji, ponavadi verjamemo, da so pravilni. Vendar se je že (večkrat) zgodilo, da se je leta kasneje našla napaka v dokazu, včasih tako nepopravljiva, da izrek ne velja. To se je zgodilo tudi Vladimirju Vojevodskemu, ruskemu matematiku, ki je za svoje delo prejel Fieldsovo medaljo (najbolj prestižno nagrado za matematike). Nekaj let po prejemu nagrade je objavil nov rezultat, ki ga je desetletje kasneje ovrgel njegov matematični kolega. To je bil povod za pospešen razvoj dokazovalnih pomočnikov, kjer računalnik sistematično preverja dokaze.