Tugevalt tagatud tarkvara laboratoorium

Andmed on kujunenud tähtsaimaks ressursiks majanduse ja avaliku halduse automatiseerimise ning lahenduste optimiseerimise jaoks. Projekti eesmärgiks on tõsta andmevaldkonna uurimistööde taset ja sünergiat, seeläbi oluliselt tugevdades Tehnikaülikooli võimekust koostööks eesti majanduse ja avaliku haldusega, nii ühisprojektide, konsultatsioonide kui täiendõppe ja tudengite ettevalmistamise kaudu. Sel eesmärgil fokuseerub projekt masinõppe kasutamisele andmevaldkonnas: masinõpe, seejuures eriti närvivõrgud, on tulevaste tarkvarasüsteemide võimekuse ja tarkvaraehituse peamine arengumootor. Konkreetne eesmärk on suurendada uute, tipptasemel spetsialistide arvu närvivõrkudel põhineva masinõppe valdkonnas, rakendades neid koostöösse olemasolevate andmeteaduse valdkondadega: andme- ja reeglikaevandamine, andmesemantika, inimkeelsed andmepäringud, teadmiste esitamine, andmeintegratsioon, statistika ja andmehaldus.

Käesoleva projekti eesmärk on töötada välja ja täiustada olemasolevaid seletatava tehisintellekti meetodeid inimese motoorsete funktsioonide analüüsimiseks. Pilootuuringud on näidanud paljulubavaid tulemusi neurodegeneratiivsete haiguste diagnoosimisel. Lisaks plaanime laiendada meetodite rakendusala meditsiinist kognitiivse arengu ja kognitiivse väsimuse analüüsile. Seletava komponendi integreerimine tagab meditsiinitöötajatele tehisintellekti tehtud otsuste vajaliku läbipaistvuse. Rakendus kognitiivse arengu valdkonnas koolihariduse protsessi toetamiseks. Kognitiivne väsimus põhjustab teadaolevalt raskeid vigastusi ja tõsist rahalist kahju. Selle nähtuse põhjalik mõistmine ja oskus väsimust ära tunda aitab muuta töökeskkond turvalisemaks ja vähendada rahalisi ja mitterahalisi kahjusid tööprotsessis.

Projekt uurib uusi sõltuvate tüüpidega tüübisüsteme, mis on sobilikud programmeerimiskeelte semantikate arendamiseks ja formaliseerimiseks tõestusassistentide abil. Eriline rõhk on keeltel, mis toetavad konkurentsust ja mittedetermiminismi, nt oleku-siirdesüsteemid ja protsessiarvutused. Populaarsed tüübiteoreetilised tõestusassistendid nagu Agda ja Coq ei sobi niisuguste keelte denotatsioonsemantika esitamiseks, kuna nende tüübisüsteemid ei ole piisavalt väljendusvõimsad. Me vastame sellele väljakutsele sel moel, et toome kaasaegsetesse tüübiteoreetilistesse raamistutesse nagu homotoopiline tüübiteooria sisse uue klassi koinduktiivseid tüüpe, mis esitavad saavutatavate funktorite terminaalseid koalgebraid. Denotatsioonsemantikas läheb protsesside mittedeteministliku ja interageeruva käitumise esitamiseks vaja tüüpe just sellest klassist. Loodavad väljendusvõimsamad tüübisüsteemid lubavad konkurentsuse ja mittedeterminismiga keelte formaalset semantikat adekvaatselt kodeerida.