| Abstract |
Šajā bakalaura darbā tiek pētīta teorēmu pierādīšanas asistentu izmantošana finanšu sektorā, pievēršoties to lomai finanšu algoritmu pareizības pārbaudē. Tajā ir izklāstīti formālās verifikācijas teorētiskie pamati, pierādījuma palīgu attīstība un to pielietojums tādās jomās kā tirdzniecības sistēmas, riska pārvaldība un viedie līgumi. Darbā iekļauts arī praktisks piemērs, kur, izmantojot Lean proof palīgu, tiek modelēts un formāli pierādīts finanšu algoritms. Rezultāti parāda, ka teorēmu pārbaudītāji var ievērojami uzlabot finanšu tehnoloģiju uzticamību, caurspīdīgumu un drošību. Pirmajā nodaļā ir paskaidrots, kāpēc teorēmu pierādītāji ir svarīgi tirgiem, apskatīta to vēsture un parādīti reālās finanšu pasaules piemēri. Otrajā nodaļā ir klasificēta tirdzniecības, riska, cenu noteikšanas un citi finanšu algoritmi, izceļot to matemātikas un verifikācijas izaicinājumus. Trešajā nodaļā ir salīdzināti Lean, Coq, Isabelle/HOL, HOL Light un Agda algoritmi, ņemot vērā loģiku, bibliotēkas, rīkus un piemērotību finanšu vajadzībām. Ceturtajā nodaļā ir ieviesti, pierādīti un Montekarlo testēti atlasīti tirdzniecības un riska algoritmi Lean valodā trīs sintētiskajos tirgos.
Dati par darba apjomu – 53 lappušu, 2 attēlu, 2 tabulu, 33 izmantoto informācijas avotu skaits. |
