Rättvisare arbetsscheman och pålitligare datasystem genom automatisering av logisk slutledning

Professor Matti Järvisalo vill skapa effektiva lösningsmetoder för beräkningsproblem som kräver exakthet och bevisligen korrekt resultat.

Vad forskar du i?

Jag forskar i automatisering av logisk slutledning och optimering med datorer på såväl teoretisk som praktisk nivå. Mitt huvudmål är att skapa effektiva allmänna lösningsmetoder för komplexa beräkningsproblem som uppstår i verkliga världen.

Vad kommer din forskning att påverka, och hur?

Förmågan att lösa svåra optimeringsproblem kan förbättra vårt dagliga liv på flera sätt. Ju vettigare arbetsscheman vi kan följa, ju snabbare kuriren kan leverera ett paket eller ju smidigare rutter från punkt A till punkt B med olika färdmedel vi kan erbjudas, desto nöjdare är vi. Ju bättre vi kan utnyttja begränsade resurser – allt från pengar till naturresurser – i produktionen av olika varor, desto mer ansvarsfullt kan vi agera.

Både i egenskap av individer och som samhälle litar vi i hög grad på datatekniska system i vårt dagliga liv. Ofta märker vi hur beroende vi är först när de inte fungerar. Särskilt fel i säkerhetskritiska system – till exempel flygplanens autopilotsystem – kan ha katastrofala följder.

Sådana problem är så komplicerade att det oftast är omöjligt för människan att hitta optimala lösningar manuellt. De alltmer effektiva algoritmiska metoderna för automatiserad slutledning, som utvecklas inom mitt forskningsområde, möjliggör bland annat utveckling av bevisligen korrekta datatekniska system. Dessutom kan dom användas för bevisa eller motbevisa öppna matematiska hypoteser.

Vad inspirerar dig särskilt mycket inom ditt område just nu?

Ämnesområdet utvecklas snabbt. Det uppkommer hela tiden nya tillämpningar.

Det här skapar nya forskningsutmaningar. Bland de senaste kan nämnas till exempel utvecklingen av metoder för att granska korrektheten av automatiskt framställda certifikat.

I många olika sorters praktiska problem är det viktigt att hitta rättvisa lösningar. Till exempel, vid planering av arbetsscheman kan det vara viktigare att fördela arbetsuppgifterna rättvist mellan arbetstagarna än att bara minimera utgifterna.

Dessutom förutsätter användning av artificiell intelligens som hjälpmedel vid beslutsfattande, en förmåga att förklara för allmänheten varför metoderna föreslår vissa beslut och varför det går att lita på dem.

 

Matti Järvisalo är professor i datavetenskap (algoritmer och maskininlärning) vid Matematisk-naturvetenskapliga fakulteten.

Läs mer om andra nya professorer.